OAI/NumberTheory/Ostmann/Arithmetic/RealSlotEvaluation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.realSlotProduct line 10
2. def OAI.Ostmann.MovingSlotReversal.realValuePivot line 13
3. def OAI.Ostmann.MovingSlotData.realValueLeafModuli line 19
4. def OAI.Ostmann.realValueNodeCutoff line 28
5. def OAI.Ostmann.realValueFourierWeight line 36
6. def OAI.Ostmann.realValueSmoothWeight line 44
7. theorem OAI.Ostmann.realSlotProduct_nat line 49
8. theorem OAI.Ostmann.MovingSlotReversal.realValuePivot_nat line 57
9. theorem OAI.Ostmann.MovingSlotData.realValueLeafModuli_nat line 62
10. theorem OAI.Ostmann.realValueNodeCutoff_nat line 72
11. theorem OAI.Ostmann.realValueSmoothWeight_nat line 82

    Source documentation

    The extension agrees exactly with the original function at every natural prime tuple, including points where a cutoff vanishes.

    theorem realValueSmoothWeight_nat {σ : Type*} (value : σ → ℕ)
        {n : ℕ} (T : MovingSlotData σ n) (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ)
        (hlo : 1 ≤ lo) (hhi : lo ≤ hi) (φ : ℝ → ℝ) (G : ℕ → ℝ) (L R : ℝ) :
        realValueSmoothWeight (fun i => (value i : ℝ)) T ψ X lo hi hlo hhi φ G L R =
          movingRealSmoothWeight value T ψ X lo hi hlo hhi φ G L R := by
    …

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