WeightedFourthMoment.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The corrected weighted fourth coefficient-energy estimate of Appendix A.4. The proof uses the actual compression-fiber energy theorem and the actual rank-additive predecessor count, not hypotheses replacing either result. The remaining Fourier interpretation is separate: energy a X is the sum of squares of coefficients after the actual derivative compression.

lemma OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.half_cancel line 27
lemma OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.half_sum_identity line 32
lemma OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.half_sum_le line 41
lemma OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.finite_level_sum line 47
abbrev OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.rank line 104
def OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.vectorFintype line 106
def OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.compressedFintype line 110
def OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.energy line 117
Source documentation
Energy of the actual merged derivative coefficients.
```
def energy (a : (E →ₗ[F2] F) → ℝ) (X : E →ₗ[F2] F) : ℝ := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.predecessor_weight_sum line 124
Source documentation
Sum of predecessor weights, using the actual binary linear-map count.
```
theorem predecessor_weight_sum (Y : E →ₗ[F2] F) (d : ℕ) (hd : rank Y ≤ d) :
    (∑ X ∈ Finset.univ.filter (fun X => RankBelow X Y),
      ((2:ℝ)⁻¹)^(4*d*rank X)) ≤ 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.rank
theorem OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.weighted_fourth_coefficient_energy line 154
Source documentation
Corrected Appendix A.4, in exact coefficient form, for arbitrary real coefficients supported on maps of rank at most d.
```
theorem weighted_fourth_coefficient_energy (a : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hdegree : ∀ Y, d < rank Y → a Y = 0) :
    (∑ X, ((2:ℝ)⁻¹)^(8*d*rank X)*(energy a X)^2) ≤ 2*(∑ Y, a Y^2)^2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.rank, OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.energy