PointedBoundaryZero.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The all-level connected-support argument in the nonspherical case of §8.

theorem OAI.HarmonicArtin.ParabolicIntersections.orbit_boundary_zero_interior_zero line 19

Source documentation

An unoperated exterior frame and an empty boundary exclude every interior generator, including generators below the harmonic cutoff.

theorem orbit_boundary_zero_interior_zero (w : List (V × Bool)) (s : V)
    (hw : ∀ a ∈ w, a.1 ≠ s) (U : Set V) (hs : s ∉ U)
    (hz : ∀ k v, v ∉ U → (∃ u ∈ U, fusionFoldedCartan m d v u < 0) →
      fusionOrbitMultiplicity m d hd hdiag hm w s k v = 0) :
    ∀ k v, v ∈ U → fusionOrbitMultiplicity m d hd hdiag hm w s k v = 0 := by
…

Mentions: OAI.HarmonicArtin.fusionFoldedCartan, OAI.HarmonicArtin.fusionOrbitMultiplicity

theorem OAI.HarmonicArtin.ParabolicIntersections.pointed_boundary_zero_interior_zero line 47
Source documentation
Connectedness of the actual pointed family converts an all-level exterior boundary vanishing statement to interior vanishing.
```
theorem pointed_boundary_zero_interior_zero (x : Artin M)
    (hx : x ∈ artinParabolic M {f}ᶜ) (K : Set S) (hf : f ∉ K)
    (hz : ∀ k v, v ∉ Sum.inl '' K →
      (∃ u ∈ Sum.inl '' K, framedCartan M v u < 0) →
      pointedMultiplicity M f x k v = 0) :
    ∀ k i, i ∈ K → pointedMultiplicity M f x k (.inl i) = 0 := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.framedCartan, OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity
theorem OAI.HarmonicArtin.ParabolicIntersections.pointed_negativeTwist_of_zero line 71
Source documentation
Termwise absence in a closed neighborhood makes its negative twists identity maps on each member of the pointed family.
```
theorem pointed_negativeTwist_of_zero (x : Artin M) (K : Set S)
    (hz : ∀ k v, v ∈ Sum.inl '' K ∨
      (∃ u ∈ Sum.inl '' K, framedCartan M v u < 0) →
      pointedMultiplicity M f x k v = 0)
    (i : S) (hi : i ∈ K) (L H : FusionLabel m) :
    classNegativeTwist Q (.inl i, L) (pointedFamily M f x H) = pointedFamily M f x H := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.framedCartan, OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity, OAI.HarmonicArtin.FusionLabel, OAI.HarmonicArtin.ParabolicIntersections.pointedFamily
theorem OAI.HarmonicArtin.ParabolicIntersections.pointed_standard_fixes_of_closed_zero line 121
Source documentation
Vanishing on a full closed neighborhood makes the standard subgroup fix the actual family, with no restriction on the levels.
```
theorem pointed_standard_fixes_of_closed_zero (x : Artin M) (K : Set S)
    (hz : ∀ k v, v ∈ Sum.inl '' K ∨
      (∃ u ∈ Sum.inl '' K, framedCartan M v u < 0) →
      pointedMultiplicity M f x k v = 0)
    (g : Artin M) (hg : g ∈ artinParabolic M K) :
    pointedFamily M f (g * x) = pointedFamily M f x := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.framedCartan, OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.pointedFamily