OAI/NumberTheory/Ostmann/Construction/HistorySmoothBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.sqrt_ratio_le_exp line 9
2. def OAI.Ostmann.HistorySmoothData.ModuliBound line 32

   Source documentation

   Leaf moduli obey the bound forced by the giant and sum-bin cutoffs. Internal cutoff factors are at most one in modulus.

   def HistorySmoothData.ModuliBound (X Δ C : ℝ) : {n : ℕ} → HistorySmoothData n → Prop
     | _, .leaf M _ cutoff => 0 < M ∧ X * Real.exp (Δ - C) ≤ M ∧ |cutoff| ≤ 1
     | _, .node cutoff left right =>
       |cutoff| ≤ 1 ∧ left.ModuliBound X Δ C ∧ right.ModuliBound X Δ C

   Mentions: OAI.Ostmann.HistorySmoothData

3. theorem OAI.Ostmann.HistorySmoothData.bounded_of_moduli line 37
4. theorem OAI.Ostmann.smooth_history_pair_exp_le line 49
5. theorem OAI.Ostmann.full_smooth_factor_exp_le line 65

   Source documentation

   The optional Archimedean multiplier contributes only its fixed exponential bound to Xi.

   theorem full_smooth_factor_exp_le {n : ℕ} (h₁ h₂ : HistorySmoothData n)
       (X Δ C K κ : ℝ) (ψhat : ℝ → ℂ) (A : ℂ)
       (hψ : ∀ t, ‖ψhat t‖ ≤ Real.exp K) (hA : ‖A‖ ≤ Real.exp κ)
       (hh₁ : h₁.ModuliBound X Δ C) (hh₂ : h₂.ModuliBound X Δ C) :
       ‖A * (h₁.value X ψhat * star (h₂.value X ψhat))‖ ≤
         Real.exp (-(2 ^ n : ℕ) * Δ + ((2 ^ n : ℕ) * (C + 2 * K) + κ)) := by
   …

   Mentions: OAI.Ostmann.HistorySmoothData