KMSAnalyticHybridEnergyLemmas.lean`

51 declarations, 0 contain sorry, 0 declared as axioms

The actual arbitrary-subspace hybrid energy estimate. The proof changes both ambient spaces to complement coordinates, invokes the proved image decomposition, and obtains every mixed slice from the actual KMS mixed restriction theorem. No derivative or moment estimate is assumed.

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.productMixedSliceBound_of_uniform line 47
Source documentation
Each image-adapted slice in the product proof is one of the actual uniform mixed slices. The dimension equality exactly matches its weight.
```
theorem productMixedSliceBound_of_uniform (i : ℕ) (L : ℝ)
    (f : ((A × U) →ₗ[F2] (B × C)) → ℝ)
    (hMixed : UniformMixedBound i L f)
    (ho : Module.finrank F2 A + Module.finrank F2 C ≤ i)
    (T : (A × U) →ₗ[F2] (B × C)) : ProductMixedSliceBound i f T L := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.ProductMixedSliceBound
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.map_leftRange_complement line 88
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_energy_le_of_uniform line 103
Source documentation
The actual hybrid derivative is uniformly bounded whenever all actual mixed slices are bounded. Both selector subspaces and every affine translate are arbitrary.
```
theorem hybridDerivative_energy_le_of_uniform
    (i : ℕ) (L : ℝ) (hL : 0 ≤ L)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (hMixed : UniformMixedBound i L f) (hi : i ≤ Module.finrank F2 E)
    (A : Submodule F2 E) (B : Submodule F2 F) (T : E →ₗ[F2] F) :
    (𝔼 N, hybridDerivative A B T (rankComponent i f) N ^ 2) ≤ L := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_energy_bound line 147
Source documentation
Genuine KMS hybrid energy bound from basis invariance and actual local squared density. This is the analytic input to the permitted generic fourth moment inequality; no hybrid estimate is included among its hypotheses.
```
theorem hybridDerivative_energy_bound
    (i : ℕ) (ε : ℝ) (hε : 0 ≤ ε)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (hd : AffineDensityBound i ε f) (hi : i ≤ Module.finrank F2 E)
    (A : Submodule F2 E) (B : Submodule F2 F) (T : E →ₗ[F2] F) :
    (𝔼 N, hybridDerivative A B T (rankComponent i f) N ^ 2) ≤ mixedRankConstant i * ε :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_energy_bound_allRanks line 193

Source documentation

The genuine hybrid derivative bound, including ranks above the ambient dimension where the selected Fourier component vanishes.

theorem hybridDerivative_energy_bound_allRanks
    (i : ℕ) (ε : ℝ) (hε : 0 ≤ ε)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (hd : AffineDensityBound i ε f)
    (A : Submodule F2 E) (B : Submodule F2 F) (T : E →ₗ[F2] F) :
    (𝔼 N, hybridDerivative A B T (rankComponent i f) N ^ 2) ≤ mixedRankConstant i * ε := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant

def OAI.UniqueGamesTheorem.Inverse.KMSMomentConstants.fourthMomentConstant line 222
Source documentation
The constant after the genuine mixed-energy estimate and A5 aggregation.
```
def fourthMomentConstant (r : ℕ) : ℝ := 2 ^ (109 * r * r + 2 * r)
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentConstants.fourthMomentConstant_pos line 224
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentConstants.fourthMomentConstant_nonneg line 228
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentConstants.mixedRankConstant_eq line 232
Source documentation
The closed mixed estimate's literal constant has a quadratic exponent.
```
theorem mixedRankConstant_eq (r : ℕ) :
    mixedRankConstant r = (2 : ℝ) ^ (6 * r * r + 2 * r) := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentConstants.a5_mul_mixedRankConstant line 240
Source documentation
Multiplying by the actual selector-count and A5 constant is exact.
```
theorem a5_mul_mixedRankConstant (r : ℕ) :
    (2 : ℝ) ^ (103 * r * r) * mixedRankConstant r = fourthMomentConstant r := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSMomentConstants.fourthMomentConstant
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentConstants.fourthMomentConstant_mono line 247
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentConstants.a5_mixed_bound line 257
Source documentation
The complete numerical closure, retaining the density and projection energy factors in the order used by the expansion interface.
```
theorem a5_mixed_bound {i r : ℕ} (hi : i ≤ r) (ε η : ℝ)
    (hε : 0 ≤ ε) (hη : 0 ≤ η) :
    (2 : ℝ) ^ (103 * i * i) * (mixedRankConstant i * ε) * η ≤
      fourthMomentConstant r * η * ε := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSMomentConstants.fourthMomentConstant

theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentTheorem.lifted_fourth_moment_bound line 289

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
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSExpansion.kms_expansion line 337
Source documentation
The KMS expansion theorem with constants independent of both dimensions and with the ambient threshold chosen after the plane dimension.
```
theorem kms_expansion : KMS.ExpansionPrinciple := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.ExpansionPrinciple
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureColumnMass.card_affineSlice line 371
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureColumnMass.card_rowFiber line 379
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureColumnMass.card_rowFiber_eq_mul line 388
Source documentation
The exact number of row-fiber points for each compatible specification on the column span. Dependent column equations cost only their actual rank.
```
theorem card_rowFiber_eq_mul (A : K →ₗ[F2] R) (Q : Submodule F2 E)
    (M₀ : E →ₗ[F2] K) :
    Nat.card (RowFiber A (A.comp M₀)) = Nat.card (AffineSlice A Q M₀) *
      2 ^ (Module.finrank F2 Q * Module.finrank F2 A.ker) := by
