DefectSequence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A positive signed extremal sequence at a fixed radius

One fixed free ultrafilter chooses the orientation and the radius. The conclusion is convergence along that actual filter, not an asserted compactness of spheres.

theorem OAI.Tingley.tendsto_signedDefect_fixed_radius line 25

Source documentation

Uniform radius control replaces a varying radius by its actual scalar limit.

theorem tendsto_signedDefect_fixed_radius
    (f : UnitSphere X ≃ᵢ UnitSphere Y) (x y : ℕ → UnitSphere X)
    (q : ℕ → ℝ) {l : Filter ℕ} {t M : ℝ}
    (hq : Tendsto q l (𝓝 t))
    (hD : Tendsto (fun n => signedDefect f (q n) (x n) (y n)) l (𝓝 M)) :
    Tendsto (fun n => signedDefect f t (x n) (y n)) l (𝓝 M) := by
…

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

theorem OAI.Tingley.radius_interior_of_positive_defect_limit line 49

Source documentation

Positive limiting defect forces a strictly interior radius.

theorem radius_interior_of_positive_defect_limit
    (f : UnitSphere X ≃ᵢ UnitSphere Y) (x y : ℕ → UnitSphere X)
    (U : Ultrafilter ℕ) {t M : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1)
    (hM : 0 < M)
    (hD : Tendsto (fun n => signedDefect f t (x n) (y n)) (U : Filter ℕ) (𝓝 M)) :
    t ∈ Set.Ioo (0 : ℝ) 1 := by
…

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

theorem OAI.Tingley.exists_fixed_radius_defect_sequence line 67

Source documentation

The absolute supremum has actual fixed-radius signed witnesses in one orientation.

theorem exists_fixed_radius_defect_sequence [Nontrivial X]
    (f : UnitSphere X ≃ᵢ UnitSphere Y) (hM : 0 < maxDefect f) :
    ∃ t : ℝ, t ∈ Set.Ioo (0 : ℝ) 1 ∧
      ((∃ x y : ℕ → UnitSphere X,
          Tendsto (fun n => signedDefect f t (x n) (y n))
            (freeUltrafilter : Filter ℕ) (𝓝 (maxDefect f))) ∨
       (∃ x y : ℕ → UnitSphere Y,
          Tendsto (fun n => signedDefect f.symm t (x n) (y n))
            (freeUltrafilter : Filter ℕ) (𝓝 (maxDefect f)))) := by
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.maxDefect, OAI.Tingley.signedDefect, OAI.Tingley.freeUltrafilter