awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun (i : ℕ) ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
C :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω))
      atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
h₁ : ∀ (n : ℕ), X n ω = Y n ω
h₂ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω), X 0 x ∂μ) (∫ (x : Ω), Y 0 x ∂μ)

Tactic:
have : μ[X 0] = μ[Y 0] := integral_congr_ae (AEStronglyMeasurable.ae_eq_mk (A 0).1)
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this_1 : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun (i : ℕ) ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
C :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω))
      atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
h₁ : ∀ (n : ℕ), X n ω = Y n ω
h₂ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
this : Eq.{u_2 + 1} (α := E) (∫ (x : Ω), X 0 x ∂μ) (∫ (x : Ω), Y 0 x ∂μ)
h₃ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω)) atTop
    (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
rw [this]
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this_1 : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun (i : ℕ) ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
C :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω))
      atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
h₁ : ∀ (n : ℕ), X n ω = Y n ω
h₂ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
this : Eq.{u_2 + 1} (α := E) (∫ (x : Ω), X 0 x ∂μ) (∫ (x : Ω), Y 0 x ∂μ)
apply :
  ∀ (n : ℕ),
    HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω) =
      HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω)
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))

Tactic:
apply Tendsto.congr (fun n ↦ ?_) h₂

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this_1 : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun (i : ℕ) ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
C :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω))
      atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
h₁ : ∀ (n : ℕ), X n ω = Y n ω
h₂ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
this : Eq.{u_2 + 1} (α := E) (∫ (x : Ω), X 0 x ∂μ) (∫ (x : Ω), Y 0 x ∂μ)
n : ℕ
e_a : ∀ (i : ℕ), Y i ω = X i ω
⊢ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω) =
    HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω)

Tactic:
congr with i
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this_1 : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun (i : ℕ) ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
C :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω))
      atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
h₁ : ∀ (n : ℕ), X n ω = Y n ω
h₂ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
this : Eq.{u_2 + 1} (α := E) (∫ (x : Ω), X 0 x ∂μ) (∫ (x : Ω), Y 0 x ∂μ)
n i : ℕ
⊢ Y i ω = X i ω

Tactic:
(h₁ i).symm

Premises used: Eq.symm
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this_1 : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun (i : ℕ) ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
C :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω))
      atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
h₁ : ∀ (n : ℕ), X n ω = Y n ω
h₂ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω)) atTop
    (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
this : Eq.{u_2 + 1} (α := E) (∫ (x : Ω), X 0 x ∂μ) (∫ (x : Ω), Y 0 x ∂μ)
n i : ℕ
⊢ Y i ω = X i ω

Tactic:
exact (h₁ i).symm

Premises used: Eq.symm
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
pos :
  ∀ (h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0),
    Tendsto (β := ℝ≥0∞)
      (fun (n : ℕ) ↦
        eLpNorm.{u_1, u_2} (ε := E)
          (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) - ∫ (x : Ω), X 0 x ∂μ) p μ)
      atTop (𝓝 0)
neg :
  ∀ (h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0),
    Tendsto (β := ℝ≥0∞)
      (fun (n : ℕ) ↦
        eLpNorm.{u_1, u_2} (ε := E)
          (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) - ∫ (x : Ω), X 0 x ∂μ) p μ)
      atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm.{u_1, u_2} (ε := E)
        (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) - ∫ (x : Ω), X 0 x ∂μ) p μ)
    atTop (𝓝 0)

Tactic:
by_cases h : ∀ᵐ ω ∂μ, X 0 ω = 0
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
rw : ∀ (i : ℕ), ∀ᵐ (a : Ω) ∂μ, X i a = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0

Tactic:
rw [ae_all_iff]

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
i : ℕ
⊢ ∀ᵐ (a : Ω) ∂μ, X i a = 0

Tactic:
(hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h

Premises used: ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.IdentDistrib.ae_snd, measurableSet_eq
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
i : ℕ
⊢ ∀ᵐ (a : Ω) ∂μ, X i a = 0

Tactic:
exact (hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h

Premises used: ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.IdentDistrib.ae_snd, measurableSet_eq
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0

Tactic:
have I : ∀ᵐ ω ∂μ, ∀ i, X i ω = 0 := by
      rw [ae_all_iff]
      intro i
      exact (hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
simp :
  eLpNorm.{u_1, u_2} (ε := E) (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) p μ = 0
⊢ eLpNorm.{u_1, u_2} (ε := E)
      (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) - ∫ (x : Ω), X 0 x ∂μ) p μ =
    0

Tactic:
simp only [integral_eq_zero_of_ae h, sub_zero]

Premises used: sub_zero, MeasureTheory.integral_eq_zero_of_ae
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
hf :
  EventuallyEq.{u_1, u_2} (β := E) (ae μ)
    (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) 0
⊢ eLpNorm.{u_1, u_2} (ε := E) (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) p μ = 0

Tactic:
apply eLpNorm_eq_zero_of_ae_zero

Premises used: MeasureTheory.eLpNorm_eq_zero_of_ae_zero
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
h₁ : ∀ (ω : Ω) (hω : ∀ (i : ℕ), X i ω = 0), HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) = 0 ω
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ)
    (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) 0

Tactic:
filter_upwards [I] with ω hω
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
ω : Ω
hω : ∀ (i : ℕ), X i ω = 0
⊢ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) = 0 ω

Tactic:
simp [hω]
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
⊢ ∀ (n : ℕ),
    eLpNorm.{u_1, u_2} (ε := E)
        (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) - ∫ (x : Ω), X 0 x ∂μ) p μ =
      0

Tactic:
have A (n : ℕ) : eLpNorm (fun ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω) - μ[X 0]) p μ = 0 := by
      simp only [integral_eq_zero_of_ae h, sub_zero]
      apply eLpNorm_eq_zero_of_ae_zero
      filter_upwards [I] with ω hω
      simp [hω]
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
A :
  ∀ (n : ℕ),
    eLpNorm.{u_1, u_2} (ε := E)
        (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) - ∫ (x : Ω), X 0 x ∂μ) p μ =
      0
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm.{u_1, u_2} (ε := E)
        (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) - ∫ (x : Ω), X 0 x ∂μ) p μ)
    atTop (𝓝 0)

Tactic:
simp [A]
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ IsProbabilityMeasure μ

Tactic:
have : IsProbabilityMeasure μ := MemLp.isProbabilityMeasure_of_indepFun
    (X 0) (X 1) (zero_lt_one.trans_le hp).ne' hp' hℒp h (hindep zero_ne_one)
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
⊢ ∀ (i : ℕ), AEStronglyMeasurable (X i) μ

Tactic:
have hmeas : ∀ i, AEStronglyMeasurable (X i) μ := fun i =>
    (hident i).aestronglyMeasurable_iff.2 hℒp.1
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
⊢ Integrable (X 0) μ

Tactic:
have hint : Integrable (X 0) μ := hℒp.integrable hp
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
⊢ ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_2} (β := E)
      (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) μ

Tactic:
have havg (n : ℕ) :
      AEStronglyMeasurable (fun ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω)) μ :=
    AEStronglyMeasurable.const_smul (aestronglyMeasurable_fun_sum _ fun i _ => hmeas i) _
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_2} (β := E)
      (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) μ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm.{u_1, u_2} (ε := E)
        (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) - ∫ (x : Ω), X 0 x ∂μ) p μ)
    atTop (𝓝 0)

Tactic:
tendsto_Lp_finite_of_tendstoInMeasure hp hp' havg (memLp_const _) ?_
    (tendstoInMeasure_of_tendsto_ae havg (strong_law_ae _ hint hindep hident))

Premises used: ProbabilityTheory.strong_law_ae, MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure, MeasureTheory.tendstoInMeasure_of_tendsto_ae, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_2} (β := E)
      (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) μ
neg :
  UnifIntegrable.{u_1, u_2, 0} (β := E)
    (fun (n : ℕ) (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) p μ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm.{u_1, u_2} (ε := E)
        (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) - ∫ (x : Ω), X 0 x ∂μ) p μ)
    atTop (𝓝 0)

Tactic:
refine tendsto_Lp_finite_of_tendstoInMeasure hp hp' havg (memLp_const _) ?_
    (tendstoInMeasure_of_tendsto_ae havg (strong_law_ae _ hint hindep hident))

Premises used: ProbabilityTheory.strong_law_ae, MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure, MeasureTheory.tendstoInMeasure_of_tendsto_ae, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_2} (β := E)
      (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) μ
neg :
  UnifIntegrable.{u_1, u_2, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i)) p μ
rw :
  Eq (α := (n : ℕ) → (ω : Ω) → E)
    (fun (n : ℕ) (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i)
⊢ UnifIntegrable.{u_1, u_2, 0} (β := E)
    (fun (n : ℕ) (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) p μ

Tactic:
rw [(_ : (fun (n : ℕ) ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω))
            = fun (n : ℕ) => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i))]
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_2} (β := E)
      (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) μ
neg :
  UniformIntegrable.{u_1, u_2, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i)) p μ
⊢ UnifIntegrable.{u_1, u_2, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i)) p μ

Tactic:
apply UniformIntegrable.unifIntegrable

Premises used: MeasureTheory.UniformIntegrable.unifIntegrable