LevelInequality.lean`

67 declarations, 0 contain sorry, 0 declared as axioms

The real-valued finite-probability steps at the end of Appendix A.5.

The results here prove normalized Cauchy--Schwarz/Hölder consequences and Boolean moment identities. They do not introduce Proposition A.5 or Lemma A.6 as axioms, and do not identify a conditional estimate with Theorem 2.3.

def OAI.MaxCutGames.Appendix.LevelInequality.IsBoolean line 20
theorem OAI.MaxCutGames.Appendix.LevelInequality.boolean_nonneg line 23
theorem OAI.MaxCutGames.Appendix.LevelInequality.boolean_sq line 27
theorem OAI.MaxCutGames.Appendix.LevelInequality.boolean_positive_moment line 30
theorem OAI.MaxCutGames.Appendix.LevelInequality.boolean_squared_norm_eq_density line 36
theorem OAI.MaxCutGames.Appendix.LevelInequality.boolean_four_thirds_moment line 40
theorem OAI.MaxCutGames.Appendix.LevelInequality.boolean_holder_fourth line 46
theorem OAI.MaxCutGames.Appendix.LevelInequality.fourth_power_le_implies_le line 78
Source documentation
The fourth-root conversion used in the final displayed inequality. This is an elementary real estimate, independent of Fourier analysis.
```
theorem fourth_power_le_implies_le {a b : ℝ} (_ha : 0 ≤ a) (hb : 0 ≤ b)
    (h : a ^ 4 ≤ b ^ 4) : a ≤ b := by
…
```

theorem OAI.MaxCutGames.Appendix.LevelInequality.boolean_level_bound_of_fourth_moment line 88

Source documentation

Once the genuine fourth-moment estimate has been established, this proves the final Boolean Hölder implication. The fourth-moment estimate is an explicit hypothesis here; this lemma itself is not Theorem 2.3.

theorem boolean_level_bound_of_fourth_moment {f h : α → ℝ}
    (hf : IsBoolean f) (d : ℕ) (η : ℝ) (hη : 0 ≤ η)
    (hprojection : (𝔼 x, h x ^ 2) = 𝔼 x, h x * f x)
    (hfourth : (𝔼 x, h x ^ 4) ≤ (2 : ℝ) ^ (113 * d * d) * η * (𝔼 x, f x)) :
    (𝔼 x, h x ^ 2) ≤
      (2 : ℝ) ^ (30 * d * d) * η ^ ((1 : ℝ) / 4) * (𝔼 x, f x ^ 2) := by
…

Mentions: OAI.MaxCutGames.Appendix.LevelInequality.IsBoolean

def OAI.MaxCutGames.Appendix.LevelInequality.frequencyRank line 138
Source documentation
The actual rank of a Fourier index S : F → E.
```
def frequencyRank (S : F →ₗ[F2] E) : ℕ := Module.finrank F2 (LinearMap.range S)
```
def OAI.MaxCutGames.Appendix.LevelInequality.rankLevel line 140
theorem OAI.MaxCutGames.Appendix.LevelInequality.linearCoeff_rankLevel line 144
theorem OAI.MaxCutGames.Appendix.LevelInequality.rankLevel_energy line 155
Source documentation
The selected rank mass equals the normalized squared norm of the actual rank projection.
```
theorem rankLevel_energy (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, rankLevel d f X ^ 2) =
      ∑ S with frequencyRank S = d, linearCoeff f S ^ 2 := by
…
```
Mentions: OAI.MaxCutGames.Appendix.LevelInequality.rankLevel, OAI.MaxCutGames.Appendix.LevelInequality.frequencyRank
theorem OAI.MaxCutGames.Appendix.LevelInequality.rankLevel_inner_self line 164
Source documentation
Orthogonal-projection identity used in the final Hölder step.
```
theorem rankLevel_inner_self (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, rankLevel d f X ^ 2) = 𝔼 X, rankLevel d f X * f X := by
…
```
Mentions: OAI.MaxCutGames.Appendix.LevelInequality.rankLevel
theorem OAI.MaxCutGames.Appendix.LevelInequality.rankLevel_energy_le line 174
Source documentation
Rank projection contracts the normalized L2 norm.
```
theorem rankLevel_energy_le (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, rankLevel d f X ^ 2) ≤ 𝔼 X, f X ^ 2 := by
…
```
Mentions: OAI.MaxCutGames.Appendix.LevelInequality.rankLevel
theorem OAI.MaxCutGames.Appendix.LevelInequality.rankLevel_degree_le line 181
theorem OAI.MaxCutGames.Appendix.LevelInequality.rankLevel_bound_of_fourth_moment line 186
def OAI.MaxCutGames.Appendix.LevelInequality.IsRestrictionGlobal line 197
theorem OAI.MaxCutGames.Appendix.LevelInequality.boolean_restriction line 203
theorem OAI.MaxCutGames.Appendix.LevelInequality.boolean_global_iff_density line 213
Source documentation
On Boolean functions the restriction-global norm bound is exactly the restriction-density hypothesis in Theorem 2.3.
```
theorem boolean_global_iff_density (f : (E →ₗ[F2] F) → ℝ) (hf : IsBoolean f)
    (d : ℕ) (η : ℝ) :
    IsRestrictionGlobal f d η ↔
      ∀ (A : Submodule F2 E) (B : Submodule F2 F) (T : E →ₗ[F2] F),
        MaxCutGames.Fourier.MatrixRestrictions.order A B ≤ d →
          (𝔼 N, MaxCutGames.Fourier.MatrixRestrictions.restrict f A B T N) ≤ η := by
