Deletion.lean`

55 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MaxCutGames.Fourier.Deletion.trueCount line 11

Source documentation

The number of entries on which a Boolean function is true.

def trueCount {Ω : Type u} (f : Ω → Bool) : List Ω → Nat
  | [] => 0
  | x :: xs => (if f x then 1 else 0) + trueCount f xs

theorem OAI.MaxCutGames.Fourier.Deletion.trueCount_mono line 15
theorem OAI.MaxCutGames.Fourier.Deletion.trueCount_eq_zero line 27
structure OAI.MaxCutGames.Fourier.Deletion.RestrictionSystem line 39
Source documentation
A family of admissible restrictions and their containing rows. Rows may overlap, and there is no requirement that different restrictions share the same ancillary data.
```
structure RestrictionSystem (Ω : Type u) (Row : Type v) (Witness : Type w) where
…
```
def OAI.MaxCutGames.Fourier.Deletion.Dense line 50
Source documentation
Strict density above the rational threshold p / q when q > 0.
```
def Dense (S : RestrictionSystem Ω Row Witness) (H : Ω → Bool)
    (p q : Nat) (t : Witness) : Prop :=
…
```
Mentions: OAI.MaxCutGames.Fourier.Deletion.RestrictionSystem
def OAI.MaxCutGames.Fourier.Deletion.BadRow line 55
Source documentation
A row is bad when it contains a dense admissible restriction.
```
def BadRow (S : RestrictionSystem Ω Row Witness) (H : Ω → Bool)
    (p q : Nat) (r : Row) : Prop :=
…
```
Mentions: OAI.MaxCutGames.Fourier.Deletion.RestrictionSystem
def OAI.MaxCutGames.Fourier.Deletion.DeletedSet line 60
Source documentation
All points of every bad row are removed.
```
def DeletedSet (S : RestrictionSystem Ω Row Witness) (H : Ω → Bool)
    (p q : Nat) (x : Ω) : Prop :=
…
```
Mentions: OAI.MaxCutGames.Fourier.Deletion.RestrictionSystem
def OAI.MaxCutGames.Fourier.Deletion.remainder line 65
Source documentation
The Boolean remainder after deleting the union of bad rows.
```
noncomputable def remainder (S : RestrictionSystem Ω Row Witness)
    (H : Ω → Bool) (p q : Nat) (x : Ω) : Bool := by
…
```
Mentions: OAI.MaxCutGames.Fourier.Deletion.RestrictionSystem
def OAI.MaxCutGames.Fourier.Deletion.removed line 71
Source documentation
The Boolean part removed from the original function.
```
noncomputable def removed (S : RestrictionSystem Ω Row Witness)
    (H : Ω → Bool) (p q : Nat) (x : Ω) : Bool := by
…
```
Mentions: OAI.MaxCutGames.Fourier.Deletion.RestrictionSystem
theorem OAI.MaxCutGames.Fourier.Deletion.remainder_le_original line 76
theorem OAI.MaxCutGames.Fourier.Deletion.dense_deletes_whole_row line 87
Source documentation
A dense restriction makes its whole row bad, including points that were not sampled by the restriction.
```
theorem dense_deletes_whole_row (S : RestrictionSystem Ω Row Witness)
    (H : Ω → Bool) (p q : Nat) (t : Witness)
    (ha : S.admissible t) (hd : Dense S H p q t)
    (x : Ω) (hx : S.row (S.containingRow t) x) :
    remainder S H p q x = false := by
…
```
Mentions: OAI.MaxCutGames.Fourier.Deletion.RestrictionSystem, OAI.MaxCutGames.Fourier.Deletion.Dense, OAI.MaxCutGames.Fourier.Deletion.remainder
theorem OAI.MaxCutGames.Fourier.Deletion.dense_restriction_remainder_zero line 97
def OAI.MaxCutGames.Fourier.Deletion.RestrictionGlobal line 106
Source documentation
Rational restriction globality of a Boolean function.
```
def RestrictionGlobal (S : RestrictionSystem Ω Row Witness) (G : Ω → Bool)
    (p q : Nat) : Prop :=
