OAI/NumberTheory/Ostmann/Arithmetic/MovingRealKernel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.HistoryFormula.continuous_realEval line 12
2. theorem OAI.Ostmann.WordTransferGuard.isClosed_archimedeanAt line 18
3. theorem OAI.Ostmann.isClosed_movingArchimedeanGate line 24
4. theorem OAI.Ostmann.continuous_topGiantReal line 33
5. theorem OAI.Ostmann.measurable_movingRealGateWeight line 40
6. theorem OAI.Ostmann.movingRealFourierWeight_norm line 55
7. theorem OAI.Ostmann.movingRealNodeCutoff_norm line 74
8. theorem OAI.Ostmann.movingRealSmoothWeight_norm line 98
9. def OAI.Ostmann.movingRealKernel line 108
10. theorem OAI.Ostmann.measurable_movingRealKernel line 114
11. theorem OAI.Ostmann.movingRealKernel_norm line 124
12. theorem OAI.Ostmann.integrable_movingRealKernel line 135
13. theorem OAI.Ostmann.moving_recursive_real_kernel line 150

    Source documentation

    The literal recursive coefficient, including all zero terms, is the fixed residue coefficient times the single bounded real kernel.

    theorem moving_recursive_real_kernel {σ I : Type*} (q : I → ℕ)
        [∀ i, Fact (q i).Prime] (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0)
        (childBound pivotBound : ℕ → ℕ)
        (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
        (E : {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
        (g : ∀ i, ZMod (q i) → ℂ) (hg : ∀ i, g i 0 = 0) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
        (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
        (φ : ℝ → ℝ) (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)
        {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
        (hf : T.Frequencies (· ≠ 0)) (XL XR a b M : ℕ)
    …

    Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree