OAI/Analysis/Littlewood/AlmostSign.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AsymptoticallyMinimalLittlewood.almost_sign_sampler line 12

   Source documentation

   The almost-sign sampling conclusion from the auxiliary packet and its packed signed curvature intervals. Every datum is fixed before the variable N.

   theorem almost_sign_sampler {δ : ℝ} (hδ : 0<δ) (hδ20 : δ<1/20) :
       ∃ X : (N : ℕ) → Fin N → ℝ, ∃ L C : ℝ,
         0≤C ∧ 1-7*δ≤L ∧
         (∀ N : ℕ, 1≤N → ∀ k, |X N k|≤1) ∧
         Tendsto (fun N : ℕ ↦ (∑ k : Fin N, (X N k)^2)/(N : ℝ)) atTop (𝓝 L) ∧
         ∀ N : ℕ, 1≤N → ∀ t∈Set.Icc (0:ℝ) 1,
           ‖(1/(Real.sqrt N : ℂ))*∑ k : Fin N, (X N k : ℂ)*realPhase (2*Real.pi*t*k)‖≤
             Real.sqrt ((1+δ)^3/(1-δ))+C/N := by
   …

   Mentions: OAI.AsymptoticallyMinimalLittlewood.realPhase