…
```
Mentions: OAI.MaxCutGames.Fourier.Deletion.RestrictionSystem
theorem OAI.MaxCutGames.Fourier.Deletion.remainder_restrictionGlobal line 112
Source documentation
Whole-row deletion establishes every admissible restriction bound. This is the first assertion of Lemma 5.2, before applying Fourier estimates.
```
theorem remainder_restrictionGlobal
    (S : RestrictionSystem Ω Row Witness) (H : Ω → Bool) (p q : Nat) :
    RestrictionGlobal S (remainder S H p q) p q := by
…
```
Mentions: OAI.MaxCutGames.Fourier.Deletion.RestrictionSystem, OAI.MaxCutGames.Fourier.Deletion.RestrictionGlobal, OAI.MaxCutGames.Fourier.Deletion.remainder
theorem OAI.MaxCutGames.Fourier.Deletion.boolean_partition line 128
Source documentation
Retained and removed contributions form a disjoint Boolean partition.
```
theorem boolean_partition (S : RestrictionSystem Ω Row Witness)
    (H : Ω → Bool) (p q : Nat) (x : Ω) :
    (remainder S H p q x || removed S H p q x) = H x ∧
    (remainder S H p q x && removed S H p q x) = false := by
…
```
Mentions: OAI.MaxCutGames.Fourier.Deletion.RestrictionSystem, OAI.MaxCutGames.Fourier.Deletion.remainder, OAI.MaxCutGames.Fourier.Deletion.removed
theorem OAI.MaxCutGames.Fourier.Deletion.trueCount_partition line 136
Source documentation
Exact conservation of retained and removed mass on any sampling list.
```
theorem trueCount_partition (S : RestrictionSystem Ω Row Witness)
    (H : Ω → Bool) (p q : Nat) (xs : List Ω) :
    trueCount H xs = trueCount (remainder S H p q) xs +
      trueCount (removed S H p q) xs := by
