OAI/NumberTheory/Ostmann/Arithmetic/BulkLogContinuity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.bulkLogValues line 11
2. theorem OAI.Ostmann.bulkLogValues_update line 14
3. theorem OAI.Ostmann.bulkLogValues_nat line 24
4. theorem OAI.Ostmann.realValueSmoothWeight_bulkLog_nat line 36

   Source documentation

   At every original prime tuple this real extension is exactly the original moving-tree weight, including points where one of the node cutoffs vanishes.

   theorem realValueSmoothWeight_bulkLog_nat {σ : Type*}
       (base sample : σ → ℕ) (S : Finset σ) (hp : ∀ i ∈ S, 0 < sample i)
       {n : ℕ} (T : MovingSlotData σ n) (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ)
       (hlo : 1 ≤ lo) (hhi : lo ≤ hi) (φ : ℝ → ℝ) (G : ℕ → ℝ) (L R : ℝ) :
       realValueSmoothWeight (bulkLogValues (fun i => (base i : ℝ)) S
         (fun i => Real.log (sample i))) T ψ X lo hi hlo hhi φ G L R =
           movingRealSmoothWeight (fun i => if i ∈ S then sample i else base i)
             T ψ X lo hi hlo hhi φ G L R := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.realValueSmoothWeight, OAI.Ostmann.bulkLogValues, OAI.Ostmann.movingRealSmoothWeight

5. theorem OAI.Ostmann.continuous_bulkLogValues line 46
6. theorem OAI.Ostmann.continuous_realSlotProduct line 53
7. theorem OAI.Ostmann.realSlotProduct_bulkLogValues line 60
8. theorem OAI.Ostmann.MovingSlotReversal.continuous_bulkLogPivot line 69
9. theorem OAI.Ostmann.MovingSlotData.continuous_bulkLogLeafModuli line 83
10. theorem OAI.Ostmann.continuous_bulkLogFourierWeight line 98
11. theorem OAI.Ostmann.continuous_bulkLogNodeCutoff line 113
12. theorem OAI.Ostmann.continuous_bulkLogSmoothWeight line 133
13. theorem OAI.Ostmann.realValueSmoothWeight_norm line 146

    Source documentation

    The bound is uniform in all real bulk variables and both giant arguments.

    theorem realValueSmoothWeight_norm {σ : Type*} (value : σ → ℝ) (i : σ)
        {n : ℕ} (T : MovingSlotData σ n) (hT : T.CompensationAbsent i)
        (ψ : 𝓢(ℝ, ℂ)) (X lo hi V : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
        (hV : T.Frequencies (fun s => |(s : ℝ)| ≤ V))
        (φ : ℝ → ℝ) (G : ℕ → ℝ) (B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
        (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|)
        (hout : ∀ x, 1 ≤ |x| → φ x = 0) (L R : ℝ) :
        ‖realValueSmoothWeight value T ψ X lo hi hlo hhi φ G L R‖ ≤
          movingFourierVariationBudget ψ V lo hi n * (2 * B + D * (Real.exp 2 - 1)) ^ (2 ^ n - 1) := by
    …

    Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.realValueSmoothWeight, OAI.Ostmann.movingFourierVariationBudget

14. def OAI.Ostmann.bulkLogSmoothFunction line 162