OAI/Analysis/LiebThirring/InitialOrbit.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Disjoint equivariant coordinate balls for the unique initial zero orbit.

  1. lemma OAI.SharpLiebThirring.PLParity.orbit_separation line 27
  2. def OAI.SharpLiebThirring.PLParity.orbitBall line 51
  3. def OAI.SharpLiebThirring.PLParity.ballLabel line 53
  4. lemma OAI.SharpLiebThirring.PLParity.ballLabel_dist line 57
  5. lemma OAI.SharpLiebThirring.PLParity.orbitBall_smul line 62
  6. lemma OAI.SharpLiebThirring.PLParity.mem_orbitBall_smul_iff line 69
  7. lemma OAI.SharpLiebThirring.PLParity.ballLabel_eq line 80
  8. lemma OAI.SharpLiebThirring.PLParity.ballLabel_smul line 90
  9. lemma OAI.SharpLiebThirring.PLParity.ballLabel_eq_of_dist line 98
  10. lemma OAI.SharpLiebThirring.PLParity.exists_common_ballLabel line 111
  11. lemma OAI.SharpLiebThirring.CubeFlags.augmented_translate_independent line 129
  12. lemma OAI.SharpLiebThirring.CubeFlags.augmented_equiv_independent line 149
  13. lemma OAI.SharpLiebThirring.CubeFlags.Signs.smul_time_zero line 156
  14. lemma OAI.SharpLiebThirring.CubeFlags.Flag.augmented_spatial_scaled line 160
  15. instance OAI.SharpLiebThirring.CubeFlags.signsSubgroupIsIsometric line 170
  16. def OAI.SharpLiebThirring.CubeFlags.affineOrbitModel line 180
  17. lemma OAI.SharpLiebThirring.CubeFlags.affineOrbitModel_smul line 184
  18. lemma OAI.SharpLiebThirring.CubeFlags.affineOrbitModel_dist line 191
  19. lemma OAI.SharpLiebThirring.CubeFlags.affineOrbitModel_augmented line 200
  20. lemma OAI.SharpLiebThirring.CubeFlags.affineOrbitModel_independent line 208
  21. lemma OAI.SharpLiebThirring.CubeFlags.Flag.dist_gridPoint_gridPoint line 223
  22. lemma OAI.SharpLiebThirring.CubeFlags.exists_generic_initial_root line 234
  23. lemma OAI.SharpLiebThirring.CubeFlags.common_flag_label line 267
  24. lemma OAI.SharpLiebThirring.CubeFlags.fixed_initial_augmented line 279
  25. lemma OAI.SharpLiebThirring.CubeFlags.dist_convex_sum_le line 308
  26. lemma OAI.SharpLiebThirring.CubeFlags.bottomSeed_open_roots line 325

    Source documentation

    The bottom cube has a nonempty open family of roots with strictly positive facet barycentric coordinates. A generic root can be chosen in this family.

    lemma bottomSeed_open_roots {d : ℕ} (h : ℝ) (hh : 0 < h) (p : Fin d → ℝ) :
    ∃ U : Set (Fin d → ℝ), IsOpen U ∧ U.Nonempty ∧
      ∀ q ∈ U, ∃ w : Fin (d + 2) → ℝ,
        (∀ k, 0 ≤ w k) ∧ (∀ k, k ≠ Fin.last (d + 1) → 0 < w k) ∧
        ∑ k, w k = 1 ∧ w (Fin.last (d + 1)) = 0 ∧
        ∑ k, w k • gridPoint h ((bottomSeed h p).vertex k) = embedSpatial q ∧
        dist (embedSpatial q) (embedSpatial p) ≤ 2 * h := by
…

    Mentions: OAI.SharpLiebThirring.CubeFlags.gridPoint, OAI.SharpLiebThirring.CubeFlags.bottomSeed, OAI.SharpLiebThirring.CubeFlags.embedSpatial