HybridCompositionLemmas.lean`

52 declarations, 0 contain sorry, 0 declared as axioms

Genuine hybrid derivative composition: the effective subspaces have additive order, and the full translate average preserves the square of the second moment. Transport of an additional map derivative is a separate step.

theorem OAI.UniqueGamesTheorem.Appendix.HybridComposition.effective_hybrid_iff line 44
theorem OAI.UniqueGamesTheorem.Appendix.HybridComposition.nested_hybridDerivative_energy line 86
theorem OAI.UniqueGamesTheorem.Appendix.HybridComposition.nested_hybridDerivative_energySquare_average line 115
theorem OAI.UniqueGamesTheorem.Appendix.HybridComposition.finrank_comap_mkQ line 128
theorem OAI.UniqueGamesTheorem.Appendix.HybridComposition.order_effective line 173
theorem OAI.UniqueGamesTheorem.Appendix.OperatorNorm.energy_sum_sq_le_card_cube line 214
theorem OAI.UniqueGamesTheorem.Appendix.OperatorNorm.fourth_sum_le_card_cube line 249
theorem OAI.UniqueGamesTheorem.Appendix.OperatorNorm.average_fourth_sum_le_card_cube line 254
theorem OAI.UniqueGamesTheorem.Appendix.OperatorNorm.compressFrequency_eq_compress line 284
theorem OAI.UniqueGamesTheorem.Appendix.OperatorNorm.nested_projector_restriction_apply line 289
theorem OAI.UniqueGamesTheorem.Appendix.OperatorNorm.a5_outer_energy line 309
theorem OAI.UniqueGamesTheorem.Appendix.OperatorNorm.a5_summand_energy line 358
theorem OAI.UniqueGamesTheorem.Appendix.OperatorNorm.a5_energySquare_le line 409
theorem OAI.UniqueGamesTheorem.Appendix.OperatorNorm.map_hybrid_fourth_average line 454
theorem OAI.UniqueGamesTheorem.Appendix.OperatorNorm.a4_fourth_average_le line 478
theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.exponent_le line 530
Source documentation
The exponent comparison after retaining the total degree loss.
```
theorem exponent_le (d i j t : ℕ) (hi : i ≤ t) (hj : j ≤ t) (ht : t ≤ d) :
    7 * d * (i + j) + 3 * i * j ≤ 24 * d * t := by
…
```

theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.weighted_moment_le line 541

Source documentation

Degree-forced zero moments allow the same weight bound on every raw triple.

theorem weighted_moment_le (d i j t : ℕ) (e : ℝ)
    (hi : i ≤ t) (hj : j ≤ t) (he : 0 ≤ e) (hz : d < t → e = 0) :
    (2 : ℝ) ^ (7 * d * (i + j) + 3 * i * j) * e ≤
      (2 : ℝ) ^ (24 * d * t) * e := by
…

def OAI.UniqueGamesTheorem.Appendix.A13Reduction.tripleMoment line 563
Source documentation
The actual averaged fourth moment attached to a raw derivative triple.
```
def tripleMoment (p : A4Index (K := F2) (W := F) (V := E))
…
```
theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.tripleMoment_nonneg line 568

theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.weak_fourth_le_counted line 577

Source documentation

A.4's native fourth-moment bound with its proved binary index count.

theorem weak_fourth_le_counted (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (A4GeometricIndex A B)] (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 M, spectralProjector (fun Y => A ≤ Y.range ∧ Y.ker ≤ B) f M ^ 4) ≤
      (2 : ℝ) ^ (3 * Module.finrank F2 A * Module.finrank F2 (F ⧸ B)) *
        ∑ p : A4GeometricIndex A B, tripleMoment p.val f := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.A13Reduction.tripleMoment

theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.weighted_weak_fourth_le_counted line 596

Source documentation

Expand one original weak-pair term, retaining its original dimensions.

theorem weighted_weak_fourth_le_counted (d : ℕ)
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (A4GeometricIndex A B)] (f : (E →ₗ[F2] F) → ℝ) :
    (2 : ℝ) ^ (7 * d * (Module.finrank F2 A + Module.finrank F2 (F ⧸ B))) *
      (𝔼 M, spectralProjector (fun Y => A ≤ Y.range ∧ Y.ker ≤ B) f M ^ 4) ≤
    ∑ p : A4GeometricIndex A B,
      (2 : ℝ) ^ (7 * d * (Module.finrank F2 A + Module.finrank F2 (F ⧸ B)) +
        3 * Module.finrank F2 A * Module.finrank F2 (F ⧸ B)) * tripleMoment p.val f := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.A13Reduction.tripleMoment

theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.tripleMoment_eq_zero_of_lt_size line 611
def OAI.UniqueGamesTheorem.Appendix.A13Reduction.tripleTerm line 619
Source documentation
The weight after relabeling the actual raw derivative triple.
```
def tripleTerm (d : ℕ) (p : A13Index.Triple (E := E) (F := F))
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.A13Index.Triple
theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.tripleTerm_nonneg line 624
theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.tripleTerm_eq_zero_of_lt_size line 628
theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.weighted_geometric_moment_le line 635
def OAI.UniqueGamesTheorem.Appendix.A13Reduction.positiveTripleSum line 656
Source documentation
The displayed A.13 sum: its original positive total order is retained.
```
def positiveTripleSum (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) : ℝ :=
…
```
def OAI.UniqueGamesTheorem.Appendix.A13Reduction.boundedPositiveTripleSum line 660
Source documentation
The same sum after the genuine degree-support cutoff.
```
def boundedPositiveTripleSum (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.weakFourthSum_le_positiveTripleSum line 666
Source documentation
Apply A.4 and its count, then forget the uniquely reconstructible weak pair. The old nonzero condition is carried by positiveMap; no descendant condition is substituted for it.
```
theorem weakFourthSum_le_positiveTripleSum (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hf : DerivativeDegree.DegreeAtMost d f) :
    A1Reduction.weakFourthSum d f ≤ positiveTripleSum d f := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.DegreeAtMost, OAI.UniqueGamesTheorem.Appendix.A1Reduction.weakFourthSum, OAI.UniqueGamesTheorem.Appendix.A13Reduction.positiveTripleSum
theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.positiveTripleSum_eq_bounded line 698
theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.degree_reduction line 720
Source documentation
Equation A.13 with the literal positive-triple sum.
```
theorem degree_reduction (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hf : DerivativeDegree.DegreeAtMost d f) :
    (𝔼 M, f M ^ 4) / 162 ≤
      (2 : ℝ) ^ (6 * d ^ 2) * (𝔼 M, f M ^ 2) ^ 2 + positiveTripleSum d f := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.DegreeAtMost, OAI.UniqueGamesTheorem.Appendix.A13Reduction.positiveTripleSum
theorem OAI.UniqueGamesTheorem.Appendix.A13Reduction.degree_reduction_truncated line 728
Source documentation
Equation A.13 after removing terms whose actual derivative is zero.
```
theorem degree_reduction_truncated (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hf : DerivativeDegree.DegreeAtMost d f) :
    (𝔼 M, f M ^ 4) / 162 ≤
      (2 : ℝ) ^ (6 * d ^ 2) * (𝔼 M, f M ^ 2) ^ 2 + boundedPositiveTripleSum d f := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.DegreeAtMost, OAI.UniqueGamesTheorem.Appendix.A13Reduction.boundedPositiveTripleSum
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.rank_arrowCongr line 774
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.rankBelow_arrowCongr line 786
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.trace_arrowCongr line 795
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.character_arrowCongr line 805
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.admissible_arrowCongr line 813
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.derivative_embedding_range line 822
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.linearCoeff_pullback line 857
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.rankProjector_pullback line 870
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.mapDerivative_energy_pullback line 882
def OAI.UniqueGamesTheorem.Appendix.NaturalTransport.quotientFactor line 905
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.quotientFactor_mkQ line 913
def OAI.UniqueGamesTheorem.Appendix.NaturalTransport.outputFactor line 918
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.outputFactor_val line 923
def OAI.UniqueGamesTheorem.Appendix.NaturalTransport.parameterFactor line 926
def OAI.UniqueGamesTheorem.Appendix.NaturalTransport.dualFactor line 931
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.dualFactor_rank line 939
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.parameterFactor_embedding line 947
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.nested_hybridDerivative_function line 957
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.nested_mapDerivative_energy line 980
theorem OAI.UniqueGamesTheorem.Appendix.NaturalTransport.nested_mapDerivative_energySquare_average line 992