OAI/Analysis/Littlewood/Main.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AsymptoticallyMinimalLittlewood.unitCircle_parameter line 8
2. lemma OAI.AsymptoticallyMinimalLittlewood.littlewood_phase line 22
3. lemma OAI.AsymptoticallyMinimalLittlewood.entropy_small_defect line 41
4. lemma OAI.AsymptoticallyMinimalLittlewood.small_delta_budget line 74
5. lemma OAI.AsymptoticallyMinimalLittlewood.defect_from_energy line 111
6. lemma OAI.AsymptoticallyMinimalLittlewood.round_sample_once line 132

   Source documentation

   At a fixed positive length, energy and the full-circle relaxed bound imply an actual real signing with the stated normalized error.

   lemma round_sample_once {N : ℕ} (hN : 1≤N) {δ K C : ℝ}
       (hδ : 0<δ) (hδ20 : δ<1/20) (X : Fin N → ℝ)
       (hX : ∀ k, |X k|≤1)
       (hE : (1-8*δ)*(N : ℝ)≤∑ k, (X k)^2)
       (hmax : ∀ t∈Set.Icc (0:ℝ) 1,
         ‖(1/(Real.sqrt N : ℂ))*∑ k : Fin N, (X k : ℂ)*realPhase (2*Real.pi*t*k)‖≤K+C/N) :
       ∃ ε : Fin N → ℝ, IsRealSigning ε ∧ ∀ z : ℂ, ‖z‖=1 →
         ‖littlewoodValue ε z‖/Real.sqrt N≤
           K+C/N+196608*(1/Real.sqrt N+2*Real.sqrt (δ*Real.log (20/δ))) := by
   …

   Mentions: OAI.AsymptoticallyMinimalLittlewood.realPhase, OAI.AsymptoticallyMinimalLittlewood.IsRealSigning, OAI.AsymptoticallyMinimalLittlewood.littlewoodValue

7. theorem OAI.AsymptoticallyMinimalLittlewood.main line 187

   Distinct definitions of this name: ComparatorChallenges/AsymptoticallyMinimalLittlewood.lean:18 (same statement text; different proof or body). Qualify references as OAI.AsymptoticallyMinimalLittlewood.main@path.