RelativeInvisibleFactor.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Removing the all-level invisible factor in the nonspherical case of §8.

def OAI.HarmonicArtin.ParabolicIntersections.ExteriorCutoff line 15
Source documentation
Every exterior count below the cutoff is zero. The cutoff is chosen from the actual finite family, independently of the harmonic minimum.
```
def ExteriorCutoff (Y : Set S) (x : Artin M) (cutoff : ℤ) : Prop :=
…
```
Mentions: OAI.HarmonicArtin.Artin
lemma OAI.HarmonicArtin.ParabolicIntersections.exteriorCutoff_exists line 18
lemma OAI.HarmonicArtin.ParabolicIntersections.relative_profile_exterior line 30
lemma OAI.HarmonicArtin.ParabolicIntersections.relative_invisible_boundary_zero line 45
Source documentation
If the containing type is the whole acting type, every exterior neighbor of the invisible set is absent at every level.
```
lemma relative_invisible_boundary_zero {Y : Set S} {x : Artin M}
    (P : RelativeVertex M Y x) (cutoff : ℤ) (hcut : ExteriorCutoff M f Y x cutoff)
    (hfull : relativeContainingType M f cutoff Y P.val = Y) :
    ∀ k v, v ∉ Sum.inl '' relativeInvisible M f cutoff Y P.val →
      (∃ u ∈ Sum.inl '' relativeInvisible M f cutoff Y P.val, framedCartan M v u < 0) →
      pointedMultiplicity M f x k v = 0 := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.RelativeVertex, OAI.HarmonicArtin.ParabolicIntersections.ExteriorCutoff, OAI.HarmonicArtin.ParabolicIntersections.relativeContainingType, OAI.HarmonicArtin.ParabolicIntersections.relativeInvisible, OAI.HarmonicArtin.framedCartan, OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity
theorem OAI.HarmonicArtin.ParabolicIntersections.relative_invisible_factor_fixes line 79
Source documentation
The entire invisible factor fixes the family, even below the cutoff. This is the additional step after Proposition 6.9 in the proof of Theorem 8.2.
```
theorem relative_invisible_factor_fixes {Y : Set S} {x : Artin M}
    (hf : f ∉ Y) (hx : x ∈ artinParabolic M {f}ᶜ)
    (P : RelativeVertex M Y x) (cutoff : ℤ) (hcut : ExteriorCutoff M f Y x cutoff)
    (hfull : relativeContainingType M f cutoff Y P.val = Y)
    (g : Artin M) (hg : g ∈ artinParabolic M (relativeInvisible M f cutoff Y P.val)) :
    pointedFamily M f (g*x) = pointedFamily M f x := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.RelativeVertex, OAI.HarmonicArtin.ParabolicIntersections.ExteriorCutoff, OAI.HarmonicArtin.ParabolicIntersections.relativeContainingType, OAI.HarmonicArtin.ParabolicIntersections.relativeInvisible, OAI.HarmonicArtin.ParabolicIntersections.pointedFamily
theorem OAI.HarmonicArtin.ParabolicIntersections.relative_nonspherical_reduction line 101
Source documentation
The nonspherical case is reduced to a proper containing type or to a proper spherical visible factor; no new containment is assumed.
```
theorem relative_nonspherical_reduction {Y : Set S} {x : Artin M}
    (hf : f ∉ Y) (hx : x ∈ artinParabolic M {f}ᶜ) (hY : ¬IsSpherical M Y) :
    ReductionAt M (pointedInitial M f) Y x := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.IsSpherical, OAI.HarmonicArtin.ParabolicIntersections.ReductionAt, OAI.HarmonicArtin.ParabolicIntersections.pointedInitial