OAI/MeasureTheory/Falconer/Angular/AngularChart.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A normalized affine line in a spherical chart

Differentiation in a gnomonic chart is the tangential projection of the coordinate direction divided by the normalization. This connects the failed perpendicular test to an ordinary one-variable phase derivative.

  1. def OAI.Falconer.normalizedLine line 19
  2. theorem OAI.Falconer.normalizedLine_norm line 22
  3. theorem OAI.Falconer.norm_line_hasDerivAt line 27
  4. theorem OAI.Falconer.normalizedLine_hasDerivAt line 41
  5. theorem OAI.Falconer.normalizedLine_phase_hasDerivAt line 54
  6. theorem OAI.Falconer.normalizedLine_phase_nonstationary line 61

    Source documentation

    The normalization costs at most two in the failed-test lower bound.

    theorem normalizedLine_phase_nonstationary (a t Δ : E) {u τ : ℝ}
    (hne : a+u•t ≠ 0) (hnorm : ‖a+u•t‖ ≤ 2) (hτ : 0 ≤ τ)
    (hderiv : τ/2 ≤ |inner ℝ (perpendicularPart (normalizedLine a t u) t) Δ|) :
    τ/4 ≤ |deriv (fun x => inner ℝ (normalizedLine a t x) Δ) u| := by
…

    Mentions: OAI.Falconer.perpendicularPart, OAI.Falconer.normalizedLine