LegendreCounterexample.lean

1 import KomorebiLSM.UniformIntervalMoments
2 import KomorebiLSM.SequentialLowerCertificate
3 import Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
4 import Mathlib.MeasureTheory.Integral.Pi
5 import Mathlib.Probability.Independence.Basic
6 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
7 import KomorebiLSM.BaseNormModels
8 import Mathlib.LinearAlgebra.Matrix.Rank
9 
10 /-! P55: two distinct strictly positive scalar laws with identical low-order
11 moments, including the exact total-variation distance and product semantics. -/
12 set_option autoImplicit false
13 open MeasureTheory Matrix
14 open scoped BigOperators ENNReal
15 
16 namespace Komorebi.LSM.LegendreCounterexample
17 
18 noncomputable section
19 
20 def L3 (u : ℝ) : ℝ := (5 * u^3 - 3 * u) / 2
21 
22 @[simp] theorem L3_neg (u : ℝ) : L3 (-u) = -L3 u := by unfold L3; ring
23 
24 @[simp] theorem L3_zero : L3 0 = 0 := by norm_num [L3]
25 
26 @[simp] theorem L3_one : L3 1 = 1 := by norm_num [L3]
27 
28 theorem L3_continuous : Continuous L3 := by unfold L3; fun_prop
29 
30 /-- A factorization gives the interval bound without presuming it. -/
31 theorem L3_le_one {u : ℝ} (hu : u ≤ 1) : L3 u ≤ 1 := by
32   have hq : 0 ≤ 5 * u^2 + 5 * u + 2 := by nlinarith [sq_nonneg (u + 1/2)]
33   have hm := mul_nonpos_of_nonpos_of_nonneg (sub_nonpos.mpr hu) hq
34   unfold L3
35   nlinarith
36 
37 theorem L3_abs_le_one {u : ℝ} (hu : u ∈ Set.Icc (-1 : ℝ) 1) : |L3 u| ≤ 1 := by
38   apply abs_le.mpr
39   constructor
40   · have h := L3_le_one (u := -u) (by linarith [hu.1])
41     rw [L3_neg] at h
42     linarith
43   · exact L3_le_one hu.2
44 
45 def density (ε : ℝ) (u : ℝ) : ℝ := 1 + ε * L3 u
46 
47 theorem density_continuous (ε : ℝ) : Continuous (density ε) := by
48   unfold density L3
49   fun_prop
50 
51 theorem density_positive {ε u : ℝ} (hε : |ε| < 1)
52     (hu : u ∈ Set.Icc (-1 : ℝ) 1) : 0 < density ε u := by
53   have habs : |ε * L3 u| < 1 := by
54     rw [abs_mul]
55     exact lt_of_le_of_lt (mul_le_mul_of_nonneg_left (L3_abs_le_one hu) (abs_nonneg ε))
56       (by simpa using hε)
57   have h := (abs_lt.mp habs).1
58   unfold density
59   linarith
60 
61 theorem measure_support : ∀ᵐ u ∂UniformIntervalMoments.measure, u ∈ Set.Icc (-1 : ℝ) 1 := by
62   unfold UniformIntervalMoments.measure AveragedCongruence.uniformInterval ProbabilityTheory.cond
63   have h : ∀ᵐ u ∂volume.restrict (Set.Ioc (-1 : ℝ) 1), u ∈ Set.Icc (-1 : ℝ) 1 :=
64     (ae_restrict_mem measurableSet_Ioc).mono fun _ h => ⟨h.1.le, h.2⟩
65   exact Measure.ae_smul_measure h _
66 
67 /-- Exact orthogonality for any power, derived from the uniform power moments. -/
68 theorem weighted_L3_integral (j : ℕ) :
69     (∫ u, u^j * L3 u ∂UniformIntervalMoments.measure) =
70       (5 * UniformIntervalMoments.moment (j + 3) -
71         3 * UniformIntervalMoments.moment (j + 1)) / 2 := by
72   have heq : (fun u : ℝ => u^j * L3 u) =
73       (fun u => (5 * u^(j+3) - 3 * u^(j+1)) / 2) := by
74     funext u
75     unfold L3
76     simp only [pow_add]
77     ring
78   rw [heq, integral_div, integral_sub
79     (UniformIntervalMoments.continuous_integrable (by fun_prop))
80     (UniformIntervalMoments.continuous_integrable (by fun_prop)),
81     integral_const_mul, integral_const_mul]
82   rfl
83 
84 theorem low_order_orthogonality (j : Fin 3) :
85     (∫ u, u^(j : ℕ) * L3 u ∂UniformIntervalMoments.measure) = 0 := by
86   rw [weighted_L3_integral]
87   fin_cases j <;> norm_num [UniformIntervalMoments.moment_formula]
88 
89 theorem density_moment (ε : ℝ) (j : Fin 3) :
90     (∫ u, u^(j : ℕ) * density ε u ∂UniformIntervalMoments.measure) =
91       UniformIntervalMoments.moment j := by
92   have heq : (fun u : ℝ => u^(j : ℕ) * density ε u) =
93       (fun u => u^(j : ℕ) + ε * (u^(j : ℕ) * L3 u)) := by
94     funext u
95     unfold density
96     ring
97   rw [heq, integral_add (UniformIntervalMoments.continuous_integrable (by fun_prop))
98     (UniformIntervalMoments.continuous_integrable (by unfold L3; fun_prop)),
99     integral_const_mul, low_order_orthogonality]
100   simp [UniformIntervalMoments.moment]
101 
102 theorem density_integral_one (ε : ℝ) :
103     (∫ u, density ε u ∂UniformIntervalMoments.measure) = 1 := by
104   have h := density_moment ε (0 : Fin 3)
105   simpa using h
106 
107 noncomputable def root : ℝ := Real.sqrt (3/5)
108 
109 theorem root_nonneg : 0 ≤ root := Real.sqrt_nonneg _
110 
111 theorem root_sq : root^2 = 3/5 := Real.sq_sqrt (by norm_num)
112 
113 theorem root_le_one : root ≤ 1 := by
114   exact Real.sqrt_le_iff.mpr ⟨by norm_num, by norm_num⟩
115 
116 theorem L3_nonpos_left {u : ℝ} (hu : u ∈ Set.Icc 0 root) : L3 u ≤ 0 := by
117   have hs : u^2 ≤ 3/5 := by nlinarith [root_nonneg, root_sq, hu.1, hu.2]
118   have hm := mul_nonpos_of_nonneg_of_nonpos hu.1 (by linarith : 5*u^2-3 ≤ 0)
119   unfold L3
120   nlinarith
121 
122 theorem L3_nonneg_right {u : ℝ} (hu : u ∈ Set.Icc root 1) : 0 ≤ L3 u := by
123   have hs : 3/5 ≤ u^2 := by nlinarith [root_nonneg, root_sq, hu.1, hu.2]
124   have hm := mul_nonneg (root_nonneg.trans hu.1) (by linarith : 0 ≤ 5*u^2-3)
125   unfold L3
126   nlinarith
127 
128 /-- The genuine signed polynomial integral on any interval. -/
129 theorem L3_interval_integral (a b : ℝ) :
130     (∫ u in a..b, L3 u) = (5*(b^4-a^4)/4 - 3*(b^2-a^2)/2)/2 := by
131   unfold L3
132   rw [intervalIntegral.integral_div, intervalIntegral.integral_sub (f := fun u : ℝ => 5 * u^3) (g := fun u : ℝ => 3*u)
133     ((continuous_const.mul (continuous_id.pow 3)).intervalIntegrable a b)
134     ((continuous_const.mul continuous_id).intervalIntegrable a b),
135     intervalIntegral.integral_const_mul, intervalIntegral.integral_const_mul, integral_pow, integral_id]
136   norm_num
137   ring
138 
139 /-- The absolute integral is computed by splitting at the actual positive root. -/
140 theorem L3_abs_integral : (∫ u, |L3 u| ∂UniformIntervalMoments.measure) = 13/40 := by
141   have hc : Continuous (fun u => |L3 u|) := L3_continuous.abs
142   have hleft : (∫ u in (0 : ℝ)..root, |L3 u|) = -(∫ u in (0 : ℝ)..root, L3 u) := by
143     rw [← intervalIntegral.integral_neg]
144     apply intervalIntegral.integral_congr
145     intro u hu
146     rw [Set.uIcc_of_le root_nonneg] at hu
147     exact abs_of_nonpos (L3_nonpos_left hu)
148   have hright : (∫ u in root..(1 : ℝ), |L3 u|) = ∫ u in root..(1 : ℝ), L3 u := by
149     apply intervalIntegral.integral_congr
150     intro u hu
151     rw [Set.uIcc_of_le root_le_one] at hu
152     exact abs_of_nonneg (L3_nonneg_right hu)
153   have hhalf : (∫ u in (0 : ℝ)..1, |L3 u|) = 13/40 := by
154     rw [← intervalIntegral.integral_add_adjacent_intervals
155       (hc.intervalIntegrable 0 root) (hc.intervalIntegrable root 1), hleft, hright,
156       L3_interval_integral, L3_interval_integral]
157     have h4 : root^4 = 9/25 := by nlinarith [sq_nonneg (root^2 - 3/5), root_sq]
158     rw [h4, root_sq]
159     norm_num
160   have hneg : (∫ u in (-1 : ℝ)..0, |L3 u|) = ∫ u in (0 : ℝ)..1, |L3 u| := by
161     have h := intervalIntegral.integral_comp_neg (a := (0 : ℝ)) (b := 1) (fun u => |L3 u|)
162     simpa using h.symm
163   rw [UniformIntervalMoments.integral_eq,
164     ← intervalIntegral.integral_add_adjacent_intervals
165       (hc.intervalIntegrable (-1) 0) (hc.intervalIntegrable 0 1), hneg, hhalf]
166   norm_num
167 
168 /-- These are genuine absolutely continuous laws, not just formal densities. -/
169 def rawLaw (ε : ℝ) : Measure ℝ :=
170   UniformIntervalMoments.measure.withDensity (fun u => ENNReal.ofReal (density ε u))
171 
172 theorem density_ae_positive {ε : ℝ} (hε : |ε| < 1) :
173     ∀ᵐ u ∂UniformIntervalMoments.measure, 0 < density ε u :=
174   measure_support.mono fun _ hu => density_positive hε hu
175 
176 theorem density_lintegral_one {ε : ℝ} (hε : |ε| < 1) :
177     (∫⁻ u, ENNReal.ofReal (density ε u) ∂UniformIntervalMoments.measure) = 1 := by
178   rw [← ofReal_integral_eq_lintegral_ofReal
179     (UniformIntervalMoments.continuous_integrable (density_continuous ε))
180     ((density_ae_positive hε).mono fun _ h => h.le), density_integral_one, ENNReal.ofReal_one]
181 
182 theorem rawLaw_isProbability {ε : ℝ} (hε : |ε| < 1) : IsProbabilityMeasure (rawLaw ε) := by
183   constructor
184   rw [rawLaw, withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ, density_lintegral_one hε]
185 
186 def law (ε : ℝ) (hε : |ε| < 1) : ProbabilityMeasure ℝ := ⟨rawLaw ε, rawLaw_isProbability hε⟩
187 
188 /-- Actual law integration agrees with weighted integration under the reference law. -/
189 theorem law_integral (ε : ℝ) (hε : |ε| < 1) (f : ℝ → ℝ) :
190     (∫ u, f u ∂(law ε hε : Measure ℝ)) =
191       ∫ u, density ε u * f u ∂UniformIntervalMoments.measure := by
192   change (∫ u, f u ∂rawLaw ε) = _
193   rw [rawLaw, integral_withDensity_eq_integral_toReal_smul
194     (density_continuous ε).measurable.ennreal_ofReal (ae_of_all _ fun _ => ENNReal.ofReal_lt_top)]
195   apply integral_congr_ae
196   filter_upwards [density_ae_positive hε] with u hu
197   rw [ENNReal.toReal_ofReal hu.le, smul_eq_mul]
198 
199 theorem law_moment (ε : ℝ) (hε : |ε| < 1) (j : Fin 3) :
200     (∫ u, u^(j : ℕ) ∂(law ε hε : Measure ℝ)) = UniformIntervalMoments.moment j := by
201   rw [law_integral]
202   simpa only [mul_comm] using density_moment ε j
203 
204 /-- Event probabilities are the actual restricted density integrals. -/
205 theorem law_event_real (ε : ℝ) (hε : |ε| < 1) (event : Set ℝ) (hevent : MeasurableSet event) :
206     (law ε hε : Measure ℝ).real event =
207       ∫ u in event, density ε u ∂UniformIntervalMoments.measure := by
208   change (rawLaw ε event).toReal = _
209   rw [rawLaw, withDensity_apply _ hevent]
210   exact (integral_eq_lintegral_of_nonneg_ae
211     (ae_restrict_of_ae ((density_ae_positive hε).mono fun _ h => h.le))
212     (density_continuous ε).aestronglyMeasurable.restrict).symm
213 
214 /-- The signed measure associated to the actual law has exactly the declared density. -/
215 theorem law_toSignedMeasure (ε : ℝ) (hε : |ε| < 1) :
216     (law ε hε : Measure ℝ).toSignedMeasure =
217       UniformIntervalMoments.measure.withDensityᵥ (density ε) := by
218   have hf : (∫⁻ u, ENNReal.ofReal (density ε u) ∂UniformIntervalMoments.measure) ≠ ⊤ := by
219     rw [density_lintegral_one hε]
220     exact ENNReal.one_ne_top
221   have hreal := withDensityᵥ_toReal (density_continuous ε).measurable.ennreal_ofReal.aemeasurable hf
222   refine hreal.symm.trans (WithDensityᵥEq.congr_ae ?_)
223   filter_upwards [density_ae_positive hε] with u hu
224   exact ENNReal.toReal_ofReal hu.le
225 
226 /-- Exact total variation of the actual positive probability laws. -/
227 theorem law_totalVariation (ε : ℝ) (hε : |ε| < 1) :
228     SequentialLowerCertificate.lawTV (law ε hε : Measure ℝ)
229       (law (-ε) (by simpa using hε) : Measure ℝ) = 13 * |ε| / 40 := by
230   have hdiff : Integrable (fun u => density ε u - density (-ε) u) UniformIntervalMoments.measure :=
231     UniformIntervalMoments.continuous_integrable ((density_continuous ε).sub (density_continuous (-ε)))
232   rw [SequentialLowerCertificate.lawTV, law_toSignedMeasure, law_toSignedMeasure,
233     ← withDensityᵥ_sub' (UniformIntervalMoments.continuous_integrable (density_continuous ε))
234       (UniformIntervalMoments.continuous_integrable (density_continuous (-ε))),
235     SignedMeasure.totalVariation_eq_variation, Measure.variation_withDensityᵥ hdiff,
236     Measure.real, withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ,
237     ← integral_norm_eq_lintegral_enorm hdiff.aestronglyMeasurable]
238   have heq : (fun u => ‖density ε u - density (-ε) u‖) =
239       (fun u => 2 * |ε| * |L3 u|) := by
240     funext u
241     rw [Real.norm_eq_abs, show density ε u - density (-ε) u = 2 * ε * L3 u by unfold density; ring,
242       abs_mul, abs_mul]
243     norm_num
244   rw [heq, integral_const_mul, L3_abs_integral]
245   ring
246 
247 theorem positive_law_totalVariation {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) :
248     SequentialLowerCertificate.lawTV (law ε (by rwa [abs_of_pos hε0]) : Measure ℝ)
249       (law (-ε) (by rwa [abs_neg, abs_of_pos hε0]) : Measure ℝ) = 13 * ε / 40 := by
250   simpa only [abs_of_pos hε0] using law_totalVariation ε (by rwa [abs_of_pos hε0])
251 
252 theorem laws_distinct {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) :
253     (law ε (by rwa [abs_of_pos hε0]) : Measure ℝ) ≠
254       (law (-ε) (by rwa [abs_neg, abs_of_pos hε0]) : Measure ℝ) := by
255   intro heq
256   have h := positive_law_totalVariation hε0 hε1
257   simp only [SequentialLowerCertificate.lawTV, heq, sub_self, SignedMeasure.totalVariation_zero,
258     Measure.real, Measure.coe_zero, Pi.zero_apply, ENNReal.toReal_zero, mul_zero] at h
259   linarith
260 
261 /-- Taking independent observations means the actual finite product measure. -/
262 def productLaw (ε : ℝ) (hε : |ε| < 1) (N : ℕ) : Measure (Fin N → ℝ) :=
263   Measure.pi (fun _ : Fin N => (law ε hε : Measure ℝ))
264 
265 instance productLaw_isProbability (ε : ℝ) (hε : |ε| < 1) (N : ℕ) :
266     IsProbabilityMeasure (productLaw ε hε N) := by unfold productLaw; infer_instance
267 
268 theorem productLaw_independent (ε : ℝ) (hε : |ε| < 1) (N : ℕ) :
269     ProbabilityTheory.iIndepFun (fun i (x : Fin N → ℝ) => x i) (productLaw ε hε N) :=
270   ProbabilityTheory.iIndepFun_pi (fun _ => measurable_id.aemeasurable)
271 
272 /-- Every low-order product moment factors and is independent of the sign. -/
273 theorem product_moments (ε : ℝ) (hε : |ε| < 1) (N : ℕ) (j : Fin N → Fin 3) :
274     (∫ x, ∏ i, (x i)^(j i : ℕ) ∂productLaw ε hε N) =
275       ∏ i, UniformIntervalMoments.moment (j i) := by
276   unfold productLaw
277   rw [integral_fintype_prod_eq_prod (fun (i : Fin N) (u : ℝ) => u^(j i : ℕ))]
278   apply Finset.prod_congr rfl
279   intro i _
280   exact law_moment ε hε (j i)
281 
282 theorem product_moments_equal (ε : ℝ) (hε : |ε| < 1) (N : ℕ) (j : Fin N → Fin 3) :
283     (∫ x, ∏ i, (x i)^(j i : ℕ) ∂productLaw ε hε N) =
284       ∫ x, ∏ i, (x i)^(j i : ℕ) ∂productLaw (-ε) (by simpa using hε) N := by
285   rw [product_moments, product_moments]
286 
287 /-- A one-dimensional positive operator density with identity mass functional. -/
288 def scalarOperator (ε u : ℝ) : ℝ →ₗ[ℝ] ℝ := density ε u • LinearMap.id
289 
290 @[simp] theorem scalarOperator_apply (ε u z : ℝ) : scalarOperator ε u z = density ε u * z := rfl
291 
292 theorem scalarOperator_positive {ε : ℝ} (hε : |ε| < 1) :
293     ∀ᵐ u ∂UniformIntervalMoments.measure,
294       ∀ z ∈ BaseNorm.scalarCone.carrier, scalarOperator ε u z ∈ BaseNorm.scalarCone.carrier := by
295   filter_upwards [density_ae_positive hε] with u hu
296   intro z hz
297   change 0 ≤ density ε u * z
298   exact mul_nonneg hu.le hz
299 
300 /-- Exact normalization on the whole predictive space. -/
301 theorem scalarOperator_normalized (ε z : ℝ) :
302     (∫ u, scalarOperator ε u z ∂UniformIntervalMoments.measure) = z := by
303   simp only [scalarOperator_apply, integral_mul_const, density_integral_one, one_mul]
304 
305 theorem scalar_initial_and_dimension :
306     (1 : ℝ) ∈ BaseNorm.scalarCone.base ∧ Module.finrank ℝ ℝ = 1 := by
307   constructor
308   · constructor <;> norm_num [BaseNorm.scalarCone]
309   · exact Module.finrank_self ℝ
310 
311 /-- An event acts on the scalar state by its actual law probability. -/
312 def eventOperator (ε : ℝ) (hε : |ε| < 1) (event : Set ℝ) : ℝ →ₗ[ℝ] ℝ :=
313   (law ε hε : Measure ℝ).real event • LinearMap.id
314 
315 theorem eventOperator_integral (ε : ℝ) (hε : |ε| < 1)
316     (event : Set ℝ) (hevent : MeasurableSet event) (z : ℝ) :
317     eventOperator ε hε event z = ∫ u in event, scalarOperator ε u z ∂UniformIntervalMoments.measure := by
318   simp only [eventOperator, LinearMap.smul_apply, LinearMap.id_apply, smul_eq_mul,
319     scalarOperator_apply, integral_mul_const]
320   rw [law_event_real ε hε event hevent]
321 
322 def wordProbability (ε : ℝ) (hε : |ε| < 1) (events : List (Set ℝ)) : ℝ :=
323   (events.map (fun event => (law ε hε : Measure ℝ).real event)).prod
324 
325 theorem event_word_scalar (ε : ℝ) (hε : |ε| < 1) (events : List (Set ℝ)) (z : ℝ) :
326     FiniteInstruments.wordAction (eventOperator ε hε) events z = wordProbability ε hε events * z := by
327   induction events generalizing z with
328   | nil => simp [FiniteInstruments.wordAction, wordProbability]
329   | cons event events ih =>
330     simp only [FiniteInstruments.wordAction, LinearMap.comp_apply, ih,
331       eventOperator, LinearMap.smul_apply, LinearMap.id_apply, smul_eq_mul,
332       wordProbability, List.map_cons, List.prod_cons]
333     ring
334 
335 /-- The scalar event representation is exactly the actual independent record law. -/
336 theorem rankone_event_realization (ε : ℝ) (hε : |ε| < 1) (N : ℕ) (events : Fin N → Set ℝ) :
337     (productLaw ε hε N).real (Set.univ.pi events) =
338       FiniteInstruments.wordAction (eventOperator ε hε) (List.ofFn events) 1 := by
339   rw [event_word_scalar, mul_one]
340   simp only [productLaw, Measure.real, Measure.pi_pi, ENNReal.toReal_prod,
341     wordProbability, List.map_ofFn, List.prod_ofFn, Function.comp_apply]
342 
343 /-- Every event-history/core table factors as an outer product. -/
344 theorem event_hankel_factor {I J : Type*} (ε : ℝ) (hε : |ε| < 1)
345     (tests : I → List (Set ℝ)) (histories : J → List (Set ℝ)) :
346     (fun i j => wordProbability ε hε (histories j ++ tests i)) =
347       Matrix.vecMulVec (fun i => wordProbability ε hε (tests i))
348         (fun j => wordProbability ε hε (histories j)) := by
349   funext i j
350   simp [wordProbability, Matrix.vecMulVec, List.map_append, List.prod_append, mul_comm]
351 
352 /-- A complete finite table containing empty history and test has rank exactly
353 one; this rules out a zero-dimensional predictive process. -/
354 theorem event_hankel_rank_one {I J : Type*} [Fintype J] (ε : ℝ) (hε : |ε| < 1)
355     (tests : I → List (Set ℝ)) (histories : J → List (Set ℝ))
356     (i₀ : I) (j₀ : J) (ht : tests i₀ = []) (hh : histories j₀ = []) :
357     Matrix.rank (fun i j => wordProbability ε hε (histories j ++ tests i)) = 1 := by
358   apply le_antisymm
359   · rw [event_hankel_factor]
360     exact Matrix.rank_vecMulVec_le _ _
361   · have hsub : Matrix.submatrix (fun i j => wordProbability ε hε (histories j ++ tests i))
362         (fun _ : Fin 1 => i₀) (fun _ : Fin 1 => j₀) = (1 : Matrix (Fin 1) (Fin 1) ℝ) := by
363       ext i j
364       fin_cases i
365       fin_cases j
366       simp [Matrix.submatrix, ht, hh, wordProbability]
367     have h := Matrix.rank_submatrix_le
368       (fun i j => wordProbability ε hε (histories j ++ tests i))
369       (fun _ : Fin 1 => i₀) (fun _ : Fin 1 => j₀)
370     rw [hsub, Matrix.rank_one, Fintype.card_fin] at h
371     exact h
372 
373 /-- The misspecification is genuine: a nonzero cubic perturbation does not
374 belong to the quadratic class even when equality is requested only on [-1,1]. -/
375 theorem density_not_quadratic {ε : ℝ} (hε : ε ≠ 0) :
376     ¬ ∃ c : Fin 3 → ℝ, ∀ u ∈ Set.Icc (-1 : ℝ) 1,
377       density ε u = ∑ k : Fin 3, c k * u^(k : ℕ) := by
378   rintro ⟨c, hc⟩
379   let p : Polynomial ℝ := Polynomial.ofFn 4 ![1, -3*ε/2, 0, 5*ε/2]
380   have heval (u : ℝ) : p.eval u = density ε u := by
381     simp only [p, UniformIntervalMoments.eval_ofFn, Fin.sum_univ_succ]
382     norm_num [density, L3, Matrix.cons_val_two]
383     ring
384   have heq : p = Polynomial.ofFn 3 c := by
385     apply Polynomial.eq_of_infinite_eval_eq
386     apply (Set.Ioo_infinite (by norm_num : (-1 : ℝ) < 1)).mono
387     intro u hu
388     change p.eval u = (Polynomial.ofFn 3 c).eval u
389     rw [heval, UniformIntervalMoments.eval_ofFn]
390     exact hc u ⟨hu.1.le, hu.2.le⟩
391   have hcoeff := congrArg (fun q : Polynomial ℝ => q.coeff 3) heq
392   norm_num [p, Polynomial.ofFn_coeff_eq_val_of_lt, Polynomial.ofFn_coeff_eq_zero_of_ge] at hcoeff
393   apply hε
394   linarith
395 
396 end
397 end Komorebi.LSM.LegendreCounterexample

Back to source controls