mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖g i x‖₊}.indicator (g i) x = {x | C ≤ ‖f i x‖₊}.indicator (f i) x

Tactic:
rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]

Goal state after:
case neg.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ x ∉ {x | C ≤ ‖g i x‖₊}
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s t : Set Ω
h : Disjoint s t
ht : MeasurableSet t
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

Tactic:
ext u hu
  simp [Measure.restrict_union h ht]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
f : Ω →ᵇ ℝ≥0
⊢ (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal = (∫⁻ (x : Ω), ↑(f x) ∂↑ν).toReal

Tactic:
toReal_lintegral_coe_eq_integral f μ,

Goal state after:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
f : Ω →ᵇ ℝ≥0
⊢ ∫ (x : Ω), ↑(f x) ∂↑μ = (∫⁻ (x : Ω), ↑(f x) ∂↑ν).toReal
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
⊢ Tendsto (fun i ↦ (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))

Tactic:
tendsto_congr' eve,

Goal state after:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
⊢ Tendsto (fun x ↦ (μs x).mass⁻¹ * (μs x).testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖g i x‖₊}.indicator (g i) x = {x | C ≤ ‖f i x‖₊}.indicator (f i) x

Tactic:
rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]

Goal state after:
case neg.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ x ∉ {x | C ≤ ‖g i x‖₊}
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖f i x‖₊}.indicator (f i) x = {x | C ≤ ‖g i x‖₊}.indicator (g i) x

Tactic:
rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]

Goal state after:
case neg.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ x ∉ {x | C ≤ ‖g i x‖₊}
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_1
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set γ),
    MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
h_set_eq : ∀ (ω : α), Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅
⊢ (fun a ↦ ((κ.map fun ω ↦ (f ω, g ω)) a) (if a ∈ u then s ×ˢ t else ∅)) =ᵐ[μ] fun a ↦
    ((κ.map f ×ₖ κ.map g) a) (if a ∈ u then s ×ˢ t else ∅)

Tactic:
filter_upwards [h s t hs ht] with ω hω

Goal state after:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set γ),
    MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
h_set_eq : ∀ (ω : α), Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅
ω : α
hω : (κ ω) (f ⁻¹' s ∩ g ⁻¹' t) = (κ ω) (f ⁻¹' s) * (κ ω) (g ⁻¹' t)
⊢ ((κ.map fun ω ↦ (f ω, g ω)) ω) (if ω ∈ u then s ×ˢ t else ∅) = ((κ.map f ×ₖ κ.map g) ω) (if ω ∈ u then s ×ˢ t else ∅)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ (μ (⋂ i, Y i ⁻¹' t i))⁻¹ * μ (⋂ i, g i) = (∏ i, μ (Y i ⁻¹' t i))⁻¹ * μ (⋂ i, g i)

Tactic:
rw [hindep.meas_iInter]
      exact fun i ↦ ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp⟩

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u → (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) (s ×ˢ t ×ˢ u) = (μ ⊗ₘ (κ.map f ×ₖ κ.map g)) (s ×ˢ t ×ˢ u)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ Measurable fun a ↦ (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)

pp: case refine_2.refine_3
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u → (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) (s ×ˢ t ×ˢ u) = (μ ⊗ₘ (κ.map f ×ₖ κ.map g)) (s ×ˢ t ×ˢ u)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      μ s_1 < ⊤ →
        ∫⁻ (x : α) in s_1, (κ x) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ = ∫⁻ (x : α) in s_1, (κ x) (f ⁻¹' s) * (κ x) (g ⁻¹' t) ∂μ

Tactic:
· exact (Kernel.measurable_coe _ (hf hs)).mul (Kernel.measurable_coe _ (hg ht))

Goal state after:
case refine_2.refine_3
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u → (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) (s ×ˢ t ×ˢ u) = (μ ⊗ₘ (κ.map f ×ₖ κ.map g)) (s ×ˢ t ×ˢ u)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      μ s_1 < ⊤ →
        ∫⁻ (x : α) in s_1, (κ x) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ = ∫⁻ (x : α) in s_1, (κ x) (f ⁻¹' s) * (κ x) (g ⁻¹' t) ∂μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : Var[X; μ] = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ

Tactic:
rw [variance_eq_integral hX.aemeasurable, integral_eq_zero_iff_of_nonneg] at h

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2) =ᵐ[μ] 0
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ = 0
⊢ 0 ≤ fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2

case hfi
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ = 0
⊢ Integrable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2) μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ cov[X, X; μ] + cov[X, Y; μ] + cov[Y, X + Y; μ] = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ]

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable (X + Y) μ

Tactic:
covariance_add_right hY hX hY,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ cov[X, X; μ] + cov[X, Y; μ] + (cov[Y, X; μ] + cov[Y, Y; μ]) = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ]

Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable (X + Y) μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
⊢ cov[X, Y + Z; μ] = cov[X, Y; μ] + cov[X, Z; μ]

Tactic:
by
  rw [covariance_comm, covariance_add_left hY hZ hX, covariance_comm X, covariance_comm Z]

