OAI/Analysis/LiebThirring/FlagGeometry.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.CubeFlags.Signs.linearIsometry line 14

   Source documentation

   Coordinate reflection as an isometric linear equivalence in the sup norm.

   def Signs.linearIsometry {n : ℕ} (s : Signs n) :
       (Fin n → ℝ) ≃ₗᵢ[ℝ] (Fin n → ℝ) where
   …

   Mentions: OAI.SharpLiebThirring.CubeFlags.Signs

2. instance OAI.SharpLiebThirring.CubeFlags.(instance at line 38) line 38
3. lemma OAI.SharpLiebThirring.CubeFlags.Signs.smul_real line 52
4. instance OAI.SharpLiebThirring.CubeFlags.(instance at line 55) line 55
5. instance OAI.SharpLiebThirring.CubeFlags.(instance at line 58) line 58
6. lemma OAI.SharpLiebThirring.CubeFlags.Signs.smul_int line 72
7. lemma OAI.SharpLiebThirring.CubeFlags.Flag.point_smul line 75
8. lemma OAI.SharpLiebThirring.CubeFlags.Flag.vertex_smul line 80
9. def OAI.SharpLiebThirring.CubeFlags.Flag.center line 86

   Source documentation

   The common final vertex is the cube center.

   def Flag.center {n : ℕ} (F : Flag n) : Fin n → ℝ := F.point (Fin.last n)

   Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

10. lemma OAI.SharpLiebThirring.CubeFlags.Flag.center_apply line 88
11. lemma OAI.SharpLiebThirring.CubeFlags.Flag.center_smul line 94
12. lemma OAI.SharpLiebThirring.CubeFlags.Flag.dist_point_center line 97
13. lemma OAI.SharpLiebThirring.CubeFlags.Flag.dist_combination_center line 105
14. lemma OAI.SharpLiebThirring.CubeFlags.Flag.neighbor_center_dist line 114
15. lemma OAI.SharpLiebThirring.CubeFlags.Flag.dist_combination_point line 133
16. lemma OAI.SharpLiebThirring.CubeFlags.dist_scale line 142
17. lemma OAI.SharpLiebThirring.CubeFlags.Flag.dist_scaled_point_center line 146
18. lemma OAI.SharpLiebThirring.CubeFlags.Flag.finite_base_bounds line 151
19. lemma OAI.SharpLiebThirring.CubeFlags.Flag.finite_near_centers line 168

    Source documentation

    Cubes whose centers are close to a compact set form a finite collection.

    lemma Flag.finite_near_centers {n : ℕ} {K : Set (Fin n → ℝ)} (hK : Bornology.IsBounded K)
        (h r : ℝ) (hh : 0 < h) :
        Set.Finite {F : Flag n | ∃ x ∈ K, dist (h • F.center) x < r} := by
    …

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

20. def OAI.SharpLiebThirring.CubeFlags.nearCylinder line 194

    Source documentation

    The spatially truncated cylinder of cubical flags used in continuation.

    def nearCylinder {n : ℕ} (K : Set (Fin n → ℝ)) (h r : ℝ) (t : Fin n) (m : ℕ) : Set (Flag n) :=
    …

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

21. lemma OAI.SharpLiebThirring.CubeFlags.finite_nearCylinder line 197
22. lemma OAI.SharpLiebThirring.CubeFlags.nearCylinder_smul line 201
23. lemma OAI.SharpLiebThirring.CubeFlags.nearCylinder_point_cthickening line 217
24. lemma OAI.SharpLiebThirring.CubeFlags.Flag.neighbor_base_of_ne_last line 228
25. lemma OAI.SharpLiebThirring.CubeFlags.Flag.neighbor_outside_time line 236

    Source documentation

    A time-boundary facet is exactly the last facet of a flag expanding time last.

    lemma Flag.neighbor_outside_time {n : ℕ} [NeZero n] (F : Flag n) (j : Fin (n + 1))
        (t : Fin n) (m : ℤ) (hlo : 0 ≤ F.base t) (hhi : F.base t < m)
        (hout : ¬ (0 ≤ (F.neighbor j).base t ∧ (F.neighbor j).base t < m)) :
        j = Fin.last n ∧ (F.order.symm t).val = n - 1 ∧
          ((F.base t = 0 ∧ F.corner t = false) ∨ (F.base t = m - 1 ∧ F.corner t = true)) := by
    …

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

26. lemma OAI.SharpLiebThirring.CubeFlags.Flag.point_time_boundary line 266
27. lemma OAI.SharpLiebThirring.CubeFlags.nearCylinder_point_time line 277
28. lemma OAI.SharpLiebThirring.CubeFlags.nearCylinder_combination_time line 291
29. def OAI.SharpLiebThirring.CubeFlags.gridPoint line 311

    Source documentation

    Embed the twice-barycenter lattice at mesh size h.

    def gridPoint {n : ℕ} (h : ℝ) (z : Fin n → ℤ) : Fin n → ℝ :=
    …

30. lemma OAI.SharpLiebThirring.CubeFlags.gridPoint_vertex line 314
31. lemma OAI.SharpLiebThirring.CubeFlags.gridPoint_smul line 320
32. lemma OAI.SharpLiebThirring.CubeFlags.gridPoint_injective line 327
33. def OAI.SharpLiebThirring.CubeFlags.vertices line 339

    Source documentation

    All vertices of a group-invariant collection of cubical flags.

    def vertices : SubMulAction H (Fin n → ℤ) where
    …

34. instance OAI.SharpLiebThirring.CubeFlags.verticesFintype line 346
35. def OAI.SharpLiebThirring.CubeFlags.flagVertex line 360
36. lemma OAI.SharpLiebThirring.CubeFlags.flagVertex_smul line 362
37. lemma OAI.SharpLiebThirring.CubeFlags.flagVertex_orbits_injective line 366
38. theorem OAI.SharpLiebThirring.CubeFlags.verticesIsCancel line 379

    Source documentation

    Freeness of the real vertex positions induces freeness on the finite vertex set. It is supplied by the compact free-locus tube, not presumed.

    theorem verticesIsCancel (h : ℝ)
        (hfree : ∀ z : vertices H D, ∀ s : H, s • gridPoint h z.val = gridPoint h z.val → s = 1) :
        IsCancelSMul H (vertices H D) where
    …

    Mentions: OAI.SharpLiebThirring.CubeFlags.vertices, OAI.SharpLiebThirring.CubeFlags.gridPoint