ParityLemmas.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Actual splitting of linear-map questions and their uniform laws.

def OAI.UniqueGamesTheorem.Fourier.Parity.finiteSum line 11
theorem OAI.UniqueGamesTheorem.Fourier.Parity.finiteSum_le line 16
theorem OAI.UniqueGamesTheorem.Fourier.Parity.finiteSum_split line 27
theorem OAI.UniqueGamesTheorem.Fourier.Parity.nonzero_sum_gt_half line 38
theorem OAI.UniqueGamesTheorem.Fourier.Parity.signed_le_abs line 46

theorem OAI.UniqueGamesTheorem.Fourier.Parity.coefficient_of_bounds line 55

Source documentation

A finite signed sum with large total and small parity-zero subtotal has a large coefficient at an index of nonzero parity. indices may overcount: only its length bound is used, so duplicate freedom is unnecessary here.

theorem coefficient_of_bounds {ι : Type} (indices : List ι)
    (coefficient character : ι → Rat) (zeroParity : ι → Bool)
    (ρ bound : Rat) (N : Nat)
    (bound_nonneg : 0 ≤ bound)
    (length_bound : indices.length ≤ N)
    (budget : (N : Rat) * bound ≤ ρ / 2)
    (sign : ∀ i ∈ indices, character i = 1 ∨ character i = -1)
    (dense : ρ < finiteSum indices (fun i => coefficient i * character i))
    (zero_bound : finiteSum indices (fun i =>
      if zeroParity i then coefficient i * character i else 0) ≤ ρ / 2) :
    ∃ i ∈ indices, zeroParity i = false ∧ bound < (coefficient i).abs := by
…

Mentions: OAI.UniqueGamesTheorem.Fourier.Parity.finiteSum

theorem OAI.UniqueGamesTheorem.Fourier.Parity.coefficient_gt_half_div line 92

Source documentation

The exact threshold in Lemma 5.3 before substituting N = 2^(r*s). The displayed nested fraction is (ρ / 2) / N, hence ρ / (2*N).

theorem coefficient_gt_half_div {ι : Type} (indices : List ι)
    (coefficient character : ι → Rat) (zeroParity : ι → Bool)
    (ρ : Rat) (N : Nat)
    (ρ_pos : 0 < ρ) (N_pos : 0 < N)
    (length_bound : indices.length ≤ N)
    (sign : ∀ i ∈ indices, character i = 1 ∨ character i = -1)
    (dense : ρ < finiteSum indices (fun i => coefficient i * character i))
    (zero_bound : finiteSum indices (fun i =>
      if zeroParity i then coefficient i * character i else 0) ≤ ρ / 2) :
    ∃ i ∈ indices, zeroParity i = false ∧
      (ρ / 2) / (N : Rat) < (coefficient i).abs := by
…

Mentions: OAI.UniqueGamesTheorem.Fourier.Parity.finiteSum

theorem OAI.UniqueGamesTheorem.Fourier.Parity.div_div_eq line 113
theorem OAI.UniqueGamesTheorem.Fourier.Parity.lemma53_arithmetic line 117
def OAI.UniqueGamesTheorem.Fourier.SplitMaps.codomainSplit line 153
Source documentation
A question into the symbol/perpendicular product is exactly a pair of independent coordinate questions.
```
def codomainSplit : (E →ₗ[K] C × D) ≃ₗ[K] (E →ₗ[K] C) × (E →ₗ[K] D) :=
…
```
def OAI.UniqueGamesTheorem.Fourier.SplitMaps.domainSplit line 157
Source documentation
A dual Fourier index on a product is exactly its two restrictions.
```
def domainSplit : (C × D →ₗ[K] E) ≃ₗ[K] (C →ₗ[K] E) × (D →ₗ[K] E) :=
…
```
theorem OAI.UniqueGamesTheorem.Fourier.SplitMaps.codomainSplit_symm_apply line 160
theorem OAI.UniqueGamesTheorem.Fourier.SplitMaps.domainSplit_symm_apply line 163
theorem OAI.UniqueGamesTheorem.Fourier.SplitMaps.expect_codomain_product line 166
theorem OAI.UniqueGamesTheorem.Fourier.SplitMaps.expect_domain_product line 176
theorem OAI.UniqueGamesTheorem.Fourier.SplitMaps.sum_domain_product line 188