Goal state after:
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEMeasurable Z μ

Tactic:
assumption

Goal state after:
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEStronglyMeasurable Y (Measure.map Z μ)

Tactic:
assumption

Goal state after:
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEStronglyMeasurable X (Measure.map Z μ)

Tactic:
assumption

Goal state after:
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEStronglyMeasurable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂Measure.map Z μ) * (Y ω - ∫ (x : Ω), Y x ∂Measure.map Z μ))
    (Measure.map Z μ)

Tactic:
assumption

Goal state after:
case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEStronglyMeasurable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂Measure.map Z μ) * (Y ω - ∫ (x : Ω), Y x ∂Measure.map Z μ))
    (Measure.map Z μ)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : Ω), (f ∘ X) x ∂P = ∫ (x : 𝓧), f x ∂map X P

Tactic:
integral_map hX.aemeasurable,

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : Ω), (f ∘ X) x ∂P = ∫ (x : Ω), f (X x) ∂P

Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f (map X P)
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝³ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝² : TopologicalSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : OpensMeasurableSpace E
X : ι → Ω' → E
hX₁ : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
hX₂ : ∀ᵐ (ω : Ω') ∂μ', Tendsto (fun i ↦ X i ω) l (𝓝 (Z ω))
⊢ ∀ (f : BoundedContinuousFunction E NNReal),
    Tendsto (fun i ↦ ∫⁻ (ω : E), ↑(f ω) ∂↑⟨Measure.map (X i) μ', ⋯⟩) l (𝓝 (∫⁻ (ω : E), ↑(f ω) ∂↑⟨Measure.map Z μ', ⋯⟩))

Tactic:
ProbabilityMeasure.coe_mk

Goal state after:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝³ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝² : TopologicalSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : OpensMeasurableSpace E
X : ι → Ω' → E
hX₁ : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
hX₂ : ∀ᵐ (ω : Ω') ∂μ', Tendsto (fun i ↦ X i ω) l (𝓝 (Z ω))
⊢ ∀ (f : BoundedContinuousFunction E NNReal),
    Tendsto (fun i ↦ ∫⁻ (ω : E), ↑(f ω) ∂Measure.map (X i) μ') l (𝓝 (∫⁻ (ω : E), ↑(f ω) ∂Measure.map Z μ'))
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : (𝓝[>] i).NeBot
hj✝ : ¬(𝓝[>] j).NeBot
hj : j ≠ i
⊢ ⨅ j, ⨅ (_ : i < j), ↑𝓕 j ≤ ↑𝓕 j

Tactic:
exact iInf₂_le j (lt_of_le_of_ne hij hj.symm)

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : PartialOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
𝓕 : Filtration ι m
i : ι
hi : 𝓝[>] i = ⊥
⊢ ↑𝓕₊ i = ↑𝓕 i

Tactic:
by
  rw [rightCont_apply, hi, neBot_iff, ne_self_iff_false, if_false]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
α : Type u_4
l : Filter α
f : α → ↥(Lp E p ν)
f₀ : ↥(Lp E p ν)
g : α → C(X, Y)
g₀ : C(X, Y)
hf : Tendsto f l (𝓝 f₀)
hg : Tendsto g l (𝓝 g₀)
hgm : ∀ (a : α), MeasurePreserving (⇑(g a)) μ ν
hgm₀ : MeasurePreserving (⇑g₀) μ ν
hp : p ≠ ∞
⊢ Tendsto (fun a ↦ (Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l (𝓝 ((Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))

Tactic:
have := (Lp.compMeasurePreserving_continuous μ ν E hp).tendsto ⟨f₀, g₀, hgm₀⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
α : Type u_4
l : Filter α
f : α → ↥(Lp E p ν)
f₀ : ↥(Lp E p ν)
g : α → C(X, Y)
g₀ : C(X, Y)
hf : Tendsto f l (𝓝 f₀)
hg : Tendsto g l (𝓝 g₀)
hgm : ∀ (a : α), MeasurePreserving (⇑(g a)) μ ν
hgm₀ : MeasurePreserving (⇑g₀) μ ν
hp : p ≠ ∞
this :
  Tendsto (fun gf ↦ (Lp.compMeasurePreserving ⇑↑gf.2 ⋯) gf.1) (𝓝 (f₀, ⟨g₀, hgm₀⟩))
    (𝓝 ((Lp.compMeasurePreserving ⇑↑(f₀, ⟨g₀, hgm₀⟩).2 ⋯) (f₀, ⟨g₀, hgm₀⟩).1))
⊢ Tendsto (fun a ↦ (Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l (𝓝 ((Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ∞
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ∞
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ∞
hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < ↑ε
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
refine ⟨s ∪ S, (by finiteness), fun i => ?_⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ∞
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ∞
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ∞
hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < ↑ε
i : Fin (n + 1)
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ ↑ε
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : μ Eg < ∞
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : μ Ef < ∞
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : μ E < ∞
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (μ E < ∞)
hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
⊢ AEStronglyMeasurable (Eᶜ.indicator (f n)) μ

Tactic:
assumption

Goal state after: