awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
B :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
ω : Ω
hωpos :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
hωneg :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
h₁ :
  ∀ (x : ℕ),
    HDiv.hDiv (α := ℝ) (∑ i ∈ range x, X i ω) (↑x : ℝ) =
      HDiv.hDiv (α := ℝ) (∑ i ∈ range x, (pos ∘ X i) ω) (↑x : ℝ) -
        HDiv.hDiv (α := ℝ) (∑ i ∈ range x, (neg ∘ X i) ω) (↑x : ℝ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have h₂ : ∫ (x : Ω), X 0 x ∂μ =
  HSub.hSub (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a)
Tactic: convert! hωpos.sub hωneg using 2
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
have refine_1 : ∀ (c : E) {s : Set E} (hs : MeasurableSet s),
  (fun (ψ : SimpleFunc E E) ↦
      ∀ᵐ (ω : Ω) ∂μ,
        Tendsto.{0, u_2} (β := E)
          (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
          atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
    (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0))
Tactic: refine SimpleFunc.induction (motive := fun ψ ↦ ∀ᵐ ω ∂μ,
    Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, ψ (X i ω))) atTop (𝓝 μ[ψ ∘ (X 0)])) ?_ ?_ φ
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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
refine_1 :
  ∀ (c : E) {s : Set E} (hs : MeasurableSet s),
    (fun (ψ : SimpleFunc E E) ↦
        ∀ᵐ (ω : Ω) ∂μ,
          Tendsto.{0, u_2} (β := E)
            (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
            atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
      (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
have refine_2 : ∀ ⦃f g : SimpleFunc E E⦄,
  Disjoint (α := Set E) (Function.support (M := E) (⇑f : (a : E) → E)) (Function.support (M := E) (⇑g : (a : E) → E)) →
    (fun (ψ : SimpleFunc E E) ↦
          ∀ᵐ (ω : Ω) ∂μ,
            Tendsto.{0, u_2} (β := E)
              (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
              atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
        f →
      (fun (ψ : SimpleFunc E E) ↦
            ∀ᵐ (ω : Ω) ∂μ,
              Tendsto.{0, u_2} (β := E)
                (fun (n : ℕ) ↦
                  HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
                atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
          g →
        (fun (ψ : SimpleFunc E E) ↦
            ∀ᵐ (ω : Ω) ∂μ,
              Tendsto.{0, u_2} (β := E)
                (fun (n : ℕ) ↦
                  HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
                atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
          (f + g)
Tactic: refine SimpleFunc.induction (motive := fun ψ ↦ ∀ᵐ ω ∂μ,
    Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, ψ (X i ω))) atTop (𝓝 μ[ψ ∘ (X 0)])) ?_ ?_ φ
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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
⊢ ∀ᵐ (ω : Ω) ∂μ,
    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 ∂μ))
have 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) ∂μ))
Tactic: simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
      SimpleFunc.coe_zero, piecewise_eq_indicator, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
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
⊢ ∀ᵐ (ω : Ω) ∂μ,
    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) ∂μ))
have F_meas : Measurable F
Tactic: have F_meas : Measurable F := (measurable_indicator_const_iff 1).2 hs
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ∂μ))
have simp : ∀ᵐ (ω : Ω) ∂μ,
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, Y i ω) (↑n : ℝ)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
Tactic: simp only [smul_eq_mul, ← div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, Y i ω) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
have hint : Integrable (Y 0) μ
Tactic: apply strong_law_ae_real
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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) μ
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, Y i ω) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
have hindep₁ : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on Y)
Tactic: apply strong_law_ae_real
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, Y i ω) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
have hident₁ : ∀ (i : ℕ), IdentDistrib (Y i) (Y 0) μ μ
Tactic: apply strong_law_ae_real
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
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.{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) ∂μ))
have this : ∀ᵐ (ω : Ω) ∂μ,
  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
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    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) ∂μ))
have 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) ∂μ))
Tactic: filter_upwards [this] with ω hω
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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
have h : ∀ (x : E), s.indicator (Function.const E c) x = HSMul.hSMul (α := ℝ) (s.indicator 1 x) c
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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
⊢ s.indicator (Function.const E c) x = HSMul.hSMul (α := ℝ) (s.indicator 1 x) c
have h : s.indicator (Function.const E c) x = s.indicator (fun (x : E) ↦ HSMul.hSMul (α := ℝ) (1 x) c) x
Tactic: rw [← indicator_smul_const_apply]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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
⊢ s.indicator (Function.const E c) x = s.indicator (fun (x : E) ↦ HSMul.hSMul (α := ℝ) (1 x) c) x
have h : Function.const E c = fun (x : E) ↦ HSMul.hSMul (α := ℝ) (1 x) c
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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
⊢ Function.const E c = fun (x : E) ↦ HSMul.hSMul (α := ℝ) (1 x) c
have h : ∀ (x : E), Function.const E c x = HSMul.hSMul (α := ℝ) (1 x) c
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
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 ∂μ))
⊢ 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) ∂μ))
have I : 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
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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.{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) ∂μ))
have 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))
Tactic: simp only [I, integral_smul_const]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 (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))
have 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
Tactic: convert! Tendsto.smul_const hω c using 1