ChartGeometry.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The failed perpendicular test in an actual spherical chart

The normalized affine chart stays within twice its tangent displacement of the cap center. Its coordinate derivative therefore inherits the uniform lower bound proved for the tangential sphere field.

theorem OAI.Falconer.norm_normalization_sub_le line 16
theorem OAI.Falconer.tangent_chart_nonzero line 34

theorem OAI.Falconer.perpendicular_failure_chart_nonstationary line 44

Source documentation

A single coordinate direction works for every allowed point and direction replacement in the discarded cell--cap term.

theorem perpendicular_failure_chart_nonstationary {w₀ d : E}
    (hw₀ : ‖w₀‖ = 1) {τ : ℝ} (hτ : 0 < τ)
    (hbad : τ < ‖perpendicularPart w₀ d‖) :
    ∃ t : E, ‖t‖ = 1 ∧ inner ℝ w₀ t = 0 ∧
      ∀ (y v : E) (u : ℝ), inner ℝ w₀ y = 0 → ‖y+u•t‖ ≤ 1 →
        ‖v-d‖ + 4*‖y+u•t‖*‖d‖ ≤ τ/2 →
        τ/4 ≤ |deriv (fun x => inner ℝ (normalizedLine (w₀+y) t x) v) u| := by
…

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