SmoothReciprocal.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Smooth reciprocal of a nonstationary phase derivative

The reciprocal is extended smoothly across zero by a scalar bump. At a point where the denominator is bounded below, its derivative bounds depend only on the normalized derivatives of that denominator.

def OAI.Falconer.smoothReciprocal line 18
theorem OAI.Falconer.smoothReciprocal_contDiff line 21
theorem OAI.Falconer.smoothReciprocal_eq line 35
theorem OAI.Falconer.smoothReciprocal_half_germ line 43

theorem OAI.Falconer.reciprocal_germ_derivatives line 55

Source documentation

The derivative constants are independent of the denominator, its lower bound, and the frequency scale. Only positive-order derivatives of the denominator enter the recurrence.

theorem reciprocal_germ_derivatives (B : ℕ → ℝ) (hB : ∀ k, 0 ≤ B k) (n : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (g q : ℝ → ℝ), ContDiff ℝ ∞ g → ContDiff ℝ ∞ q →
      ∀ (τ D x : ℝ), 0 < τ → 0 ≤ D → τ ≤ |g x| →
      (fun y => q y * g y) =ᶠ[𝓝 x] (fun _ => 1) →
      (∀ k, 1 ≤ k → k ≤ n → |iteratedDeriv k g x| ≤ B k * τ * D^k) →
      |iteratedDeriv n q x| ≤ C * τ⁻¹ * D^n := by
…