production module

`AutoSamplingTheory.TechnicalLemmas.Probability.FiniteProductSupport`

2 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Probability/FiniteProductSupport.lean.

Imports

Mathlib.MeasureTheory.Measure.FiniteMeasurePi externalMathlib.MeasureTheory.Measure.Typeclasses.Probability external

Imported by

AutoSamplingTheory.TechnicalLemmas.Analysis.CyclicCostExpectationAutoSamplingTheory.TechnicalLemmas.ProbabilityTests.FiniteProductSupport

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Probability.FiniteProductSupport.pi_box_apply_eq_one Partial Not mapped

- Coordinate probability-one sets form a probability-one box.

theorem pi_box_apply_eq_one
    (mu : ∀ i, ProbabilityMeasure (X i)) (s : ∀ i, Set (X i))
    (hs : ∀ i, mu i (s i) = 1) :
    ProbabilityMeasure.pi mu (Set.pi Set.univ s) = 1 := by
  rw [ProbabilityMeasure.pi_pi]
  simp [hs]

/-- Under coordinate measurability, the product tuple belongs to the
probability-one box almost surely. -/

AutoSamplingTheory/TechnicalLemmas/Probability/FiniteProductSupport.lean:29published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Probability.FiniteProductSupport.ae_mem_pi_box Partial Not mapped

- Under coordinate measurability, the product tuple belongs to the probability-one box almost surely.

theorem ae_mem_pi_box
    (mu : ∀ i, ProbabilityMeasure (X i)) (s : ∀ i, Set (X i))
    (hmeas : ∀ i, MeasurableSet (s i))
    (hs : ∀ i, mu i (s i) = 1) :
    ∀ᵐ x ∂(ProbabilityMeasure.pi mu : Measure (∀ i, X i)),
      x ∈ Set.pi Set.univ s := by
  have hbox : MeasurableSet (Set.pi Set.univ s) :=
    MeasurableSet.pi countable_univ (fun i _hi => hmeas i)
  apply (mem_ae_iff_prob_eq_one hbox).2
  rw [← ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure]
  simp [pi_box_apply_eq_one mu s hs]

end

end FiniteProductSupport
end Probability
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Probability/FiniteProductSupport.lean:38published source at 0e31a3cda412