OrbitAverageIntegral.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrals of finite orbit averages

Convex averaging preserves integrals against an invariant measure, including its restriction to an almost invariant measurable set.

theorem OAI.PolycyclicRecognition.smulInvariantMeasure_restrict_ae line 24

Source documentation

Restricting an invariant measure to an almost invariant set is invariant.

theorem smulInvariantMeasure_restrict_ae (s : Set X) (hs : MeasurableSet s)
    (hi : ∀ g : G, (g • ·) ⁻¹' s =ᵐ[ν] s) : SMulInvariantMeasure G X (ν.restrict s) := by
…

theorem OAI.PolycyclicRecognition.FiniteOrbitAverage.lintegral line 32

Source documentation

Finite convex averaging preserves every nonnegative integral.

theorem FiniteOrbitAverage.lintegral (A : FiniteOrbitAverage G) (f : X → ℝ)
    (hf : Measurable f) (hn : ∀ x, 0 ≤ f x) :
    (∫⁻ x, ENNReal.ofReal (A.apply f x) ∂ν) = ∫⁻ x, ENNReal.ofReal (f x) ∂ν := by
…

Mentions: OAI.PolycyclicRecognition.FiniteOrbitAverage