KMSMomentTheorem.lean`

50 declarations, 0 contain sorry, 0 declared as axioms

The actual upper fourth-moment theorem for the full-rank lift of a Grassmann set. Its hypotheses are literal tuple probabilities. The affine sampling law, mixed estimate and hybrid derivative estimate are all discharged by proved lemmas; there is no analytic estimate among the hypotheses.

theorem OAI.MaxCutGames.Inverse.KMSMomentTheorem.lifted_fourth_moment_bound line 22

Source documentation

The upper moment has a constant depending only on the cutoff. Its tuple budget is 2r and its domain threshold is r, both fixed before the dimensions.

theorem lifted_fourth_moment_bound
    (r : ℕ) (ε : ℝ) (hε : 0 ≤ ε)
    (ell : ℕ) (hell : r ≤ ell) (n : ℕ)
    (S : Finset (Vertex n ell)) (hS : TuplePseudorandom S (2 * r) ε)
    (i : ℕ) (hi : i ≤ r) :
    (𝔼 X : BasisMap n ell, rankComponent i (liftedIndicator S) X ^ 4) ≤
      fourthMomentConstant r *
        (𝔼 X : BasisMap n ell, rankComponent i (liftedIndicator S) X ^ 2) * ε := by
…

def OAI.MaxCutGames.Inverse.KMSMomentScalar.IsBoolean line 63
theorem OAI.MaxCutGames.Inverse.KMSMomentScalar.boolean_nonneg line 66
theorem OAI.MaxCutGames.Inverse.KMSMomentScalar.boolean_sq line 70
theorem OAI.MaxCutGames.Inverse.KMSMomentScalar.boolean_average_nonneg line 73
theorem OAI.MaxCutGames.Inverse.KMSMomentScalar.boolean_squared_average line 76
theorem OAI.MaxCutGames.Inverse.KMSMomentScalar.boolean_fourth_holder line 83
Source documentation
Two finite Cauchy–Schwarz steps, with the Boolean support kept explicitly.
```
theorem boolean_fourth_holder {f : X → ℝ} (hf : IsBoolean f) (g : X → ℝ) :
    (𝔼 x, g x * f x) ^ 4 ≤ (𝔼 x, g x ^ 4) * (𝔼 x, f x) ^ 3 := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSMomentScalar.IsBoolean
theorem OAI.MaxCutGames.Inverse.KMSMomentScalar.projection_energy_le_density line 113
Source documentation
The squared norm of an orthogonal component is bounded by the Boolean function's density. The projection identity is the only needed property.
```
theorem projection_energy_le_density {f : X → ℝ} (hf : IsBoolean f) (g : X → ℝ)
    (hprojection : (𝔼 x, g x ^ 2) = 𝔼 x, g x * f x) :
    (𝔼 x, g x ^ 2) ≤ 𝔼 x, f x := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSMomentScalar.IsBoolean
theorem OAI.MaxCutGames.Inverse.KMSMomentScalar.projection_fifth_le_density_fourth_moment line 124
Source documentation
A stronger lower fourth-moment estimate than KMS Lemma 2.14, avoiding division by the density and remaining valid at density zero.
```
theorem projection_fifth_le_density_fourth_moment {f : X → ℝ} (hf : IsBoolean f)
    (g : X → ℝ) (hprojection : (𝔼 x, g x ^ 2) = 𝔼 x, g x * f x) :
    (𝔼 x, g x ^ 2) ^ 5 ≤ (𝔼 x, f x) ^ 4 * (𝔼 x, g x ^ 4) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSMomentScalar.IsBoolean
theorem OAI.MaxCutGames.Inverse.KMSMomentScalar.fourth_root_power line 139
theorem OAI.MaxCutGames.Inverse.KMSMomentScalar.le_of_fourth_power_le line 144
theorem OAI.MaxCutGames.Inverse.KMSMomentScalar.lowLevel_bound_of_fourthMoment line 151
def OAI.MaxCutGames.Inverse.KMSLowLevel.rankEnergy line 209
theorem OAI.MaxCutGames.Inverse.KMSLowLevel.sum_rankEnergy line 212

theorem OAI.MaxCutGames.Inverse.KMSLowLevel.spectral_cutoff line 224

