LeanMachineLearning exposition

hasLaw_eval_infinitePi🔗

Minimal Lean file

hasLaw_eval_infinitePi🔗

LemmahasLaw_eval_infinitePi
Details

No docstring.

🔗theorem
hasLaw_eval_infinitePi.{u_3, u_4} {ι : Type u_3} {X : ι → Type u_4}
  {mX : (i : ι) → MeasurableSpace (X i)}
  (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (i : ι) :
  ProbabilityTheory.HasLaw (Function.eval i) (μ i)
    (MeasureTheory.Measure.infinitePi μ)
hasLaw_eval_infinitePi.{u_3, u_4}
  {ι : Type u_3} {X : ι → Type u_4}
  {mX : (i : ι) → MeasurableSpace (X i)}
  (μ :
    (i : ι) → MeasureTheory.Measure (X i))
  [hμ :
    ∀ (i : ι),
      MeasureTheory.IsProbabilityMeasure
        (μ i)]
  (i : ι) :
  ProbabilityTheory.HasLaw
    (Function.eval i) (μ i)
    (MeasureTheory.Measure.infinitePi μ)

Code

lemma _root_.hasLaw_eval_infinitePi {ι : Type*} {X : ι → Type*} {mX : ∀ i, MeasurableSpace (X i)}
  (μ : (i : ι) → Measure (X i)) [hμ : ∀ i, IsProbabilityMeasure (μ i)] (i : ι) :
    HasLaw (Function.eval i) (μ i) (Measure.infinitePi μ) where
  aemeasurable
Used by (2)

Actions: Source · Open Issue

Proof
Measurable.aemeasurable (by fun_prop)
  map_eq := by exact (measurePreserving_eval_infinitePi μ i).map_eq