A5Induction.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Actual norm and induction steps for Proposition A.5. The universal degree property below is the motive for strong induction on the degree; defining that property does not assert its truth.

def OAI.MaxCutGames.Appendix.A5Induction.BoundAtDegree line 27
Source documentation
The strong-induction motive quantifies over the actual changing domains. Quotients and subspaces preserve the fixed universe levels.
```
def BoundAtDegree (d : ℕ) : Prop :=
…
```
theorem OAI.MaxCutGames.Appendix.A5Induction.damping_le line 37
theorem OAI.MaxCutGames.Appendix.A5Induction.coefficient_absorption line 55
def OAI.MaxCutGames.Appendix.A5Induction.dampedMapMoment line 93
Source documentation
The actual weighted map-derivative sum left by the finite reindexing.
```
def dampedMapMoment (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) : ℝ :=
…
```
theorem OAI.MaxCutGames.Appendix.A5Induction.dampedMapMoment_le line 98
def OAI.MaxCutGames.Appendix.A5Induction.dampedHybridMoment line 124
theorem OAI.MaxCutGames.Appendix.A5Induction.dampedHybridMoment_le line 128
theorem OAI.MaxCutGames.Appendix.A5Induction.hybridProjector_zero_pair line 147
theorem OAI.MaxCutGames.Appendix.A5Induction.energy_sq_le_hybridMomentSum line 153
theorem OAI.MaxCutGames.Appendix.A5Induction.degree_zero_bound line 188

theorem OAI.MaxCutGames.Appendix.A5Induction.recurrence_closure line 195

Source documentation

Close the actual recurrence once its finite index expansion is supplied. This lemma states that recurrence explicitly; it is not the public A.5 theorem.

theorem recurrence_closure (d : ℕ) (hd : 1 ≤ d)
    (f : (E →ₗ[F2] F) → ℝ) (hf : DegreeAtMost d f)
    (hrec : (𝔼 M, f M ^ 4) / 162 ≤
      (2 : ℝ) ^ (6 * d * d) * (𝔼 M, f M ^ 2)^2 +
        (2 : ℝ) ^ (100 * d * d) * dampedHybridMoment d f) :
    (𝔼 M, f M ^ 4) ≤ (2 : ℝ) ^ (100 * d * d) * hybridMomentSum d f := by
…

Mentions: OAI.MaxCutGames.Appendix.A5Induction.dampedHybridMoment

theorem OAI.MaxCutGames.Appendix.A5Induction.lifted_outer_dimensions line 231

Source documentation

Dimension bounds for the outer subspaces used by the actual A.5 operator identity, obtained from the order of an actual derivative-space index.

theorem lifted_outer_dimensions (X : F →ₗ[F2] E)
    (C : Submodule F2 (E ⧸ X.range)) (D : Submodule F2 X.ker)
    (d : ℕ) (hcut : Module.finrank F2 X.range + order C D ≤ d) :
    Module.finrank F2 (C.comap X.range.mkQ) ≤ d ∧
      Module.finrank F2 (F ⧸ D.map X.ker.subtype) ≤ d := by
…

theorem OAI.MaxCutGames.Appendix.A5Induction.a5_energySquare_le_power line 247

Source documentation

The native A.5 energy inequality with its actually proved numerical complement factor. The only cutoff is the rank plus the outer derivative order.

theorem a5_energySquare_le_power (X : F →ₗ[F2] E)
    (C : Submodule F2 (E ⧸ X.range)) (D : Submodule F2 X.ker)
    [Fintype (OperatorPartitions.A5GeometricIndex X
      (C.comap X.range.mkQ) (D.map X.ker.subtype))]
    (d : ℕ) (hcut : Module.finrank F2 X.range + order C D ≤ d)
    (f : (E →ₗ[F2] F) → ℝ) (S : Parameter X.range X.ker) :
    (𝔼 N, hybridDerivative C D S (mapDerivative X f) N ^ 2) ^ 2 ≤
      (2 : ℝ) ^ (6 * d * Module.finrank F2 X.range) *
        ∑ p : OperatorPartitions.A5GeometricIndex X
          (C.comap X.range.mkQ) (D.map X.ker.subtype),
          (𝔼 N, mapDerivative (LinearIdentities.compress X p.val.1 p.val.2)
            (hybridDerivative p.val.1 p.val.2 (embed X.range X.ker S) f) N ^ 2)^2 := by
