OAI/Topology/ArtinGroups/ParabolicIntersections/PointedMultiplicity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Layer counts of the pointed categorical family, at every integer level.

  1. def OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity line 21
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity_nonneg line 24
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedFamily_word line 27
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity_sum line 35
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity_values_finite line 43

    Source documentation

    Bounded count intervals contain only finitely many actual count values.

    lemma pointedMultiplicity_values_finite (f : S) (B : ℝ) :
    {r : ℝ | r ≤ B ∧ ∃ x k v, r = pointedMultiplicity M f x k v}.Finite := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity

  6. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity_support_finite line 52
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity_exterior line 68

    Source documentation

    The relative family changes no count outside the operated standard subgroup.

    lemma pointedMultiplicity_exterior (J : Set S) (g : Artin M)
    (hg : g ∈ artinParabolic M J) (f : S) (x : Artin M)
    (v : S ⊕ Unit) (hv : v ∉ Sum.inl '' J) (k : ℤ) :
    pointedMultiplicity M f (g * x) k v = pointedMultiplicity M f x k v := by
…

    Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity

  8. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity_frame line 81

    Source documentation

    A frame color outside the operated type retains its unique level-zero count.

    lemma pointedMultiplicity_frame (J : Set S) (f : S) (hf : f ∉ J)
    (x : Artin M) (hx : x ∈ artinParabolic M J) (k : ℤ) :
    pointedMultiplicity M f x k (.inl f) = if k = 0 then 1 else 0 := by
…

    Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.pointedMultiplicity