ConditionalPairs.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Pairs sampled from a conditional measure

Resampling the second coordinate from its conditional distribution preserves both coordinate marginals. These pairs let the Hopf principle apply inside a foliation chart, with both ambient marginals dominated by the original finite invariant measure.

def OAI.DukePrimeDegree.conditionalPairMeasure line 25
Source documentation
Keep the transverse coordinate and independently resample the leaf coordinate using its conditional law.
```
noncomputable def conditionalPairMeasure (ρ : Measure (S × B)) [IsFiniteMeasure ρ] :
    Measure ((S × B) × B) :=
…
```
instance OAI.DukePrimeDegree.(instance at line 29) line 29
lemma OAI.DukePrimeDegree.conditionalPairMeasure_left line 34
lemma OAI.DukePrimeDegree.conditionalPairMeasure_right line 38
lemma OAI.DukePrimeDegree.map_conditionalPair_left line 51
lemma OAI.DukePrimeDegree.map_conditionalPair_right line 58

lemma OAI.DukePrimeDegree.ae_conditionalPair_of_ambient line 69

Source documentation

An ambient almost-everywhere property holds at both sampled points.

lemma ae_conditionalPair_of_ambient (ρ : Measure (S × B)) [IsFiniteMeasure ρ]
    {P : S × B → Prop} (hP : ∀ᵐ z ∂ρ, P z) :
    ∀ᵐ z ∂conditionalPairMeasure ρ, P z.1 ∧ P (z.1.1, z.2) := by
…

Mentions: OAI.DukePrimeDegree.conditionalPairMeasure

theorem OAI.DukePrimeDegree.ae_conditionalPair_eq_of_asymptotic_orbits line 84

Source documentation

A chart whose same-fiber point pairs become asymptotic carries constant conditional values for every integrable invariant observable. The conclusion is with respect to the actual conditional kernel.

theorem ae_conditionalPair_eq_of_asymptotic_orbits
    {α : Type*} [UniformSpace α] [T2Space α] [NormalSpace α]
    [WeaklyLocallyCompactSpace α] [MeasurableSpace α] [BorelSpace α]
    (μ : Measure α) [μ.Regular]
    (ρ : Measure (S × B)) [IsFiniteMeasure ρ]
    (R : S × B → α) (hR : Measurable R) (hRμ : ρ.map R ≤ μ)
    (T : α → α) (hT : MeasurePreserving T μ μ)
    (hasymptotic : ∀ᵐ z ∂conditionalPairMeasure ρ,
      Tendsto (fun n => (T^[n] (R z.1), T^[n] (R (z.1.1, z.2)))) atTop (𝓤 α))
    (f : α → ℝ) (hf : Integrable f μ) (hfinv : (fun x => f (T x)) =ᵐ[μ] f) :
    ∀ᵐ z ∂conditionalPairMeasure ρ, f (R z.1) = f (R (z.1.1, z.2)) := by
…

Mentions: OAI.DukePrimeDegree.conditionalPairMeasure

theorem OAI.DukePrimeDegree.ae_conditional_eq_of_asymptotic_orbits line 107