OAI/Analysis/FiniteFactor/Coupling/Prefix.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.integral_infinitePi_finset_prod line 12

   Source documentation

   Finite-coordinate factorization under the actual infinite product measure.

   theorem integral_infinitePi_finset_prod {ι : Type*} {X : ι → Type*}
       [∀ i, MeasurableSpace (X i)] (μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)]
       (I : Finset ι) (f : ∀ i, X i → ℝ) (hf : ∀ i, Measurable (f i)) :
       (∫ x, ∏ i ∈ I, f i (x i) ∂Measure.infinitePi μ) = ∏ i ∈ I, ∫ t, f i t ∂μ i := by
   …

2. def OAI.FiniteFactor.CouplingParameters.prefixDensity line 30
3. theorem OAI.FiniteFactor.CouplingParameters.prefixDensity_measurable line 33
4. theorem OAI.FiniteFactor.CouplingParameters.prefixDensity_nonneg line 37
5. theorem OAI.FiniteFactor.CouplingParameters.prefixDensity_memLp line 41
6. theorem OAI.FiniteFactor.CouplingParameters.prefixDensity_integral line 53
7. theorem OAI.FiniteFactor.CouplingParameters.prefixDensity_sq_integral line 59
8. theorem OAI.FiniteFactor.CouplingParameters.prefixDensity_energy line 65
9. theorem OAI.FiniteFactor.CouplingParameters.prefixDensity_inner line 75

   Source documentation

   Exact orthogonality identity for nested finite product densities.

   theorem prefixDensity_inner (p : ι → CouplingParameters) (right : ι → Bool)
       {I J : Finset ι} (hIJ : I ⊆ J) :
       (∫ x, prefixDensity p right I x * prefixDensity p right J x
         ∂Measure.infinitePi (fun _ : ι => unitIntervalMeasure)) =
       ∫ x, prefixDensity p right I x ^ 2 ∂Measure.infinitePi (fun _ : ι => unitIntervalMeasure) := by
   …

   Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.prefixDensity, OAI.FiniteFactor.unitIntervalMeasure

10. theorem OAI.FiniteFactor.CouplingParameters.prefixDensity_cylinder line 117

    Source documentation

    The lifted prefix density has exactly the finite endpoint law on every Borel cylinder at that prefix.

    theorem prefixDensity_cylinder (p : ι → CouplingParameters) (right : ι → Bool)
        (I : Finset ι) {S : Set (I → ℝ)} (hS : MeasurableSet S) :
        ENNReal.ofReal (∫ x in (I.restrict (π := fun _ : ι => ℝ)) ⁻¹' S, prefixDensity p right I x
    …

    Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.prefixDensity

11. theorem OAI.FiniteFactor.CouplingParameters.prefixDensity_cylinder_of_subset line 136

    Source documentation

    Enlarging the prefix does not change any earlier cylinder law.

    theorem prefixDensity_cylinder_of_subset (p : ι → CouplingParameters) (right : ι → Bool)
        {J I : Finset ι} (hJI : J ⊆ I) {S : Set (J → ℝ)} (hS : MeasurableSet S) :
        ENNReal.ofReal (∫ x in (J.restrict (π := fun _ : ι => ℝ)) ⁻¹' S, prefixDensity p right I x
    …

    Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.prefixDensity