OAI/Analysis/LiebThirring/CubeFlags.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Equivariant cubical barycentric flags. A codimension-one face of a full flag has one canonical neighboring flag; this avoids any orientation choices.

  1. structure OAI.SharpLiebThirring.CubeFlags.Flag line 33

    Source documentation

    A maximal flag in the barycentric subdivision of an integer cube.

    @[ext] structure Flag (n : ℕ) where
…
  2. def OAI.SharpLiebThirring.CubeFlags.Flag.vertex line 39

    Source documentation

    Twice the barycenter of the kth cubical face in a maximal flag.

    def Flag.vertex {n : ℕ} (F : Flag n) (k : Fin (n + 1)) (i : Fin n) : ℤ :=
…

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

  3. def OAI.SharpLiebThirring.CubeFlags.Flag.point line 43

    Source documentation

    The real vertex obtained by rescaling the half-integer grid.

    def Flag.point {n : ℕ} (F : Flag n) (k : Fin (n + 1)) : Fin n → ℝ :=
…

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

  4. lemma OAI.SharpLiebThirring.CubeFlags.Flag.vertex_bounds line 46
  5. lemma OAI.SharpLiebThirring.CubeFlags.Flag.point_bounds line 51
  6. def OAI.SharpLiebThirring.CubeFlags.Flag.flip line 60

    Source documentation

    Toggle the endpoint chosen in coordinate i.

    def Flag.flip {n : ℕ} (F : Flag n) (i : Fin n) : Flag n :=
…

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

  7. lemma OAI.SharpLiebThirring.CubeFlags.Flag.flip_base line 63
  8. lemma OAI.SharpLiebThirring.CubeFlags.Flag.flip_order line 64
  9. lemma OAI.SharpLiebThirring.CubeFlags.Flag.flip_flip line 66
  10. def OAI.SharpLiebThirring.CubeFlags.Flag.cross line 70

    Source documentation

    Across the final facet, pass to the neighboring cube and toggle its endpoint.

    def Flag.cross {n : ℕ} (F : Flag n) (i : Fin n) : Flag n :=
…

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

  11. lemma OAI.SharpLiebThirring.CubeFlags.Flag.cross_order line 73
  12. lemma OAI.SharpLiebThirring.CubeFlags.Flag.cross_cross line 75
  13. def OAI.SharpLiebThirring.CubeFlags.Flag.swap line 80

    Source documentation

    Swap the order of two successive face expansions.

    def Flag.swap {n : ℕ} (F : Flag n) (i j : Fin n) : Flag n :=
…

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

  14. lemma OAI.SharpLiebThirring.CubeFlags.Flag.swap_swap line 83
  15. lemma OAI.SharpLiebThirring.CubeFlags.Flag.flip_vertex line 87
  16. lemma OAI.SharpLiebThirring.CubeFlags.Flag.cross_vertex line 94
  17. lemma OAI.SharpLiebThirring.CubeFlags.Flag.swap_vertex line 105
  18. def OAI.SharpLiebThirring.CubeFlags.Flag.neighbor line 120

    Source documentation

    The other maximal flag sharing the facet obtained by deleting vertex j.

    def Flag.neighbor {n : ℕ} [NeZero n] (F : Flag n) (j : Fin (n + 1)) : Flag n :=