…
```

theorem OAI.UniqueGamesTheorem.Inverse.RowErasureColumnMass.card_rowFiber_le_mul line 397

Source documentation

A denominator-free bound by the listed column count and ambient output dimension, with no independence or full-rank hypothesis.

theorem card_rowFiber_le_mul (A : K →ₗ[F2] R) (Q : Submodule F2 E)
    (M₀ : E →ₗ[F2] K) (ell r : ℕ)
    (hQ : Module.finrank F2 Q ≤ r) (hK : Module.finrank F2 K ≤ ell) :
    Nat.card (RowFiber A (A.comp M₀)) ≤
      Nat.card (AffineSlice A Q M₀) * 2 ^ (ell * r) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.RowErasureColumnMass.column_fraction_eq line 410

Source documentation

The exact uniform fraction of the row fiber occupied by its compatible affine column slice.

theorem column_fraction_eq (A : K →ₗ[F2] R) (Q : Submodule F2 E)
    (M₀ : E →ₗ[F2] K) :
    (Nat.card (AffineSlice A Q M₀) : ℝ) /
        (Nat.card (RowFiber A (A.comp M₀)) : ℝ) =
      1 / (2 : ℝ) ^ (Module.finrank F2 Q * Module.finrank F2 A.ker) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.RowErasureColumnMass.column_fraction_ge line 424

Source documentation

At most r independent column constraints retain at least the fraction 2^(-ell*r) of any nonempty row-advice fiber.

theorem column_fraction_ge (A : K →ₗ[F2] R) (Q : Submodule F2 E)
    (M₀ : E →ₗ[F2] K) (ell r : ℕ)
    (hQ : Module.finrank F2 Q ≤ r) (hK : Module.finrank F2 K ≤ ell) :
    1 / (2 : ℝ) ^ (ell * r) ≤
      (Nat.card (AffineSlice A Q M₀) : ℝ) /
        (Nat.card (RowFiber A (A.comp M₀)) : ℝ) := by
…

def OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.rowFiber line 458
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.mem_rowFiber line 462
def OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.rowOnly line 467
Source documentation
Forget only the column equations of a slice.
```
def rowOnly {ell m : ℕ} (S : Slice ell m) : Slice ell m where
…
```
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.rowOnly_contains_iff line 475
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.rowOnly_points line 488
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.contains_rowOnly line 494
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.rowOnly_columnSpan line 498
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.rowOnly_quotient_finrank line 504
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.rowFiber_card line 516
Source documentation
The size of an actual nonempty row fiber, in the same coordinates used by the selector's uniform matrix sample.
```
theorem rowFiber_card {ell m : ℕ} (S : Slice ell m) (M₀ : Mat ell m)
    (h₀ : S.Contains M₀) :
    (rowFiber S.rowCoefficient S.rowValue).card =
      2 ^ (m * Module.finrank F2 S.rowMap.ker) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.rowFiber
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.rowFiber_nonempty line 525
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.column_fraction_ge line 535
Source documentation
The chosen nonempty column event has the required mass inside its actual row-advice fiber. The target coefficient and intercept do not affect its size.
```
theorem column_fraction_ge {ell m r : ℕ} (d : Description ell m r)
    (hne : d.toSlice.points.Nonempty) :
    1 / (2 : ℝ) ^ (ell * r) ≤
      (d.toSlice.points.card : ℝ) / ((rowFiber d.1 d.2.1).card : ℝ) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureDescriptionColumnMass.rowFiber
def OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedPoints line 578
def OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedHit line 584
theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedPoints_of_good line 588
theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedHit_of_good line 595
theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedPoints_support line 608
theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedEvent_iff_points line 622
theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedMatch_iff_points line 638
theorem OAI.UniqueGamesTheorem.Inverse.RowErasure.SliceFamily.selectedPoints_match_sum line 656
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selectedPoints_column_mass line 685
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selected_event_mass_ge line 702
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selected_match_mass_ge line 729
def OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selectedEventMass line 753
def OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selectedMatchMass line 756
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selectedEventMass_ge line 759
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selectedMatchMass_ge line 772
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selectedEventMass_weighted_ge line 781
Source documentation
Context weights may be the pushforward of verifier seeds and need not be uniform on distinct questions. Normalization is not needed for this inequality.
```
theorem selectedEventMass_weighted_ge {Q : Type*} [Fintype Q]
    (w : Q → ℝ) (hw : ∀ q, 0 ≤ w q) (f : Q → Mat ell m → Vector ell)
    (α g₀ : ℝ)
    (hgood : g₀ ≤ ∑ q, w q * adviceMass ((family ell m r).goodAt (f q) α)) :
    (1 / (2 : ℝ) ^ (ell * r)) * g₀ ≤ ∑ q, w q * selectedEventMass r (f q) α := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.family, OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selectedEventMass
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selectedMatchMass_weighted_ge line 799
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selectedMatchMass_conditional_ge line 813
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selectedEventMass_contextual_ge line 821
Source documentation
The same bound for a uniform finite seed space, allowing repeated contexts.
```
theorem selectedEventMass_contextual_ge {Q : Type*} [Fintype Q]
    (f : Q → Mat ell m → Vector ell) (α g₀ : ℝ)
    (hgood : g₀ ≤ 𝔼 q, adviceMass ((family ell m r).goodAt (f q) α)) :
    (1 / (2 : ℝ) ^ (ell * r)) * g₀ ≤ 𝔼 q, selectedEventMass r (f q) α := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.family, OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selectedEventMass
theorem OAI.UniqueGamesTheorem.Inverse.RowErasureMatrix.selectedMatchMass_contextual_ge line 830