…
```
Mentions: OAI.MaxCutGames.Appendix.LevelInequality.IsBoolean, OAI.MaxCutGames.Appendix.LevelInequality.IsRestrictionGlobal, OAI.MaxCutGames.Fourier.MatrixRestrictions.order, OAI.MaxCutGames.Fourier.MatrixRestrictions.restrict
def OAI.MaxCutGames.Appendix.LevelInequality.Theorem23 line 222
def OAI.MaxCutGames.Appendix.DerivativeDegree.DegreeAtMost line 252
Source documentation
Fourier support is restricted to maps of rank at most d.
```
def DegreeAtMost (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) : Prop :=
…
```
theorem OAI.MaxCutGames.Appendix.DerivativeDegree.DegreeAtMost.mono line 256
theorem OAI.MaxCutGames.Appendix.DerivativeDegree.degree_rankLevel line 261
theorem OAI.MaxCutGames.Appendix.DerivativeDegree.degree_spectralProjector line 265
theorem OAI.MaxCutGames.Appendix.DerivativeDegree.eq_zero_of_linearCoeff_zero line 272
theorem OAI.MaxCutGames.Appendix.DerivativeDegree.hybridDerivative_coeff_zero_of_lt line 291
theorem OAI.MaxCutGames.Appendix.DerivativeDegree.degree_hybridDerivative line 319
theorem OAI.MaxCutGames.Appendix.DerivativeDegree.hybridDerivative_eq_zero_of_lt_order line 326
theorem OAI.MaxCutGames.Appendix.DerivativeDegree.mapDerivative_coeff_zero_of_lt line 334
theorem OAI.MaxCutGames.Appendix.DerivativeDegree.degree_mapDerivative line 356
theorem OAI.MaxCutGames.Appendix.DerivativeDegree.mapDerivative_eq_zero_of_lt_rank line 362
theorem OAI.MaxCutGames.Appendix.DerivativeDegree.mapDerivative_zero line 369
theorem OAI.MaxCutGames.Appendix.DerivativeDegree.degree_map_hybridDerivative line 376

theorem OAI.MaxCutGames.Appendix.DerivativeDegree.map_hybridDerivative_eq_zero_of_lt_order_rank line 386

Source documentation

The support cutoff keeps the total order intact even when order A B > d.

theorem map_hybridDerivative_eq_zero_of_lt_order_rank
    (A : Submodule F2 E) (B : Submodule F2 F)
    (X : B →ₗ[F2] (E ⧸ A)) (T : E →ₗ[F2] F) {d : ℕ}
    (f : (E →ₗ[F2] F) → ℝ) (hf : DegreeAtMost d f)
    (h : d < order A B + Module.finrank F2 X.range) :
    mapDerivative X (hybridDerivative A B T f) = 0 := by
…

Mentions: OAI.MaxCutGames.Appendix.DerivativeDegree.DegreeAtMost

theorem OAI.MaxCutGames.Appendix.DerivativeDegree.map_hybridDerivative_fourth_average_eq_zero_of_lt_order_rank line 399
theorem OAI.MaxCutGames.Appendix.DegreeZero.rank_pos_of_ne_zero line 420
theorem OAI.MaxCutGames.Appendix.DegreeZero.eq_constant_of_degree_zero line 433
theorem OAI.MaxCutGames.Appendix.DegreeZero.fourth_moment_eq_energy_sq line 443
def OAI.MaxCutGames.Appendix.A5IndexCount.insideEquiv line 462
theorem OAI.MaxCutGames.Appendix.A5IndexCount.internal_isCompl line 471
def OAI.MaxCutGames.Appendix.A5IndexCount.projectionA0 line 488
theorem OAI.MaxCutGames.Appendix.A5IndexCount.projectionA0_injective line 494
def OAI.MaxCutGames.Appendix.A5IndexCount.fullRange line 524
theorem OAI.MaxCutGames.Appendix.A5IndexCount.fullRange_surjective line 529
theorem OAI.MaxCutGames.Appendix.A5IndexCount.quotientRestriction_surjective line 533
theorem OAI.MaxCutGames.Appendix.A5IndexCount.quotientRestriction_same_kernel line 544
def OAI.MaxCutGames.Appendix.A5IndexCount.sectionB0 line 558
theorem OAI.MaxCutGames.Appendix.A5IndexCount.range_sectionB0 line 566
theorem OAI.MaxCutGames.Appendix.A5IndexCount.recover_sectionB0 line 573
theorem OAI.MaxCutGames.Appendix.A5IndexCount.sectionB0_injective line 591
def OAI.MaxCutGames.Appendix.A5IndexCount.encode line 602
theorem OAI.MaxCutGames.Appendix.A5IndexCount.encode_injective line 608
theorem OAI.MaxCutGames.Appendix.A5IndexCount.card_geometricIndex_le line 621
theorem OAI.MaxCutGames.Appendix.A5IndexCount.card_geometricIndex_degree_le line 640
theorem OAI.MaxCutGames.Appendix.A5IndexCount.card_geometricIndex_cube_le line 655

theorem OAI.MaxCutGames.Appendix.Induction.outer_order_cutoff line 672

Source documentation

The corrected outer-order cutoff (A.14), with natural subtraction explicit.

theorem outer_order_cutoff (d i j k a b : Nat)
    (ha : i + k ≤ a) (hb : j + k ≤ b) (ht : i + j + k ≤ d)
    (ho : (a - i - k) + (b - j - k) ≤ d - (i + j + k)) :
    a + b ≤ d + k := by
…

theorem OAI.MaxCutGames.Appendix.Induction.complement_dimension_bounds line 679

Source documentation

Each complementary-space dimension is at most the original degree.

theorem complement_dimension_bounds (d i j k a b : Nat)
    (ha : i + k ≤ a) (hb : j + k ≤ b) (h : a + b ≤ d + k) :
    a - i ≤ d ∧ b - j ≤ d := by
…

theorem OAI.MaxCutGames.Appendix.Induction.recombined_order_cutoff line 685
Source documentation
Recombination preserves the required derivative degree cutoff.
```
theorem recombined_order_cutoff (d k a b : Nat)
    (ha : k ≤ a) (hb : k ≤ b) (h : a + b ≤ d + k) :
    (a - k) + (b - k) + k ≤ d := by