…

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

  19. lemma OAI.SharpLiebThirring.CubeFlags.Flag.neighbor_neighbor line 125
  20. lemma OAI.SharpLiebThirring.CubeFlags.Flag.neighbor_vertex line 136
  21. lemma OAI.SharpLiebThirring.CubeFlags.Flag.flip_ne line 154
  22. lemma OAI.SharpLiebThirring.CubeFlags.Flag.cross_ne line 160
  23. lemma OAI.SharpLiebThirring.CubeFlags.Flag.swap_ne line 166
  24. lemma OAI.SharpLiebThirring.CubeFlags.Flag.neighbor_ne line 172
  25. lemma OAI.SharpLiebThirring.CubeFlags.span_consecutive line 190
  26. lemma OAI.SharpLiebThirring.CubeFlags.linearIndependent_consecutive_iff line 211
  27. def OAI.SharpLiebThirring.CubeFlags.Flag.step line 219
  28. lemma OAI.SharpLiebThirring.CubeFlags.Flag.step_ne_zero line 222
  29. lemma OAI.SharpLiebThirring.CubeFlags.Flag.point_succ_sub line 226
  30. lemma OAI.SharpLiebThirring.CubeFlags.Flag.linearIndependent_steps line 243
  31. lemma OAI.SharpLiebThirring.CubeFlags.Flag.augmented_linearIndependent line 258
  32. def OAI.SharpLiebThirring.CubeFlags.Flag.reflect line 277

    Source documentation

    Coordinate reflections preserve the entire flag subdivision.

    def Flag.reflect {n : ℕ} (s : Fin n → Bool) (F : Flag n) : Flag n where
…

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

  33. lemma OAI.SharpLiebThirring.CubeFlags.Flag.reflect_false line 282
  34. lemma OAI.SharpLiebThirring.CubeFlags.Flag.reflect_reflect line 285
  35. lemma OAI.SharpLiebThirring.CubeFlags.Flag.reflect_vertex line 292
  36. lemma OAI.SharpLiebThirring.CubeFlags.Flag.reflect_point line 300
  37. lemma OAI.SharpLiebThirring.CubeFlags.Flag.reflect_flip line 308
  38. lemma OAI.SharpLiebThirring.CubeFlags.Flag.reflect_cross line 317
  39. lemma OAI.SharpLiebThirring.CubeFlags.Flag.reflect_swap line 334
  40. lemma OAI.SharpLiebThirring.CubeFlags.Flag.reflect_neighbor line 337
  41. structure OAI.SharpLiebThirring.CubeFlags.Signs line 350

    Source documentation

    Coordinate reflections form an elementary two-group.

    @[ext] structure Signs (n : ℕ) where
…
  42. def OAI.SharpLiebThirring.CubeFlags.Signs.equiv line 353
  43. instance OAI.SharpLiebThirring.CubeFlags.(instance at line 359) line 359
  44. instance OAI.SharpLiebThirring.CubeFlags.(instance at line 360) line 360
  45. instance OAI.SharpLiebThirring.CubeFlags.(instance at line 362) line 362
  46. lemma OAI.SharpLiebThirring.CubeFlags.Signs.mul_val line 372
  47. lemma OAI.SharpLiebThirring.CubeFlags.Signs.one_val line 374
  48. lemma OAI.SharpLiebThirring.CubeFlags.Signs.inv_eq line 375
  49. instance OAI.SharpLiebThirring.CubeFlags.(instance at line 377) line 377
  50. lemma OAI.SharpLiebThirring.CubeFlags.Flag.smul_def line 382
  51. instance OAI.SharpLiebThirring.CubeFlags.(instance at line 384) line 384
  52. lemma OAI.SharpLiebThirring.CubeFlags.Flag.smul_neighbor line 394
  53. lemma OAI.SharpLiebThirring.CubeFlags.Flag.vertex_orbits_distinct line 400

    Source documentation

    No two vertices of a flag belong to the same coordinate-reflection orbit. Parity records the order in which coordinates become barycenters.

    lemma Flag.vertex_orbits_distinct {n : ℕ} (F : Flag n)
    (j k : Fin (n + 1)) (s : Signs n)
    (he : ∀ i, F.vertex j i = if s.val i then -F.vertex k i else F.vertex k i) : j = k := by
…

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

  54. def OAI.SharpLiebThirring.CubeFlags.Flag.depth line 424

    Source documentation

    Distance, with the corner sign, from the chosen endpoint of a coordinate.

    def Flag.depth {n : ℕ} (F : Flag n) (i : Fin n) (x : Fin n → ℝ) : ℝ :=