Source documentation

Exact rank multiplier cutoff, without dimension-dependent constants.

theorem spectral_cutoff (rank : I → ℕ) (a : I → ℝ) (r : ℕ) :
    (∑ s, ((2 : ℝ) ^ rank s)⁻¹ * a s ^ 2) ≤
      (∑ i ∈ Finset.range (r + 1), rankEnergy rank a i) +
        ((2 : ℝ) ^ (r + 1))⁻¹ * ∑ s, a s ^ 2 := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSLowLevel.rankEnergy

theorem OAI.MaxCutGames.Inverse.KMSLowLevel.spectral_cutoff_of_level_bounds line 246
def OAI.MaxCutGames.Inverse.KMSLowLevel.uniformNoise line 271
Source documentation
The actual operator samples both rank-one factors uniformly, including zero.
```
def uniformNoise (f : (E →ₗ[F2] F) → ℝ) : (E →ₗ[F2] F) → ℝ :=
…
```
theorem OAI.MaxCutGames.Inverse.KMSLowLevel.uniformNoise_apply line 276
theorem OAI.MaxCutGames.Inverse.KMSLowLevel.uniformNoise_energy line 283
theorem OAI.MaxCutGames.Inverse.KMSLowLevel.rankEnergy_eq line 294

theorem OAI.MaxCutGames.Inverse.KMSLowLevel.rankComponent_bound line 302

Source documentation

The scalar fourth-moment argument applied to genuine rank projections.

theorem rankComponent_bound (f : (E →ₗ[F2] F) → ℝ) (hf : IsBoolean f)
    (r i : ℕ) (ε : ℝ) (hε : 0 ≤ ε)
    (hupper : (𝔼 X, rankComponent i f X ^ 4) ≤
      (2 : ℝ) ^ (25 * r ^ 3) * (𝔼 X, rankComponent i f X ^ 2) * ε) :
    (𝔼 X, rankComponent i f X ^ 2) ≤
      (2 : ℝ) ^ (7 * r ^ 3 + 3) * ε ^ ((1 : ℝ) / 4) * (𝔼 X, f X) := by
…

theorem OAI.MaxCutGames.Inverse.KMSLowLevel.uniformNoise_bound_of_fourthMoments line 313

Source documentation

The KMS spectral conclusion once the actual pseudorandom upper fourth moments have been proved. The error, cutoff and constants precede dimensions.

theorem uniformNoise_bound_of_fourthMoments (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBoolean f) (r : ℕ) (ε : ℝ) (hε : 0 ≤ ε)
    (hupper : ∀ i ≤ r, (𝔼 X, rankComponent i f X ^ 4) ≤
      (2 : ℝ) ^ (25 * r ^ 3) * (𝔼 X, rankComponent i f X ^ 2) * ε) :
    (𝔼 X, f X * uniformNoise f X) ≤
      ((r + 1 : ℕ) * ((2 : ℝ) ^ (7 * r ^ 3 + 3) * ε ^ ((1 : ℝ) / 4)) +
        ((2 : ℝ) ^ (r + 1))⁻¹) * (𝔼 X, f X) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSLowLevel.uniformNoise

theorem OAI.MaxCutGames.Inverse.KMSLowLevel.projection_bound_of_general_fourthMoment line 344

Source documentation

No particular polynomial in the cutoff is required for the scalar step.

theorem projection_bound_of_general_fourthMoment {X : Type*} [Fintype X]
    {f : X → ℝ} (hf : IsBoolean f) (g : X → ℝ)
    (C ε : ℝ) (hC : 0 ≤ C) (hε : 0 ≤ ε)
    (hprojection : (𝔼 x, g x ^ 2) = 𝔼 x, g x * f x)
    (hupper : (𝔼 x, g x ^ 4) ≤ C * (𝔼 x, g x ^ 2) * ε) :
    (𝔼 x, g x ^ 2) ≤ (C + 1) * ε ^ ((1 : ℝ) / 4) * (𝔼 x, f x) := by
…

theorem OAI.MaxCutGames.Inverse.KMSLowLevel.uniformNoise_bound_of_general_fourthMoments line 382

Source documentation