…

Mentions: OAI.MaxCutGames.Appendix.OperatorPartitions.A5GeometricIndex, OAI.MaxCutGames.Appendix.LinearIdentities.compress

def OAI.MaxCutGames.Appendix.A5Induction.postA5Sum line 313
Source documentation
Actual A.5 descendants before recombining the first hybrid restriction.
```
def postA5Sum (X : F →ₗ[F2] E) (e : ℕ) (f : (E →ₗ[F2] F) → ℝ) : ℝ :=
…
```
theorem OAI.MaxCutGames.Appendix.A5Induction.mapDerivative_hybridMomentSum_le line 318
theorem OAI.MaxCutGames.Appendix.A5Induction.postA5Sum_hybrid_average line 345
Source documentation
Recombination uses the natural domain and codomain isomorphisms. The intermediate shifts need only be the actual embedded derivative parameters.
```
theorem postA5Sum_hybrid_average (A : Submodule F2 E) (B : Submodule F2 F)
    (X : B →ₗ[F2] (E ⧸ A)) (e : ℕ) (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 T, postA5Sum X e (hybridDerivative A B T f)) =
      A5Passage.descendantSum A B X e f := by
…
```
Mentions: OAI.MaxCutGames.Appendix.A5Induction.postA5Sum, OAI.MaxCutGames.Appendix.A5Passage.descendantSum

theorem OAI.MaxCutGames.Appendix.A5Induction.a15_of_strong_induction line 365

Source documentation

The actual A.15 induction step for one positive-order derivative triple. The induction hypothesis is used only at the strictly smaller degree d-t, on its genuine quotient-domain and kernel-codomain spaces.

theorem a15_of_strong_induction (d t : ℕ) (A : Submodule F2 E)
    (B : Submodule F2 F) (X : B →ₗ[F2] (E ⧸ A))
    (ht : t = order A B + Module.finrank F2 X.range)
    (htpos : 0 < t) (htd : t ≤ d)
    (ih : ∀ e, e < d → BoundAtDegree.{u, v} e)
    (f : (E →ₗ[F2] F) → ℝ) (hf : DegreeAtMost d f) :
    (𝔼 T, 𝔼 N, mapDerivative X (hybridDerivative A B T f) N ^ 4) ≤
      (2 : ℝ) ^ (100 * (d - t) * (d - t) + 6 * d * Module.finrank F2 X.range) *
        A5Passage.descendantSum A B X (d - t) f := by
…

Mentions: OAI.MaxCutGames.Appendix.A5Passage.descendantSum

