ExactInvariantFunctions.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Pointwise invariant versions under a Haar measure class

The version is formed by averaging only on orbits where the observable is almost everywhere constant. Those orbits form an exactly invariant measurable set. This avoids an intersection of uncountably many conull sets and does not assume amenability of the acting group.

def OAI.DukePrimeDegree.orbitConstantMean line 26
def OAI.DukePrimeDegree.orbitConstantSet line 29
lemma OAI.DukePrimeDegree.measurable_orbitConstantMean line 32
lemma OAI.DukePrimeDegree.measurableSet_orbitConstantSet line 39
lemma OAI.DukePrimeDegree.orbitConstantMean_smul_of_mem line 57
lemma OAI.DukePrimeDegree.smul_mem_orbitConstantSet line 66

theorem OAI.DukePrimeDegree.exists_pointwise_invariant_version_of_probability_class line 83

Source documentation

A probability in a right-translation invariant measure class gives an exactly invariant measurable version of an almost invariant real observable. The observable need not be globally bounded.

theorem exists_pointwise_invariant_version_of_probability_class
    (ρ : Measure H) [IsProbabilityMeasure ρ]
    (hρ : ∀ g : H, QuasiMeasurePreserving (fun h : H => h * g) ρ ρ)
    (μ : Measure Y) [SFinite μ]
    (hsmul : Measurable (fun p : H × Y => p.1 • p.2))
    (f : Y → ℝ) (hf : Measurable f)
    (hfix : ∀ h : H, (fun x : Y => f (h • x)) =ᵐ[μ] f) :
    ∃ f₀ : Y → ℝ, Measurable[PrimeDegreePackets.actionInvariantSigma H Y] f₀ ∧
      f₀ =ᵐ[μ] f ∧ ∀ (h : H) (x : Y), f₀ (h • x) = f₀ x := by
…

Mentions: OAI.PrimeDegreePackets.actionInvariantSigma

theorem OAI.DukePrimeDegree.exists_probability_right_quasiInvariant_measure line 121

Source documentation

Normalize the finite measure previously constructed from Haar. This is an actual probability measure, not a probability input.

theorem exists_probability_right_quasiInvariant_measure
    [MeasurableMul₂ H] [MeasurableInv H] (haar : Measure H) [SFinite haar]
    [haar.IsMulLeftInvariant] (hhaar : haar ≠ 0) :
    ∃ ρ : Measure H, IsProbabilityMeasure ρ ∧
      ∀ g : H, QuasiMeasurePreserving (fun h : H => h * g) ρ ρ := by
…

theorem OAI.DukePrimeDegree.exists_pointwise_invariant_version_of_haar line 133