OAI/Topology/EilenbergGanea/WordEquations.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EilenbergGanea.localized_word_root_sublevel line 18

   Source documentation

   A concrete sublevel version of localized degree. The only root isolation conditions are a uniform radial bound and exclusion of the threshold; no regularity of any root or of the sublevel boundary is assumed.

   theorem localized_word_root_sublevel {m : ℕ}
       (w : Fin m → FreeGroup (Fin m)) (hB : (exponentMatrix w).det ≠ 0)
       (F : ℝ × ((Fin m → ℂ) × (Fin m → ℂ)) → ((Fin m → ℂ) × (Fin m → ℂ)))
       (hF : ContDiff ℝ 2 F) (hF0 : ∀ q, F (0, q) = splitWordMap w q)
       (h : ℝ × ((Fin m → ℂ) × (Fin m → ℂ)) → ℝ) (hh : Continuous h)
       (δ R : ℝ) (hR : ‖((1 : Fin m → ℂ), (0 : Fin m → ℂ))‖ < R)
       (h1 : h (0, (1, 0)) < δ)
       (hi : ∀ z : ℂ, ‖z‖ = 1 → ∀ q, h (0, (q.1, z • q.2)) = h (0, q))
       (hbound : ∀ q, q.1 ∈ Icc (0 : ℝ) 1 → F q = 0 → ‖q.2‖ < R)
       (hiso : ∀ q, q.1 ∈ Icc (0 : ℝ) 1 → F q = 0 → h q ≠ δ) :
       ∃ x, F (1, x) = 0 ∧ h (1, x) < δ := by
   …

   Mentions: OAI.EilenbergGanea.exponentMatrix, OAI.EilenbergGanea.splitWordMap

2. def OAI.EilenbergGanea.coefficientWordMap line 78

   Source documentation

   Word evaluation with a fixed alphabet of coefficient letters and a finite alphabet of unknowns. Coefficients may vary smoothly with a real parameter.

   def coefficientWordMap {ι : Type*} {m d : ℕ}
       (w : Fin d → FreeGroup (ι ⊕ Fin m)) (a : ℝ → ι → SU2)
       (q : ℝ × (Fin m → SU2)) : Fin d → SU2 :=
   …

   Mentions: OAI.EilenbergGanea.SU2

3. def OAI.EilenbergGanea.eraseCoefficients line 83
4. theorem OAI.EilenbergGanea.coefficientWordMap_initial line 86
5. theorem OAI.EilenbergGanea.radialCutoff_family_smooth line 101

   Source documentation

   The same conjugation-invariant radial cutoff handles arbitrary coefficient words, and does not create roots on the coordinate hyperplanes.

   theorem radialCutoff_family_smooth {m : ℕ} {V : Type*}
       [NormedAddCommGroup V] [NormedSpace ℝ V]
       (f : ℝ × (Fin m → ℍ) → V)
       (hf : ∀ q, (∀ i, q.2 i ≠ 0) → ContDiffAt ℝ ∞ f q) :
       ContDiff ℝ ∞ (fun q => radialCutoff q.2 • f q) := by
   …

   Mentions: OAI.EilenbergGanea.radialCutoff

6. theorem OAI.EilenbergGanea.coefficientWordMap_normalized_smoothAt line 118
7. def OAI.EilenbergGanea.radialCoefficientWordMap line 137
8. def OAI.EilenbergGanea.smoothRadialCoefficientWordMap line 142
9. theorem OAI.EilenbergGanea.smoothRadialCoefficientWordMap_smooth line 147
10. theorem OAI.EilenbergGanea.radialCoefficientWordMap_norm line 158
11. theorem OAI.EilenbergGanea.radialCoefficientWordMap_eq_one_iff line 166
12. theorem OAI.EilenbergGanea.smoothRadialCoefficientWordMap_eq_one_iff line 185
13. theorem OAI.EilenbergGanea.smoothRadialCoefficientWordMap_initial line 206
14. def OAI.EilenbergGanea.cutoffCoefficientProducts line 223
15. theorem OAI.EilenbergGanea.cutoffCoefficientProducts_smooth line 229
16. theorem OAI.EilenbergGanea.cutoffCoefficientProducts_unitary line 235
17. theorem OAI.EilenbergGanea.quaternionConjugate_sub line 249
18. theorem OAI.EilenbergGanea.coefficientWordMap_initial_conjugate line 253
19. theorem OAI.EilenbergGanea.cutoffCoefficientProducts_initial_conjugate line 268
20. theorem OAI.EilenbergGanea.cutoffCoefficientProducts_initial_size_invariant line 278
21. theorem OAI.EilenbergGanea.coefficient_word_sublevel_solvable line 295

    Source documentation

    Finite-word-system solvability with an actual distinguished-word sublevel isolator. Arbitrarily singular initial word roots are allowed.

    theorem coefficient_word_sublevel_solvable {ι : Type*} {m d : ℕ}
        (w : Fin m → FreeGroup (ι ⊕ Fin m)) (ρ : Fin d → FreeGroup (ι ⊕ Fin m))
        (a : ℝ → ι → SU2) (ha : ∀ i, ContDiff ℝ ∞ (fun t => (a t i : ℍ)))
        (ha0 : ∀ i, a 0 i = 1)
        (hB : (exponentMatrix (fun i => eraseCoefficients (w i))).det ≠ 0)
        (δ : ℝ) (hδ : 0 < δ)
        (hiso : ∀ t ∈ Icc (0 : ℝ) 1, ∀ x : Fin m → SU2,
          coefficientWordMap w a (t, x) = 1 →
          ‖(fun i => (coefficientWordMap ρ a (t, x) i : ℍ)) - 1‖ ≠ δ) :
        ∃ x : Fin m → SU2, coefficientWordMap w a (1, x) = 1 ∧
          ‖(fun i => (coefficientWordMap ρ a (1, x) i : ℍ)) - 1‖ < δ := by
    …

    Mentions: OAI.EilenbergGanea.SU2, OAI.EilenbergGanea.exponentMatrix, OAI.EilenbergGanea.eraseCoefficients, OAI.EilenbergGanea.coefficientWordMap