theorem OAI.MaxCutGames.Appendix.A5Induction.boundedTripleSum_le_descendants line 403
Source documentation
Apply the genuine lower-degree induction step to every term of the checked A.13 sum, preserving its original positive-order cutoff.
```
theorem boundedTripleSum_le_descendants (d : ℕ)
    (ih : ∀ e, e < d → BoundAtDegree.{u, v} e)
    (f : (E →ₗ[F2] F) → ℝ) (hf : DegreeAtMost d f) :
    A13Reduction.boundedPositiveTripleSum d f ≤
      ∑ p : A13Index.BoundedPositiveTriple (E := E) (F := F) d,
…
```
Mentions: OAI.MaxCutGames.Appendix.A13Reduction.boundedPositiveTripleSum, OAI.MaxCutGames.Appendix.A13Index.BoundedPositiveTriple
theorem OAI.MaxCutGames.Appendix.A5Induction.boundAtDegree line 440
Source documentation
Proposition A.5 on every finite-dimensional binary linear-map space, proved by strong induction with all changing domains in the motive.
```
theorem boundAtDegree (d : ℕ) : BoundAtDegree.{u, v} d := by
…
```
theorem OAI.MaxCutGames.Appendix.A5Induction.derivative_inequality line 464
theorem OAI.MaxCutGames.Appendix.HybridCounting.comap_subtype_injective_inline_HybridCounting line 478
theorem OAI.MaxCutGames.Appendix.HybridCounting.map_quotient_injective_inline_HybridCounting line 491
theorem OAI.MaxCutGames.Appendix.HybridCounting.finite_submodules_inline_HybridCounting line 509
theorem OAI.MaxCutGames.Appendix.HybridCounting.card_hybrid_pairs_le line 519
Source documentation
All actual Hybrid pairs for this frequency, with no ambient-dimension factor.
```
theorem card_hybrid_pairs_le (Y : F →ₗ[F2] E) (d : ℕ)
    (hY : finrank F2 Y.range ≤ d) :
    Nat.card {p : Submodule F2 E × Submodule F2 F //
      LinearIdentities.Hybrid Y p.1 p.2} ≤ 2 ^ (2 * d * d) := by
…
```
Mentions: OAI.MaxCutGames.Appendix.LinearIdentities.Hybrid
theorem OAI.MaxCutGames.Appendix.HybridCounting.card_hybridIndex_le_two line 563
Source documentation
The actual order-bounded index subtype injects into the conditioned pairs.
```
theorem card_hybridIndex_le_two (Y : F →ₗ[F2] E) (d : ℕ)
    (hY : finrank F2 Y.range ≤ d) :
    Nat.card {s : Derivatives.HybridIndex (E := E) (F := F) d //
…
```
Mentions: OAI.MaxCutGames.Appendix.Derivatives.HybridIndex
theorem OAI.MaxCutGames.Appendix.HybridCounting.card_hybridIndex_le line 582
theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.selector_energy_le line 610
Source documentation
The actual selector multiplicity on frequencies of rank at most d. This uses only the proved finite subspace count and Parseval.
```
theorem selector_energy_le (d : ℕ) (g : (E →ₗ[F2] F) → ℝ)
    (hg : DegreeAtMost d g) :
    hybridSelectorEnergy d g ≤ (2 : ℝ) ^ (3 * d * d) * (𝔼 X, g X ^ 2) := by
…
```

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.fourth_moment_le_of_uniform_hybrid_energy line 632

Source documentation

Generic closure of the fourth-moment estimate from a uniform bound on the actual hybrid derivatives. Its eventual KMS application must prove hH from the basis-invariant function and its local densities.

theorem fourth_moment_le_of_uniform_hybrid_energy
    (d : ℕ) (g : (E →ₗ[F2] F) → ℝ) (hg : DegreeAtMost d g)
    (H : ℝ) (hH0 : 0 ≤ H)
    (hH : ∀ (A : Submodule F2 E) (B : Submodule F2 F) (T : E →ₗ[F2] F),
      order A B ≤ d → (𝔼 N, hybridDerivative A B T g N ^ 2) ≤ H) :
    (𝔼 X, g X ^ 4) ≤ (2 : ℝ) ^ (103 * d * d) * H * (𝔼 X, g X ^ 2) := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.rankComponent_eq_rankProjection line 678
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.rankComponent_invariant line 688
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.rankComponent_coeff_eq_zero_of_ne line 694
Source documentation
The degree bound follows from the literal coefficient filter.
```
theorem rankComponent_coeff_eq_zero_of_ne (i : ℕ)
    (f : (E →ₗ[F2] F) → ℝ) (S : F →ₗ[F2] E)
    (hS : Module.finrank F2 S.range ≠ i) :
    linearCoeff (rankComponent i f) S = 0 := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.rankComponent
theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.rankComponent_degree line 725
Source documentation
Actual finite Fourier support of the component, with no rank-level inequality invoked.
```
theorem rankComponent_degree (i : ℕ) (f : (E →ₗ[F2] F) → ℝ) :
    DerivativeDegree.DegreeAtMost i (rankComponent i f) := by
…
```

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.rankComponent_fourth_moment_le_of_hybrid line 734

Source documentation

Generic fourth-moment closure for the literal KMS rank component.

theorem rankComponent_fourth_moment_le_of_hybrid (i : ℕ)
    (f : (E →ₗ[F2] F) → ℝ) (H : ℝ) (hH0 : 0 ≤ H)
    (hH : ∀ (A : Submodule F2 E) (B : Submodule F2 F) (T : E →ₗ[F2] F),
      order A B ≤ i →
      (𝔼 N, Derivatives.hybridDerivative A B T (rankComponent i f) N ^ 2) ≤ H) :
    (𝔼 X, rankComponent i f X ^ 4) ≤
      (2 : ℝ) ^ (103 * i * i) * H * (𝔼 X, rankComponent i f X ^ 2) :=
…