The actual full-uniform rank-one correlation, with a general moment constant.

theorem uniformNoise_bound_of_general_fourthMoments
    (f : (E →ₗ[F2] F) → ℝ) (hf : IsBoolean f)
    (r : ℕ) (C ε : ℝ) (hC : 0 ≤ C) (hε : 0 ≤ ε)
    (hupper : ∀ i ≤ r, (𝔼 X, rankComponent i f X ^ 4) ≤
      C * (𝔼 X, rankComponent i f X ^ 2) * ε) :
    (𝔼 X, f X * uniformNoise f X) ≤
      ((r + 1 : ℕ) * ((C + 1) * ε ^ ((1 : ℝ) / 4)) +
        ((2 : ℝ) ^ (r + 1))⁻¹) * (𝔼 X, f X) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSLowLevel.uniformNoise

theorem OAI.MaxCutGames.Inverse.KMSLowLevel.exists_general_cutoff_parameters line 402

Source documentation

Even an arbitrarily large constant depending on r alone permits the cutoff and tolerance to be chosen before both dimensions.

theorem exists_general_cutoff_parameters (C : ℕ → ℝ) (hC : ∀ r, 0 ≤ C r)
    {ζ : ℝ} (hζ : 0 < ζ) :
    ∃ r : ℕ, 1 ≤ r ∧ ∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 ∧
      (r + 1 : ℕ) * ((C r + 1) * ε ^ ((1 : ℝ) / 4)) +
        ((2 : ℝ) ^ (r + 1))⁻¹ ≤ ζ / 2 := by
…

theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.expect_coe_eq line 456
Source documentation
Finset conditioning and uniform sampling from its membership subtype are the same normalized finite sum, including the empty event.
```
theorem expect_coe_eq (s : Finset Ω) (f : Ω → ℝ) :
    (𝔼 x : s, f x.val) = s.expect f := by
…
```
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.expect_unit_interval line 462
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.mass_mul_expect line 472
Source documentation
The weighted conditional expectation is the unnormalized sum divided by the ambient cardinality, also for an empty conditioning event.
```
theorem mass_mul_expect (s : Finset Ω) (f : Ω → ℝ) :
    (s.card : ℝ) / Fintype.card Ω * s.expect f =
      (∑ x ∈ s, f x) / Fintype.card Ω := by
…
```

theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.expect_partition line 485

Source documentation

Exact two-event total expectation, with the same zero convention on both conditional expectations as mathlib's finite expectation.

theorem expect_partition (s : Finset Ω) (f : Ω → ℝ) :
    (𝔼 x, f x) =
      (s.card : ℝ) / Fintype.card Ω * s.expect f +
      ((Finset.univ \ s).card : ℝ) / Fintype.card Ω *
        (Finset.univ \ s).expect f := by
…

theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.abs_expect_sub_restrict_le line 496
Source documentation
Conditioning a bounded function changes its expectation by at most the discarded probability mass. No independence assumption is used here.
```
theorem abs_expect_sub_restrict_le [Nonempty Ω] (s : Finset Ω) (f : Ω → ℝ)
    (hf0 : ∀ x, 0 ≤ f x) (hf1 : ∀ x, f x ≤ 1) :
    |(𝔼 x, f x) - s.expect f| ≤
      ((Finset.univ \ s).card : ℝ) / Fintype.card Ω := by
…
```
abbrev OAI.MaxCutGames.Inverse.KMSBasisComparison.Functional line 537
instance OAI.MaxCutGames.Inverse.KMSBasisComparison.functionalFinite line 539
instance OAI.MaxCutGames.Inverse.KMSBasisComparison.functionalFintype line 543
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.card_functional line 545
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.card_ambient line 552
def OAI.MaxCutGames.Inverse.KMSBasisComparison.goodParameters line 556
Source documentation
Actual good pairs in the unconditioned product sample space.
```
def goodParameters {n ell : ℕ} (X : BasisMap n ell) :
    Finset (Functional ell × KMS.Ambient n) :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.Functional, OAI.MaxCutGames.Inverse.KMS.Ambient
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.mem_goodParameters line 561
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.card_range line 566
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.card_goodParameters line 572
Source documentation
The exact good-event count, including the zero-dimensional boundary.
```
theorem card_goodParameters {n ell : ℕ} (X : BasisMap n ell)
    (hX : Function.Injective X) :
    (goodParameters X).card = (2 ^ ell - 1) * (2 ^ n - 2 ^ ell) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.goodParameters
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.badParameters_mass_le line 587
Source documentation
Exceptional mass is bounded by the sum of the two factor exceptions.
```
theorem badParameters_mass_le {n ell : ℕ} (X : BasisMap n ell)
    (hX : Function.Injective X) :
    1 - ((goodParameters X).card : ℝ) /
        Fintype.card (Functional ell × KMS.Ambient n) ≤
      ((2 : ℝ) ^ ell)⁻¹ + (2 : ℝ) ^ ell / (2 : ℝ) ^ n := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.goodParameters, OAI.MaxCutGames.Inverse.KMSBasisComparison.Functional, OAI.MaxCutGames.Inverse.KMS.Ambient
theorem OAI.MaxCutGames.Inverse.KMSBasisComparison.badParameters_mass_le_compl line 605
Source documentation
The same estimate in the complement-cardinality form used for deleting the bad event from a finite expectation.
```
theorem badParameters_mass_le_compl {n ell : ℕ} (X : BasisMap n ell)
    (hX : Function.Injective X) :
    (((Finset.univ \ goodParameters X).card : ℕ) : ℝ) /
        Fintype.card (Functional ell × KMS.Ambient n) ≤
      ((2 : ℝ) ^ ell)⁻¹ + (2 : ℝ) ^ ell / (2 : ℝ) ^ n := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisComparison.BasisMap, OAI.MaxCutGames.Inverse.KMSBasisComparison.goodParameters, OAI.MaxCutGames.Inverse.KMSBasisComparison.Functional, OAI.MaxCutGames.Inverse.KMS.Ambient
abbrev OAI.MaxCutGames.Inverse.MatrixChart.Lines line 632
Source documentation
One-dimensional vector subspaces.
```
abbrev Lines (K E : Type*) [Field K] [AddCommGroup E] [Module K E] :=
…
```
abbrev OAI.MaxCutGames.Inverse.MatrixChart.Hyperplanes line 636
Source documentation
Hyperplanes, expressed without truncated dimension subtraction.
```
abbrev Hyperplanes (K E : Type*) [Field K] [AddCommGroup E] [Module K E] :=
…
```
def OAI.MaxCutGames.Inverse.MatrixChart.hyperplanesEquivDualLines line 640
Source documentation
Dual annihilation bijects hyperplanes with lines in the dual space.
```
noncomputable def hyperplanesEquivDualLines [FiniteDimensional K E] :
    Hyperplanes K E ≃ Lines K (Module.Dual K E) where
…
```
Mentions: OAI.MaxCutGames.Inverse.MatrixChart.Hyperplanes, OAI.MaxCutGames.Inverse.MatrixChart.Lines
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_lines_binary line 657
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_hyperplanes_binary line 689
theorem OAI.MaxCutGames.Inverse.MatrixChart.finrank_map_mkQ_add line 696
Source documentation
A dimension identity for the quotient correspondence, retaining addition.
```
theorem finrank_map_mkQ_add [FiniteDimensional K E]
    (H W : Submodule K E) (hHW : H ≤ W) :
    finrank K (W.map H.mkQ) + finrank K H = finrank K W := by
…
```
abbrev OAI.MaxCutGames.Inverse.MatrixChart.Extensions line 708
Source documentation
One-dimensional extensions of a subspace.
```
abbrev Extensions (H : Submodule K E) :=
…
```
def OAI.MaxCutGames.Inverse.MatrixChart.extensionsEquivLines line 712
Source documentation
The quotient correspondence identifies extensions with quotient lines.
```
noncomputable def extensionsEquivLines [FiniteDimensional K E]
    (H : Submodule K E) : Extensions H ≃ Lines K (E ⧸ H) where
…
```
Mentions: OAI.MaxCutGames.Inverse.MatrixChart.Extensions, OAI.MaxCutGames.Inverse.MatrixChart.Lines
theorem OAI.MaxCutGames.Inverse.MatrixChart.card_extensions_binary line 732