awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
refine_1 :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦
        HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ x ∈ Finset.range n, s.indicator (Function.const E c) (X x ω)))
      atTop (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦
        HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹
          (∑ i ∈ Finset.range n,
            (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0) : (a : E) → E) (X i ω)))
      atTop
      (𝓝
        (∫ (x : Ω),
          ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) : (a : E) → E) ∘ X 0) x ∂μ))

Tactic:
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
      SimpleFunc.coe_zero, piecewise_eq_indicator, Function.comp_apply]

Premises used: MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, Function.comp_apply, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, MeasureTheory.SimpleFunc.coe_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
⊢ Measurable F

Tactic:
have F_meas : Measurable F := (measurable_indicator_const_iff 1).2 hs
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
simp :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, Y i ω) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))

Tactic:
simp only [smul_eq_mul, ← div_eq_inv_mul]

Premises used: smul_eq_mul, div_eq_inv_mul
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
hint : Integrable (Y 0) μ
hindep₁ : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on Y)
hident₁ : ∀ (i : ℕ), IdentDistrib (Y i) (Y 0) μ μ
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, Y i ω) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))

Tactic:
apply strong_law_ae_real

Premises used: ProbabilityTheory.strong_law_ae_real
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
⊢ Integrable (Y 0) μ

Tactic:
SimpleFunc.integrable_of_isFiniteMeasure
          ((SimpleFunc.piecewise s hs (SimpleFunc.const _ (1 : ℝ))
            (SimpleFunc.const _ (0 : ℝ))).comp (X 0) h')

Premises used: MeasureTheory.SimpleFunc.const, Set.indicator, MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure, Set.piecewise, OfNat.ofNat, MeasureTheory.SimpleFunc.comp, MeasureTheory.SimpleFunc.piecewise, ite
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
⊢ Integrable (Y 0) μ

Tactic:
exact SimpleFunc.integrable_of_isFiniteMeasure
          ((SimpleFunc.piecewise s hs (SimpleFunc.const _ (1 : ℝ))
            (SimpleFunc.const _ (0 : ℝ))).comp (X 0) h')

Premises used: MeasureTheory.SimpleFunc.const, MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure, OfNat.ofNat, MeasureTheory.SimpleFunc.comp, MeasureTheory.SimpleFunc.piecewise
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
⊢ Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on Y)

Tactic:
fun i j hij ↦ IndepFun.comp (hindep hij) F_meas F_meas

Premises used: ProbabilityTheory.IndepFun.comp, Pairwise
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
⊢ Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on Y)

Tactic:
exact fun i j hij ↦ IndepFun.comp (hindep hij) F_meas F_meas

Premises used: ProbabilityTheory.IndepFun.comp
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
⊢ ∀ (i : ℕ), IdentDistrib (Y i) (Y 0) μ μ

Tactic:
fun i ↦ (hident i).comp F_meas

Premises used: ProbabilityTheory.IdentDistrib.comp
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
⊢ ∀ (i : ℕ), IdentDistrib (Y i) (Y 0) μ μ

Tactic:
exact fun i ↦ (hident i).comp F_meas

Premises used: ProbabilityTheory.IdentDistrib.comp
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))

Tactic:
have : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ (n : ℝ)⁻¹ • ∑ i ∈ Finset.range n, Y i ω)
        atTop (𝓝 μ[Y 0]) := by
      simp only [smul_eq_mul, ← div_eq_inv_mul]
      apply strong_law_ae_real
      · exact SimpleFunc.integrable_of_isFiniteMeasure
          ((SimpleFunc.piecewise s hs (SimpleFunc.const _ (1 : ℝ))
            (SimpleFunc.const _ (0 : ℝ))).comp (X 0) h')
      · exact fun i j hij ↦ IndepFun.comp (hindep hij) F_meas F_meas
      · exact fun i ↦ (hident i).comp F_meas
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
h :
  ∀ (ω : Ω)
    (hω :
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
        (𝓝 (∫ (x : Ω), Y 0 x ∂μ))),
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦
        HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ x ∈ Finset.range n, s.indicator (Function.const E c) (X x ω)))
      atTop (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦
        HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ x ∈ Finset.range n, s.indicator (Function.const E c) (X x ω)))
      atTop (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))

Tactic:
filter_upwards [this] with ω hω
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
h : ∀ (x : E), s.indicator (Function.const E c) x = HSMul.hSMul (α := ℝ) (s.indicator 1 x) c
⊢ s.indicator (Function.const E c) = fun (x : E) ↦ HSMul.hSMul (α := ℝ) (s.indicator 1 x) c

Tactic:
ext
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
x : E
h : s.indicator (Function.const E c) x = s.indicator (fun (x : E) ↦ HSMul.hSMul (α := ℝ) (1 x) c) x
⊢ s.indicator (Function.const E c) x = HSMul.hSMul (α := ℝ) (s.indicator 1 x) c

Tactic:
rw [← indicator_smul_const_apply]

Premises used: Set.indicator_smul_const_apply
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
x : E
h : Function.const E c = fun (x : E) ↦ HSMul.hSMul (α := ℝ) (1 x) c
⊢ s.indicator (Function.const E c) x = s.indicator (fun (x : E) ↦ HSMul.hSMul (α := ℝ) (1 x) c) x

Tactic:
congr! 1
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
x : E
h : ∀ (x : E), Function.const E c x = HSMul.hSMul (α := ℝ) (1 x) c
⊢ Function.const E c = fun (x : E) ↦ HSMul.hSMul (α := ℝ) (1 x) c

Tactic:
ext
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
x x_1 : E
⊢ Function.const E c x_1 = HSMul.hSMul (α := ℝ) (1 x_1) c

Tactic:
simp
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
⊢ s.indicator (Function.const E c) = fun (x : E) ↦ HSMul.hSMul (α := ℝ) (s.indicator 1 x) c

Tactic:
have I : indicator s (Function.const E c) = (fun x ↦ (indicator s (1 : E → ℝ) x) • c) := by
      ext
      rw [← indicator_smul_const_apply]
      congr! 1
      ext
      simp
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
I : s.indicator (Function.const E c) = fun (x : E) ↦ HSMul.hSMul (α := ℝ) (s.indicator 1 x) c
h :
  Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ x ∈ Finset.range n, HSMul.hSMul (α := ℝ) (s.indicator 1 (X x ω)) c))
    atTop (𝓝 (HSMul.hSMul (α := ℝ) (∫ (x : Ω), s.indicator 1 (X 0 x) ∂μ) c))
⊢ Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦
      HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ x ∈ Finset.range n, s.indicator (Function.const E c) (X x ω)))
    atTop (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))

Tactic:
simp only [I, integral_smul_const]

Premises used: integral_smul_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
I : s.indicator (Function.const E c) = fun (x : E) ↦ HSMul.hSMul (α := ℝ) (s.indicator 1 x) c
⊢ Tendsto (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑x : ℝ)⁻¹ (∑ i ∈ Finset.range x, Y i ω) • c) atTop
    (𝓝 (HSMul.hSMul (α := ℝ) (∫ (x : Ω), Y 0 x ∂μ) c))

Tactic:
Tendsto.smul_const hω c

Premises used: Filter.Tendsto.smul_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
I : s.indicator (Function.const E c) = fun (x : E) ↦ HSMul.hSMul (α := ℝ) (s.indicator 1 x) c
h :
  Eq.{u_2 + 1} (α := ℕ → E)
    (fun (n : ℕ) ↦
      HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ x ∈ Finset.range n, HSMul.hSMul (α := ℝ) (s.indicator 1 (X x ω)) c))
    fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑x : ℝ)⁻¹ (∑ i ∈ Finset.range x, Y i ω) • c
⊢ Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ x ∈ Finset.range n, HSMul.hSMul (α := ℝ) (s.indicator 1 (X x ω)) c))
    atTop (𝓝 (HSMul.hSMul (α := ℝ) (∫ (x : Ω), s.indicator 1 (X 0 x) ∂μ) c))

Tactic:
convert! Tendsto.smul_const hω c using 1

Premises used: Filter.Tendsto.smul_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun (n : ℕ) ↦ F ∘ X n
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
I : s.indicator (Function.const E c) = fun (x : E) ↦ HSMul.hSMul (α := ℝ) (s.indicator 1 x) c
⊢ Eq.{u_2 + 1} (α := ℕ → E)
    (fun (n : ℕ) ↦
      HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ x ∈ Finset.range n, HSMul.hSMul (α := ℝ) (s.indicator 1 (X x ω)) c))
    fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑x : ℝ)⁻¹ (∑ i ∈ Finset.range x, Y i ω) • c

Tactic:
simp [F, Y, ← sum_smul, smul_smul]

Premises used: Finset.sum_smul, smul_smul