OAI/Analysis/LiebThirring/BoundaryParity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.CubeFlags.bottom_hit_unique line 18
2. lemma OAI.SharpLiebThirring.CubeFlags.mesh_parity_contradiction line 69

   Source documentation

   Finite equivariant parity rules out a bounded approximating cylinder whose only boundary hits lie in the one initial root orbit.

   lemma mesh_parity_contradiction {d : ℕ} (H : Subgroup (Signs (d + 1)))
       (hHt : ∀ s : H, s.val.val (Fin.last d) = false)
       (D : SubMulAction H (Flag (d + 1))) [Fintype D]
       {V : Type u137} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
       (ρ : H →* (V ≃ₗ[ℝ] V)) (L : (Fin d → ℝ) ≃ₗ[ℝ] V)
       (p q : Fin d → ℝ) (R h : ℝ) (hR : 0 < R) (hh : 0 < h) (hhr : 2*h < R)
       (hsep : ∀ g k : H, g ≠ k → 8 * R < dist (g • embedSpatial p) (k • embedSpatial p))
       (a : vertices H D → V) (ha : ∀ s : H, ∀ z, a (s • z) = ρ s (a z))
       (haug : ∀ F : D, ∀ j : Fin (d + 2), LinearIndependent ℝ
         (fun k : {k // k ≠ j} ↦ ((1 : ℝ), a (flagVertex H D F k))))
       (hvec : ∀ F : D, ∀ i j : Fin (d + 2), i ≠ j → LinearIndependent ℝ
         (fun k : {k // k ≠ i ∧ k ≠ j} ↦ a (flagVertex H D F k)))
   …

   Mentions: OAI.SharpLiebThirring.CubeFlags.Signs, OAI.SharpLiebThirring.CubeFlags.Flag, OAI.SharpLiebThirring.CubeFlags.embedSpatial, OAI.SharpLiebThirring.CubeFlags.vertices, OAI.SharpLiebThirring.CubeFlags.flagVertex

3. lemma OAI.SharpLiebThirring.CubeFlags.fixed_initial_vectors line 136
4. lemma OAI.SharpLiebThirring.CubeFlags.generic_initial_approximation line 157
5. lemma OAI.SharpLiebThirring.CubeFlags.mesh_boundary_bottom line 255
6. lemma OAI.SharpLiebThirring.CubeFlags.isOpen_orbitBall line 280
7. lemma OAI.SharpLiebThirring.CubeFlags.dist_spatial_le line 288
8. lemma OAI.SharpLiebThirring.CubeFlags.exists_positive_mesh line 294
9. lemma OAI.SharpLiebThirring.CubeFlags.bottomSeed_mem_nearCylinder line 301
10. lemma OAI.SharpLiebThirring.CubeFlags.bottomSeed_neighbor_not_mem line 308
11. theorem OAI.SharpLiebThirring.CubeFlags.exists_terminal_zero_affine line 332

    Source documentation

    The exact continuation principle needed below, first for an affine initial model in disjoint neighborhoods of its one free zero orbit. The proof uses finite equivariant PL perturbation and mod-two boundary pairing.

    theorem exists_terminal_zero_affine {d : ℕ}
        (H : Subgroup (Signs (d + 1))) (hHt : ∀ s : H, s.val.val (Fin.last d) = false)
        {V : Type u142} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
        (ρ : H →* (V ≃ₗ[ℝ] V)) (L : (Fin d → ℝ) ≃ₗ[ℝ] V)
        (hρ : ∀ s : H, ∀ v : V, ‖ρ s v‖ = ‖v‖)
        (p : Fin d → ℝ) (R : ℝ) (hR : 0 < R)
        (hsep : ∀ g k : H, g ≠ k → 8 * R < dist (g • embedSpatial p) (k • embedSpatial p))
        (f : (Fin (d + 1) → ℝ) → V)
        (hf : ContinuousOn f {x | x (Fin.last d) ∈ Set.Icc (0 : ℝ) 1})
        (hfe : ∀ s : H, ∀ x, f (s • x) = ρ s (f x))
        (hmodel : ∀ x, x (Fin.last d) = 0 → x ∈ orbitBall (G := H) (embedSpatial p) R →
    …

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