OAI/Computability/MaxCut/PCP/Parity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Fourier.Parity.finiteSum line 8
2. theorem OAI.MaxCutGames.Fourier.Parity.finiteSum_le line 13
3. theorem OAI.MaxCutGames.Fourier.Parity.finiteSum_split line 24
4. theorem OAI.MaxCutGames.Fourier.Parity.nonzero_sum_gt_half line 35
5. theorem OAI.MaxCutGames.Fourier.Parity.signed_le_abs line 43
6. theorem OAI.MaxCutGames.Fourier.Parity.coefficient_of_bounds line 52

   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.MaxCutGames.Fourier.Parity.finiteSum

7. theorem OAI.MaxCutGames.Fourier.Parity.coefficient_gt_half_div line 89

   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.MaxCutGames.Fourier.Parity.finiteSum

8. theorem OAI.MaxCutGames.Fourier.Parity.div_div_eq line 110
9. theorem OAI.MaxCutGames.Fourier.Parity.lemma53_arithmetic line 114