…

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

  55. lemma OAI.SharpLiebThirring.CubeFlags.Flag.depth_point line 427
  56. lemma OAI.SharpLiebThirring.CubeFlags.Flag.depth_combination line 434
  57. lemma OAI.SharpLiebThirring.CubeFlags.Flag.depth_nonneg line 442
  58. lemma OAI.SharpLiebThirring.CubeFlags.Flag.depth_le_half line 452
  59. lemma OAI.SharpLiebThirring.CubeFlags.Flag.depth_pos line 465
  60. lemma OAI.SharpLiebThirring.CubeFlags.Flag.depth_lt_half line 479
  61. lemma OAI.SharpLiebThirring.CubeFlags.Flag.depth_antitone line 496
  62. lemma OAI.SharpLiebThirring.CubeFlags.Flag.depth_strictAnti line 508
  63. lemma OAI.SharpLiebThirring.CubeFlags.Flag.combination_bounds line 525
  64. lemma OAI.SharpLiebThirring.CubeFlags.Flag.combination_strict_bounds line 535
  65. lemma OAI.SharpLiebThirring.CubeFlags.Flag.eq_of_strict_combination line 548

    Source documentation

    Relative interiors of the maximal flag simplices are disjoint, even across neighboring integer cubes. This is the only uniqueness fact needed to count an initial affine zero.

    lemma Flag.eq_of_strict_combination {n : ℕ} (F G : Flag n)
    (w z : Fin (n + 1) → ℝ) (hw : ∀ k, 0 < w k) (hz : ∀ k, 0 ≤ z k)
    (hsw : ∑ k, w k = 1) (hsz : ∑ k, z k = 1)
    (he : ∑ k, w k • F.point k = ∑ k, z k • G.point k) : F = G := by
…

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

  66. lemma OAI.SharpLiebThirring.CubeFlags.Flag.depth_lt_half_of_pos_zero line 593

    Source documentation

    The corner vertex controls strict distance from the midplanes.

    lemma Flag.depth_lt_half_of_pos_zero {n : ℕ} (F : Flag n)
    (w : Fin (n + 1) → ℝ) (hw : ∀ k, 0 ≤ w k) (h₀ : 0 < w 0)
    (hs : ∑ k, w k = 1) (i : Fin n) :
    F.depth i (∑ k, w k • F.point k) < 1 / 2 := by
…

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

  67. lemma OAI.SharpLiebThirring.CubeFlags.Flag.depth_pos_of_weight line 611
  68. lemma OAI.SharpLiebThirring.CubeFlags.Flag.depth_strictAnti_of_weight line 625
  69. lemma OAI.SharpLiebThirring.CubeFlags.Flag.eq_of_facet_combination line 645

    Source documentation

    Bottom-facet interiors are disjoint among flags on the same side of the bottom hyperplane. The last coordinate expanded is the time coordinate t.

    lemma Flag.eq_of_facet_combination {n : ℕ} [NeZero n] (F G : Flag n)
    (t : Fin n) (ht : (F.order.symm t).val = n - 1)
    (hbt : F.base t = G.base t) (hct : F.corner t = G.corner t)
    (w z : Fin (n + 1) → ℝ) (hw : ∀ k, 0 ≤ w k)
    (hwp : ∀ k, k ≠ Fin.last n → 0 < w k) (hz : ∀ k, 0 ≤ z k)
    (hsw : ∑ k, w k = 1) (hsz : ∑ k, z k = 1)
    (he : ∑ k, w k • F.point k = ∑ k, z k • G.point k) : F = G := by
…

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

  70. lemma OAI.SharpLiebThirring.CubeFlags.Flag.neighbor_ne_reflect_of_free line 726

    Source documentation

    A shared facet whose vertices have trivial stabilizers cannot identify its two incident flags under a reflection action. The hypothesis will be supplied by the positive distance from zero-row strata.

    lemma Flag.neighbor_ne_reflect_of_free {n : ℕ} [NeZero n] (F : Flag n)
    (j : Fin (n + 1)) (s : Signs n)
    (hfree : ∀ k : Fin (n + 1),
      (∀ i, (if s.val i then -F.vertex k i else F.vertex k i) = F.vertex k i) → s = 1) :
    F.neighbor j ≠ s • F := by
…

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