…
```
theorem OAI.MaxCutGames.Appendix.Induction.square_remainder_budget line 690
theorem OAI.MaxCutGames.Appendix.Induction.induction_exponent_budget line 701
Source documentation
The exponent inequality preceding (A.16), with negative exponents moved to the left side so natural subtraction cannot hide an invalid inequality.
```
theorem induction_exponent_budget (d t k : Nat) (ht : t ≤ d) (hk : k ≤ t) :
    100 * ((d - t) * (d - t)) + 27 * (d * t) + 6 * (d * k) +
      63 * (d * t) + 4 * (d * k) ≤ 100 * (d * d) := by
…
```
theorem OAI.MaxCutGames.Appendix.Induction.antecedent_exponent_budget line 708
theorem OAI.MaxCutGames.Appendix.Induction.first_triangle_exponent_budget line 719
Source documentation
The factor from the fourth-power triangle inequality fits inside the 12d(i+j) budget used before (A.13).
```
theorem first_triangle_exponent_budget (d i j : Nat) (hi : i ≤ d) :
    7 * (d * (i + j)) + 3 * (i * j) ≤ 12 * (d * (i + j)) := by
…
```
theorem OAI.MaxCutGames.Appendix.Induction.initial_order_bound line 726
Source documentation
The derivative order t is at least half the original pair order.
```
theorem initial_order_bound (i j k : Nat) (hi : k ≤ i) (hj : k ≤ j) :
    i + j ≤ 2 * (i + j - k) := by
…
```
theorem OAI.MaxCutGames.Appendix.Induction.positive_rank_geometric_slack line 731
Source documentation
For positive k the geometric-series exponent has at least d of slack.
```
theorem positive_rank_geometric_slack (d k : Nat) (hk : 1 ≤ k) :
    31 * (d * (k + 1)) + d ≤ 63 * (d * k) := by
…
```
theorem OAI.MaxCutGames.Appendix.Induction.corrected_weight_exponent line 738
Source documentation
The rank-dependent decay in (A.16) contains the corrected 8dk weight.
```
theorem corrected_weight_exponent (d k : Nat) :
    31 * (d * (k + 1)) + 4 * (d * k) =
      31 * d + 27 * (d * k) + 8 * (d * k) := by
…
```

theorem OAI.MaxCutGames.Appendix.Induction.extension_unique line 748

Source documentation

When B′ plus the prescribed kernel spans the domain, the map on B′ determines its extension. Thus fixing image and kernel in the antecedent count leaves no additional induced-isomorphism choice. The hypotheses expose the only algebra used; the ambient finite vector spaces are not yet built.

theorem extension_unique {B V : Type} [Add B] [Add V]
    (zero : V) (X₁ X₂ : B → V) (B' K : B → Prop)
    (right_zero : ∀ v : V, v + zero = v)
    (add₁ : ∀ x y, X₁ (x + y) = X₁ x + X₁ y)
    (add₂ : ∀ x y, X₂ (x + y) = X₂ x + X₂ y)
    (span : ∀ x, ∃ b z, B' b ∧ K z ∧ x = b + z)
    (agree : ∀ b, B' b → X₁ b = X₂ b)
    (kill₁ : ∀ z, K z → X₁ z = zero)
    (kill₂ : ∀ z, K z → X₂ z = zero) : X₁ = X₂ := by
…