OAI/Topology/ArtinGroups/ParabolicIntersections/PointedProfile.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Harmonic profiles on actual parabolic cosets for a relative frame.

  1. def OAI.HarmonicArtin.ParabolicIntersections.pointedHarmonicAt line 14
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedHarmonicAt_outside line 17
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedHarmonicAt_nonneg line 22
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedHarmonicAt_harmonic line 27
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedHarmonicAt_invariant line 32
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedHarmonicAt_of_mem line 39
  7. def OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector line 45
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_eq line 48
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_nonneg line 53
  10. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_harmonic line 57
  11. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_support_finite line 61
  12. def OAI.HarmonicArtin.ParabolicIntersections.pointedCosetSum line 71
  13. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_le_sum line 74
  14. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_bounded_finite line 78
  15. def OAI.HarmonicArtin.ParabolicIntersections.pointedProfile line 104

    Source documentation

    Shift the fixed integer cutoff to zero while retaining every recorded level.

    noncomputable def pointedProfile (P : Deligne M) (cutoff : ℤ) : ℕ →₀ (S ⊕ Unit → ℝ) :=
…

    Mentions: OAI.HarmonicArtin.Deligne

  16. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedProfile_apply line 110