InvariantDisintegration.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Conditional measures over an invariant measurable factor

Disintegrating the graph of an invariant measurable map gives a measurable probability kernel with the original measure as barycenter. Uniqueness of conditional kernels proves invariance of its components almost everywhere, for each acting element. No ergodicity is assumed here.

def OAI.PolycyclicRecognition.factorGraphMeasure line 27
Source documentation
The graph measure, with the factor in the first coordinate.
```
def factorGraphMeasure (_hf : Measurable f) : Measure (Y × X) := μ.map (fun x => (f x, x))
…
```
instance OAI.PolycyclicRecognition.factorGraphMeasure_probability line 31
def OAI.PolycyclicRecognition.factorConditionalKernel line 36
Source documentation
The actual conditional probability kernel supplied by disintegration.
```
def factorConditionalKernel (hf : Measurable f) : Kernel Y X := (factorGraphMeasure μ f hf).condKernel
```
Mentions: OAI.PolycyclicRecognition.factorGraphMeasure
instance OAI.PolycyclicRecognition.factorConditionalKernel_markov line 38
theorem OAI.PolycyclicRecognition.factorGraphMeasure_fst line 43
theorem OAI.PolycyclicRecognition.factorConditionalKernel_disintegrate line 48
theorem OAI.PolycyclicRecognition.factorConditionalKernel_barycenter line 55
Source documentation
Conditioning preserves the original measure as its setwise barycenter.
```
theorem factorConditionalKernel_barycenter (s : Set X) (hs : MeasurableSet s) :
    μ s = ∫⁻ x, factorConditionalKernel μ f hf (f x) s ∂μ := by
…
```
Mentions: OAI.PolycyclicRecognition.factorConditionalKernel

theorem OAI.PolycyclicRecognition.factorGraphMeasure_map_smul line 69

Source documentation

An invariant factor makes the graph measure invariant in its second coordinate.

theorem factorGraphMeasure_map_smul [SMulInvariantMeasure G X μ]
    (hfi : ∀ (g : G) (s : Set Y), MeasurableSet s →
      ∀ x, f (g • x) ∈ s ↔ f x ∈ s) (g : G) :
    (factorGraphMeasure μ f hf).map (Prod.map id (g • ·)) = factorGraphMeasure μ f hf := by
…

Mentions: OAI.PolycyclicRecognition.factorGraphMeasure

theorem OAI.PolycyclicRecognition.factorConditionalKernel_map_smul_ae line 89

Source documentation

Each fixed acting element preserves almost every conditional probability.

theorem factorConditionalKernel_map_smul_ae [SMulInvariantMeasure G X μ]
    (hfi : ∀ (g : G) (s : Set Y), MeasurableSet s →
      ∀ x, f (g • x) ∈ s ↔ f x ∈ s) (g : G) :
    ∀ᵐ y ∂μ.map f,
      (factorConditionalKernel μ f hf y).map (g • ·) = factorConditionalKernel μ f hf y := by
…

Mentions: OAI.PolycyclicRecognition.factorConditionalKernel

theorem OAI.PolycyclicRecognition.factorConditionalKernel_invariant_ae line 106

Source documentation

A countable action has invariant conditional probabilities almost everywhere.

theorem factorConditionalKernel_invariant_ae [Countable G] [SMulInvariantMeasure G X μ]
    (hfi : ∀ (g : G) (s : Set Y), MeasurableSet s →
      ∀ x, f (g • x) ∈ s ↔ f x ∈ s) :
    ∀ᵐ y ∂μ.map f, SMulInvariantMeasure G X (factorConditionalKernel μ f hf y) := by
…

Mentions: OAI.PolycyclicRecognition.factorConditionalKernel