OAI/Analysis/FiniteFactor/Coupling/Limit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.CouplingParameters.infiniteEndpoint_density_of_prefix_bound line 13

   Source documentation

   Uniformly square-integrable finite endpoint densities produce an actual infinite-product density, with the same square-integral bound.

   theorem infiniteEndpoint_density_of_prefix_bound {ι : Type*}
       (p : ι → CouplingParameters) (right : ι → Bool) (I : ℕ → Finset ι)
       (hmono : Monotone I) (hcover : ∀ J : Finset ι, ∃ n, J ⊆ I n)
       (C : ℝ) (hb : ∀ n, (∫ x, prefixDensity p right (I n) x ^ 2
         ∂Measure.infinitePi (fun _ : ι => unitIntervalMeasure)) ≤ C) :
       ∃ g : (ι → ℝ) → ℝ,
         MemLp g 2 (Measure.infinitePi (fun _ : ι => unitIntervalMeasure)) ∧
         (∀ᵐ x ∂Measure.infinitePi (fun _ : ι => unitIntervalMeasure), 0 ≤ g x) ∧
         (∫ x, g x ^ 2 ∂Measure.infinitePi (fun _ : ι => unitIntervalMeasure)) ≤ C ∧
         Measure.infinitePi (fun i => (p i).selectedLaw true (right i)) =
           (Measure.infinitePi (fun _ : ι => unitIntervalMeasure)).withDensity
             (fun x => ENNReal.ofReal (g x)) := by
   …

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