OAI/MeasureTheory/Falconer/Fourier/ChartDerivatives.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Uniform derivatives of the normalized line chart

The scalar denominator is a smooth function of two real variables on a fixed compact square. Its bounds are independent of the chart center, tangent direction, and displacement. No analytic input is assumed here.

  1. def OAI.Falconer.partialSecond line 20
  2. theorem OAI.Falconer.partialSecond_smooth line 24
  3. theorem OAI.Falconer.partialSecond_eq line 31
  4. theorem OAI.Falconer.uniform_section_derivatives line 47
  5. def OAI.Falconer.chartLineKernel line 58
  6. theorem OAI.Falconer.chartLineKernel_smooth line 61
  7. theorem OAI.Falconer.chartLineKernel_derivatives line 65
  8. theorem OAI.Falconer.chartLineLinearKernel_derivatives line 70
  9. def OAI.Falconer.chartDensityKernel line 75
  10. theorem OAI.Falconer.chartDensityKernel_smooth line 78
  11. theorem OAI.Falconer.chartDensityKernel_derivatives line 82
  12. theorem OAI.Falconer.tangent_line_norm_sq line 90
  13. theorem OAI.Falconer.tangent_line_phase_eq line 99
  14. theorem OAI.Falconer.tangent_line_phase_smooth line 110
  15. theorem OAI.Falconer.tangent_line_phase_derivatives line 121

    Source documentation

    All phase derivatives on the unit chart are bounded by the displacement norm, with constants independent of the ambient dimension and chart.

    theorem tangent_line_phase_derivatives (n : ℕ) :
    ∃ B : ℝ, 0 ≤ B ∧ ∀ (w y t v : E),
      ‖w‖ = 1 → ‖t‖ = 1 → inner ℝ w y = 0 → inner ℝ w t = 0 →
      inner ℝ y t = 0 → ‖y‖ ≤ 1 → ∀ u ∈ Icc (-1 : ℝ) 1,
      |iteratedDeriv n (fun x => inner ℝ (normalizedLine (w+y) t x) v) u| ≤ B*‖v‖ := by
…

    Mentions: OAI.Falconer.normalizedLine