…
```
Mentions: OAI.MaxCutGames.Fourier.Deletion.RestrictionSystem, OAI.MaxCutGames.Fourier.Deletion.trueCount, OAI.MaxCutGames.Fourier.Deletion.remainder, OAI.MaxCutGames.Fourier.Deletion.removed
abbrev OAI.MaxCutGames.Fourier.MatrixRestrictions.Ambient line 159
abbrev OAI.MaxCutGames.Fourier.MatrixRestrictions.Parameter line 163
def OAI.MaxCutGames.Fourier.MatrixRestrictions.embed line 167
Source documentation
The canonical inclusion of L(E/W,C') into L(E,C).
```
def embed (W : Submodule F2 E)
    (C' : Submodule F2 C) (A : Parameter W C') : (E →ₗ[F2] C) :=
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.Parameter
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.embed_apply line 171
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.embed_injective line 175
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.embed_vanishes line 184
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.embed_range line 192
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.exists_embed_iff line 199
Source documentation
These are exactly the maps vanishing on W with image in C'.
```
theorem exists_embed_iff (W : Submodule F2 E)
    (C' : Submodule F2 C) (B : (E →ₗ[F2] C)) :
    (∃ A : Parameter W C', embed W C' A = B) ↔
      W ≤ LinearMap.ker B ∧ LinearMap.range B ≤ C' := by
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.Parameter, OAI.MaxCutGames.Fourier.MatrixRestrictions.embed
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.quotient_embed_zero line 219
Source documentation
Quotient rows are unchanged by every admissible restriction perturbation.
```
theorem quotient_embed_zero (W : Submodule F2 E)
    (C' : Submodule F2 C) (A : Parameter W C') :
    C'.mkQ.comp (embed W C' A) = 0 := by
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.Parameter, OAI.MaxCutGames.Fourier.MatrixRestrictions.embed
def OAI.MaxCutGames.Fourier.MatrixRestrictions.translate line 227
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.translate_injective line 231
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.quotient_translate line 237
def OAI.MaxCutGames.Fourier.MatrixRestrictions.embedding line 251
Source documentation
The perturbation inclusion is itself a binary linear map.
```
def embedding (W : Submodule F2 E) (C' : Submodule F2 C) :
    Parameter W C' →ₗ[F2] (E →ₗ[F2] C) where
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.Parameter
def OAI.MaxCutGames.Fourier.MatrixRestrictions.order line 263
def OAI.MaxCutGames.Fourier.MatrixRestrictions.restrict line 267
Source documentation
Restrict a real observable to the actual affine quotient-map domain.
```
def restrict (f : (E →ₗ[F2] C) → ℝ) (W : Submodule F2 E)
    (C' : Submodule F2 C) (X : E →ₗ[F2] C) : Parameter W C' → ℝ :=
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.Parameter
instance OAI.MaxCutGames.Fourier.MatrixRestrictions.parameterFintype line 271
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.parameter_card_pos line 280
Source documentation
Every actual restriction domain has at least its zero map.
```
theorem parameter_card_pos [Finite E] [Finite C]
    (W : Submodule F2 E) (C' : Submodule F2 C) :
    0 < Fintype.card (Parameter W C') := Fintype.card_pos
```
Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.Parameter
structure OAI.MaxCutGames.Fourier.MatrixRestrictions.Row line 285
Source documentation
An actual row includes its target subspace as part of its index.
```
structure Row (E C : Type*) [AddCommGroup E] [Module F2 E]
    [AddCommGroup C] [Module F2 C] where
…
```
structure OAI.MaxCutGames.Fourier.MatrixRestrictions.Witness line 290
def OAI.MaxCutGames.Fourier.MatrixRestrictions.samples line 296
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.samples_length line 301
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.samples_nonempty line 305
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.mem_samples_iff line 312
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.samples_nodup line 319
def OAI.MaxCutGames.Fourier.MatrixRestrictions.system line 326
Source documentation
Actual affine matrix restrictions instantiate the generic deletion interface.
```
noncomputable def system [Finite E] [Finite C] (r : Nat) :
    Deletion.RestrictionSystem (E →ₗ[F2] C) (Row E C) (Witness E C) where
…
```
Mentions: OAI.MaxCutGames.Fourier.Deletion.RestrictionSystem, OAI.MaxCutGames.Fourier.MatrixRestrictions.Row, OAI.MaxCutGames.Fourier.MatrixRestrictions.Witness
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.remainder_restriction_count line 339
Source documentation
Every actual affine restriction of order at most r obeys the residual count bound after whole-row deletion. No linear containment assumption remains.
```
theorem remainder_restriction_count [Finite E] [Finite C]
    (H : (E →ₗ[F2] C) → Bool) (r p q : Nat) (t : Witness E C)
    (ht : order t.vanishing t.target ≤ r) :
    q * Deletion.trueCount (Deletion.remainder (system r) H p q) (samples t) ≤
      p * Fintype.card (Parameter t.vanishing t.target) := by
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.Witness, OAI.MaxCutGames.Fourier.MatrixRestrictions.order, OAI.MaxCutGames.Fourier.Deletion.trueCount, OAI.MaxCutGames.Fourier.Deletion.remainder, OAI.MaxCutGames.Fourier.MatrixRestrictions.system, OAI.MaxCutGames.Fourier.MatrixRestrictions.samples, OAI.MaxCutGames.Fourier.MatrixRestrictions.Parameter
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.trueCount_eq_countP_inline_MatrixRestrictions line 347
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.samples_trueCount line 355
Source documentation
Exact numerator for uniform sampling of the actual affine restriction.
```
theorem samples_trueCount [Finite E] [Finite C] (H : (E →ₗ[F2] C) → Bool)
    (t : Witness E C) :
    Deletion.trueCount H (samples t) =
      (Finset.univ.filter fun A : Parameter t.vanishing t.target =>
        H (translate t.vanishing t.target t.base A) = true).card := by
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.Witness, OAI.MaxCutGames.Fourier.Deletion.trueCount, OAI.MaxCutGames.Fourier.MatrixRestrictions.samples, OAI.MaxCutGames.Fourier.MatrixRestrictions.Parameter, OAI.MaxCutGames.Fourier.MatrixRestrictions.translate
def OAI.MaxCutGames.Fourier.MatrixRestrictions.density line 368
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.density_eq_count_div line 373
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.dense_iff_lt_density line 381
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.remainder_restriction_density line 397
Source documentation
Whole-row deletion gives the normalized real restriction bound on every actual affine restriction of the permitted dimension and codimension.
```
theorem remainder_restriction_density [Finite E] [Finite C]
    (H : (E →ₗ[F2] C) → Bool) (r p q : Nat) (hq : 0 < q)
    (t : Witness E C) (ht : order t.vanishing t.target ≤ r) :
    density (Deletion.remainder (system r) H p q) t ≤ (p : ℝ) / q := by
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.Witness, OAI.MaxCutGames.Fourier.MatrixRestrictions.order, OAI.MaxCutGames.Fourier.MatrixRestrictions.density, OAI.MaxCutGames.Fourier.Deletion.remainder, OAI.MaxCutGames.Fourier.MatrixRestrictions.system
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.remainder_restriction_sq_expect line 414
Source documentation
The same bound expressed as the squared normalized real L² norm. This is the restriction-global hypothesis used by the Fourier level theorem.
```
theorem remainder_restriction_sq_expect [Finite E] [Finite C]
    (H : (E →ₗ[F2] C) → Bool) (r p q : Nat) (hq : 0 < q)
    (W : Submodule F2 E) (C' : Submodule F2 C)
    (horder : order W C' ≤ r) (X : E →ₗ[F2] C) :
    (𝔼 A : Parameter W C',
      (restrict (fun Y => if Deletion.remainder (system r) H p q Y
        then (1 : ℝ) else 0) W C' X A) ^ 2) ≤ (p : ℝ) / q := by
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.order, OAI.MaxCutGames.Fourier.MatrixRestrictions.Parameter, OAI.MaxCutGames.Fourier.MatrixRestrictions.restrict, OAI.MaxCutGames.Fourier.Deletion.remainder, OAI.MaxCutGames.Fourier.MatrixRestrictions.system
def OAI.MaxCutGames.Fourier.MatrixRestrictions.quotientKernelEquiv line 434
Source documentation
A dual map killed by the quotient has a unique factor with values in W. This is the exact finite object counted in the parity argument of Lemma 5.3.
```
def quotientKernelEquiv (W : Submodule F2 E) :
    {T : C →ₗ[F2] E // W.mkQ.comp T = 0} ≃ (C →ₗ[F2] W) where
…
```
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.quotientKernel_card line 453
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.quotientKernel_filter_card line 461
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.deletedSet_iff_exists_target line 471
Source documentation
Every deleted point determines its row once the target subspace is fixed. Thus the union bound ranges over target subspaces, not over row values.
```
theorem deletedSet_iff_exists_target [Finite E] [Finite C]
    (H : (E →ₗ[F2] C) → Bool) (r p q : Nat) (X : E →ₗ[F2] C) :
    Deletion.DeletedSet (system r) H p q X ↔
      ∃ C' : Submodule F2 C,
        Deletion.BadRow (system r) H p q ⟨C', C'.mkQ.comp X⟩ := by
…
```
Mentions: OAI.MaxCutGames.Fourier.Deletion.DeletedSet, OAI.MaxCutGames.Fourier.MatrixRestrictions.system, OAI.MaxCutGames.Fourier.Deletion.BadRow
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.badRow_codim_le line 484
theorem OAI.MaxCutGames.Fourier.MatrixRestrictions.deletedSet_iff_exists_admissible_target line 495