OAI/NumberTheory/DukePrimeDegree/Geometry/LeafNormalizationInjectivity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Recovering normalized leaf measures from based leaves

Two leaf measures normalized on the same window agree if their based normalizations agree at one center of positive finite mass. This removes the projective scalar when applying intrinsic holonomy inside a box.

  1. theorem OAI.DukePrimeDegree.eq_of_anchorNormalize_eq line 20
  2. theorem OAI.DukePrimeDegree.eq_of_basedRealMeasure_eq line 29
  3. theorem OAI.DukePrimeDegree.eq_of_rebasedRealMeasure_eq line 53

    Source documentation

    Holonomy may compare two different centers. Normalizing both original measures on the same window still removes the projective scalar.

    theorem eq_of_rebasedRealMeasure_eq
    (ν ρ : Measure ℝ) [IsLocallyFiniteMeasure ν] [IsLocallyFiniteMeasure ρ]
    (S : Set ℝ) (hνS : ν S = 1) (hρS : ρ S = 1) (t u : ℝ)
    (hνt : 0 < ν (Metric.ball t 1)) (hρu : 0 < ρ (Metric.ball u 1))
    (h : basedRealMeasure ρ u = basedRealMeasure (basedRealMeasure ν t) (u - t)) :
    ν = ρ := by
…