Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case hint
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := ⋯
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := ⋯
Y : ℕ → ℕ → Ω → E := ⋯
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
k : ℕ
G : ℕ → E → ℝ := ⋯
G_meas : ∀ (k : ℕ), Measurable (G k)
I : ∀ (k i : ℕ), (fun ω ↦ ‖(X i - Y k i) ω‖) = G k ∘ X i
⊢ Integrable (fun ω ↦ ‖(X 0 - Y k 0) ω‖) μ

pp: case hindep
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := ⋯
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := ⋯
Y : ℕ → ℕ → Ω → E := ⋯
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
k : ℕ
G : ℕ → E → ℝ := ⋯
G_meas : ∀ (k : ℕ), Measurable (G k)
I : ∀ (k i : ℕ), (fun ω ↦ ‖(X i - Y k i) ω‖) = G k ∘ X i
⊢ Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on fun i ω ↦ ‖(X i - Y k i) ω‖)

pp: case hident
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := ⋯
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := ⋯
Y : ℕ → ℕ → Ω → E := ⋯
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
k : ℕ
G : ℕ → E → ℝ := ⋯
G_meas : ∀ (k : ℕ), Measurable (G k)
I : ∀ (k i : ℕ), (fun ω ↦ ‖(X i - Y k i) ω‖) = G k ∘ X i
⊢ ∀ (i : ℕ), IdentDistrib (fun ω ↦ ‖(X i - Y k i) ω‖) (fun ω ↦ ‖(X 0 - Y k 0) ω‖) μ μ

Tactic:
· exact (hint.sub ((φ k).comp (X 0) h'.measurable).integrable_of_isFiniteMeasure).norm

Goal state after:
case hindep
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := ⋯
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := ⋯
Y : ℕ → ℕ → Ω → E := ⋯
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
k : ℕ
G : ℕ → E → ℝ := ⋯
G_meas : ∀ (k : ℕ), Measurable (G k)
I : ∀ (k i : ℕ), (fun ω ↦ ‖(X i - Y k i) ω‖) = G k ∘ X i
⊢ Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on fun i ω ↦ ‖(X i - Y k i) ω‖)

case hident
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := ⋯
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := ⋯
Y : ℕ → ℕ → Ω → E := ⋯
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
k : ℕ
G : ℕ → E → ℝ := ⋯
G_meas : ∀ (k : ℕ), Measurable (G k)
I : ∀ (k i : ℕ), (fun ω ↦ ‖(X i - Y k i) ω‖) = G k ∘ X i
⊢ ∀ (i : ℕ), IdentDistrib (fun ω ↦ ‖(X i - Y k i) ω‖) (fun ω ↦ ‖(X 0 - Y k 0) ω‖) μ μ