Alignment.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Alignment from an attained positive defect

The actual positive schedule supplies the invariant convex set; the actual return-map estimate and the proved fixed-point theorem supply its fixed point. The original center and scalar remain unchanged throughout the construction.

def OAI.Tingley.aligned_of_return_fixed line 25

Source documentation

A fixed point of the genuine sphere return map gives the exact four chords.

def aligned_of_return_fixed
    (f : UnitSphere X ≃ᵢ UnitSphere Y) (y : UnitSphere X)
    (t M : ℝ) (ht : 0 < t ∧ t < 1) (hb : HasDefectBound f M)
    (v : UnitSphere X) (hv : v ∈ extremalSphere f y t ht M)
    (hfixed : returnSphere f y t ht v = v) : AlignedConfiguration f y t M where
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.HasDefectBound, OAI.Tingley.extremalSphere, OAI.Tingley.returnSphere, OAI.Tingley.AlignedConfiguration

theorem OAI.Tingley.exists_alignedConfiguration line 61

Source documentation

Alignment has no supplied invariant-set, contraction or fixed-point premise.

theorem exists_alignedConfiguration [CompleteSpace X]
    (f : UnitSphere X ≃ᵢ UnitSphere Y) (y x₀ : UnitSphere X)
    (t M : ℝ) (ht : 0 < t ∧ t < 1) (hM : 0 < M)
    (hb : HasDefectBound f M) (hatt : signedDefect f t x₀ y = M) :
    Nonempty (AlignedConfiguration f y t M) := by
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.HasDefectBound, OAI.Tingley.signedDefect, OAI.Tingley.AlignedConfiguration