OAI/Analysis/LiebThirring/Continuation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.CubeFlags.radialCut line 19

   Source documentation

   A continuous cutoff equal to one on the inner half ball.

   def radialCut (R t : ℝ) : ℝ := max 0 (min 1 (2 - 2*t/R))

2. lemma OAI.SharpLiebThirring.CubeFlags.radialCut_nonneg line 21
3. lemma OAI.SharpLiebThirring.CubeFlags.radialCut_le_one line 22
4. lemma OAI.SharpLiebThirring.CubeFlags.radialCut_eq_zero line 24
5. lemma OAI.SharpLiebThirring.CubeFlags.radialCut_eq_one line 30
6. lemma OAI.SharpLiebThirring.CubeFlags.continuous_radialCut line 34
7. def OAI.SharpLiebThirring.CubeFlags.localAffine line 45
8. def OAI.SharpLiebThirring.CubeFlags.flattenTerm line 48
9. def OAI.SharpLiebThirring.CubeFlags.flattenInitial line 51
10. lemma OAI.SharpLiebThirring.CubeFlags.localAffine_smul line 55
11. lemma OAI.SharpLiebThirring.CubeFlags.continuous_localAffine line 60
12. lemma OAI.SharpLiebThirring.CubeFlags.continuous_flattenInitial line 67
13. lemma OAI.SharpLiebThirring.CubeFlags.flattenInitial_equivariant line 75
14. lemma OAI.SharpLiebThirring.CubeFlags.flattenInitial_eq_self line 88
15. lemma OAI.SharpLiebThirring.CubeFlags.flattenInitial_in_ball line 101
16. lemma OAI.SharpLiebThirring.CubeFlags.flattenInitial_inner line 126
17. lemma OAI.SharpLiebThirring.CubeFlags.affineOrbitModel_zero_bottom line 143
18. lemma OAI.SharpLiebThirring.CubeFlags.flattenInitial_zero_bottom line 158
19. lemma OAI.SharpLiebThirring.CubeFlags.flattenInitial_final line 188
20. lemma OAI.SharpLiebThirring.CubeFlags.compact_zeros_flattenInitial line 211
21. theorem OAI.SharpLiebThirring.CubeFlags.exists_terminal_zero_local line 229

    Source documentation

    A simple initial zero need only agree with its invertible linearization up to a relative error of one half. Compactly supported flattening turns this into the affine continuation theorem, without adding any new final zeros.

    theorem exists_terminal_zero_local
        (hHt : ∀ s : H, s.val.val (Fin.last d) = false)
        (hρ : ∀ s : H, ∀ v : V, ‖ρ s v‖ = ‖v‖)
        (hR : 0 < R) (hR1 : R ≤ 1)
        (hsep : ∀ g k : H, g ≠ k → 8 * R < dist (g • embedSpatial p) (k • embedSpatial p))
        (hball : orbitBall (G := H) (embedSpatial p) R ⊆ freeLocus (G := H))
    …

    Mentions: OAI.SharpLiebThirring.CubeFlags.embedSpatial

22. lemma OAI.SharpLiebThirring.CubeFlags.hasFDerivAt_relative_error line 269
23. theorem OAI.SharpLiebThirring.CubeFlags.exists_terminal_zero_simple line 303

    Source documentation

    A continuous equivariant homotopy with compact free zero set and one simple initial zero orbit must have a terminal zero. No smoothness is required away from the distinguished initial point.

    theorem exists_terminal_zero_simple {d : ℕ}
        (H : Subgroup (Signs (d + 1))) (hHt : ∀ s : H, s.val.val (Fin.last d) = false)
        {V : Type u147} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
        (ρ : H →* (V ≃ₗ[ℝ] V)) (L : (Fin d → ℝ) ≃ₗ[ℝ] V)
        (hρ : ∀ s : H, ∀ v : V, ‖ρ s v‖ = ‖v‖)
        (p : Fin d → ℝ) (f : (Fin (d + 1) → ℝ) → V)
        (hf : Continuous f) (hfe : ∀ s : H, ∀ x, f (s • x) = ρ s (f x))
        (hp0 : f (embedSpatial p) = 0)
        (hd : HasFDerivAt (fun u : Fin d → ℝ ↦ f (embedSpatial u))
          L.toContinuousLinearEquiv.toContinuousLinearMap p)
        (hz0 : ∀ x, x (Fin.last d) = 0 → f x = 0 → ∃ s : H, s • embedSpatial p = x)
        (hK : IsCompact {x | x (Fin.last d) ∈ Set.Icc (0 : ℝ) 1 ∧ f x = 0})
    …

    Mentions: OAI.SharpLiebThirring.CubeFlags.Signs, OAI.SharpLiebThirring.CubeFlags.embedSpatial