NonstationaryGeometry.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Nonstationary directions for discarded graph edges

The sphere vector field is the tangential projection of one fixed unit vector. Its phase derivative stays large on a cap when a perpendicular center test fails. This is the geometric part of graph:localization; integration by parts is a separate analytic step.

theorem OAI.Falconer.perpendicularPart_self_adjoint line 18
theorem OAI.Falconer.perpendicularPart_orthogonal line 25
theorem OAI.Falconer.perpendicularPart_inner_original line 30
theorem OAI.Falconer.exists_unit_tangent line 48
Source documentation
A fixed unit tangent at the cap center whose scalar product with the center displacement equals its perpendicular length.
```
theorem exists_unit_tangent {w : E} (hw : ‖w‖ = 1) (v : E)
    (hne : perpendicularPart w v ≠ 0) :
    ∃ t : E, ‖t‖ = 1 ∧ inner ℝ w t = 0 ∧
      inner ℝ t v = ‖perpendicularPart w v‖ := by
…
```
Mentions: OAI.Falconer.perpendicularPart

theorem OAI.Falconer.angular_phase_derivative_error line 63

Source documentation

The sphere field t - ⟪w,t⟫ w is tangent and has the expected uniform phase-derivative error under cap and point replacement.

theorem angular_phase_derivative_error {w w₀ t : E}
    (hw : ‖w‖ = 1) (hw₀ : ‖w₀‖ = 1) (ht : ‖t‖ = 1)
    (htan : inner ℝ w₀ t = 0) (v d : E) :
    |inner ℝ (perpendicularPart w t) v - inner ℝ t d| ≤
      ‖v-d‖ + 2 * ‖w-w₀‖ * ‖d‖ := by
…

Mentions: OAI.Falconer.perpendicularPart

theorem OAI.Falconer.perpendicular_failure_nonstationary line 80

Source documentation

One fixed tangent direction witnesses nonstationarity throughout the allowed perturbations of a discarded perpendicular edge.

theorem perpendicular_failure_nonstationary {w₀ d : E} (hw₀ : ‖w₀‖ = 1)
    {τ : ℝ} (hτ : 0 < τ) (hbad : τ < ‖perpendicularPart w₀ d‖) :
    ∃ t : E, ‖t‖ = 1 ∧ inner ℝ w₀ t = 0 ∧
      ∀ w v : E, ‖w‖ = 1 →
        ‖v-d‖ + 2 * ‖w-w₀‖ * ‖d‖ ≤ τ/2 →
        τ/2 ≤ |inner ℝ (perpendicularPart w t) v| := by
…

Mentions: OAI.Falconer.perpendicularPart

theorem OAI.Falconer.longitudinal_failure_nonstationary line 102

Source documentation

Failure of the longitudinal center test gives a radial phase derivative bounded away from zero after the two endpoint replacements.

theorem longitudinal_failure_nonstationary {w₁ w₂ z₁ z₂ : E}
    (hw₁ : ‖w₁‖ = 1) (hw₂ : ‖w₂‖ = 1)
    (v₁ v₂ d₁ d₂ : E) {τ : ℝ}
    (hbad : τ < |inner ℝ z₁ d₁ + inner ℝ z₂ d₂|)
    (herr : (‖v₁-d₁‖ + ‖w₁-z₁‖ * ‖d₁‖) +
      (‖v₂-d₂‖ + ‖w₂-z₂‖ * ‖d₂‖) ≤ τ/2) :
    τ/2 ≤ |inner ℝ w₁ v₁ + inner ℝ w₂ v₂| := by
…