BumpDerivatives.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform derivatives of scaled cap bumps

A single compactly supported bump controls every center and radius. The scale enters through the curve supplied to that fixed bump, so the k-th bound loses only the k-th power of the inverse cap radius.

def OAI.Falconer.unitCapBump line 18
theorem OAI.Falconer.capBump_eq_unit line 24

theorem OAI.Falconer.capBump_curve_derivatives line 31

Source documentation

This applies to an arbitrary smooth curve and will be specialized to the rotated normalized line. The constant is independent of its center and scale.

theorem capBump_curve_derivatives (d m : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (δ : ℝ) (hδ : 0 < δ), δ ≤ 1 →
      ∀ (c : Sphere d) (γ : ℝ → Space d), ContDiff ℝ ∞ γ →
      ∀ (D u : ℝ), 1 ≤ D →
      (∀ k, 1 ≤ k → k ≤ m → ‖iteratedDeriv k γ u‖ ≤ D^k) →
      |iteratedDeriv m (fun t => capBump δ hδ c (γ t)) u| ≤ C*(D/δ)^m := by
…

Mentions: OAI.Falconer.Sphere, OAI.Falconer.Space, OAI.Falconer.capBump

theorem OAI.Falconer.tangent_line_eq line 74
theorem OAI.Falconer.tangent_line_derivatives line 84

theorem OAI.Falconer.tangent_line_derivative_scale line 120

Source documentation

One fixed scale controls all positive orders up to a chosen finite order.

theorem tangent_line_derivative_scale (m : ℕ) :
    ∃ D : ℝ, 1 ≤ D ∧ ∀ (w y t : E),
      ‖w‖ = 1 → ‖t‖ = 1 → inner ℝ w y = 0 → inner ℝ w t = 0 →
      inner ℝ y t = 0 → ‖y‖ ≤ 1 → ∀ u ∈ Icc (-1 : ℝ) 1,
      ∀ k, 1 ≤ k → k ≤ m → ‖iteratedDeriv k (normalizedLine (w+y) t) u‖ ≤ D^k := by
…

Mentions: OAI.Falconer.normalizedLine