mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : 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
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
h : ∫⁻ (a : α) in u, ((κ.map fun ω ↦ (f ω, g ω)) a) (s ×ˢ t) ∂μ = ∫⁻ (a : α) in u, ((κ.map f ×ₖ κ.map g) a) (s ×ˢ t) ∂μ
hu : MeasurableSet u
hμu : μ u < ⊤
ω : α
⊢ Measurable fun ω ↦ (f ω, g ω)

Tactic:
fun_prop

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

Goal state before:
pp: α : 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
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
h : ∫⁻ (a : α) in u, ((κ.map fun ω ↦ (f ω, g ω)) a) (s ×ˢ t) ∂μ = ∫⁻ (a : α) in u, ((κ.map f ×ₖ κ.map g) a) (s ×ˢ t) ∂μ
hu : MeasurableSet u
hμu : μ u < ⊤
ω : α
⊢ Measurable f

Tactic:
fun_prop

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

Goal state before:
pp: α : 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
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
h : ∫⁻ (a : α) in u, ((κ.map fun ω ↦ (f ω, g ω)) a) (s ×ˢ t) ∂μ = ∫⁻ (a : α) in u, ((κ.map f ×ₖ κ.map g) a) (s ×ˢ t) ∂μ
hu : MeasurableSet u
hμu : μ u < ⊤
ω : α
⊢ Measurable g

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_7
mΩ : MeasurableSpace Ω
μ : Measure Ω
M : Type u_10
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
f g : Ω → M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
hfg : f ⟂ᵢ[μ] g
⊢ Measure.map (fun p ↦ p.1 * p.2) ((Measure.map f μ).prod (Measure.map g μ)) = Measure.map f μ ∗ₘ Measure.map g μ

Tactic:
Measure.mconv

Goal state after:
Ω : Type u_7
mΩ : MeasurableSpace Ω
μ : Measure Ω
M : Type u_10
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
f g : Ω → M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
hfg : f ⟂ᵢ[μ] g
⊢ Measure.map (fun p ↦ p.1 * p.2) ((Measure.map f μ).prod (Measure.map g μ)) =
    Measure.map (fun x ↦ x.1 * x.2) ((Measure.map f μ).prod (Measure.map g μ))
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this✝ : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ AEMeasurable (X * Y) ℙ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this✝ : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ AEMeasurable X ℙ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this✝ : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ AEMeasurable Y ℙ

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ AEStronglyMeasurable (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) μ

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
⊢ eVar[X; μ] = 0 ↔ X =ᵐ[μ] fun x ↦ ∫ (x : Ω), X x ∂μ

Tactic:
by
  simp [evariance, lintegral_eq_zero_iff' ((hX.sub_const _).enorm.pow_const _), EventuallyEq,
    sub_eq_zero]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
ω : Ω
⊢ Integrable (fun x ↦ c) μ

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : MemLp X 2 μ
hX_int : Integrable X μ
⊢ Integrable (fun x ↦ c) μ

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
⊢ AEStronglyMeasurable (fun ω ↦ -X ω) μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ContinuousENorm E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousENorm F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E → F → G
cB : Continuous (Function.uncurry B)
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖B x y‖ₑ ≤ ↑C * ‖x‖ₑ * ‖y‖ₑ
⊢ AEMeasurable (fun ω ↦ ‖X ω‖ₑ * ‖Y ω‖ₑ) μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E →L[𝕜] F →L[𝕜] G
⊢ Continuous (Function.uncurry fun x1 x2 ↦ (B x1) x2)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousENorm E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : OpensMeasurableSpace E
inst✝⁴ : NormedAddGroup F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable (fun ω ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun x ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun x ↦ ‖Y x‖ₑ
⊢ AEMeasurable (fun ω ↦ ‖X ω‖ₑ * ‖Y ω‖ₑ) μ

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
h : Integrable (fun a ↦ (X a - ∫ (x : Ω), X x ∂μ) ^ 2) μ
⊢ AEStronglyMeasurable (X - fun ω ↦ ∫ (x : Ω), X x ∂μ) μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : Integrable f (Measure.map X μ)
hg : Integrable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
this : IsProbabilityMeasure μ
⊢ AEMeasurable (fun ω ↦ (X ω, Y ω)) μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : Integrable f (Measure.map X μ)
hg : Integrable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
this : IsProbabilityMeasure μ
⊢ Continuous (Function.uncurry fun x1 x2 ↦ (B x1) x2)

Tactic:
fun_prop

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

Goal state before:
pp: ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ Measurable fun ω ↦ ω i

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ
hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ
⊢ Integrable (fun ω ↦ -X ω ^ 2 + (a + b) * X ω) μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst✝ : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : X ⟂ᵢ[P] Y
⊢ AEMeasurable X P

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst✝ : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : X ⟂ᵢ[P] Y
⊢ AEMeasurable Y P

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst✝ : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : HasLaw (fun ω ↦ (X ω, Y ω)) (μ.prod ν) P
⊢ AEMeasurable X P

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst✝ : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : HasLaw (fun ω ↦ (X ω, Y ω)) (μ.prod ν) P
⊢ AEMeasurable Y P

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : iIndepFun X P
⊢ ∀ (i : ι), AEMeasurable (X i) P

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝¹ : IsProbabilityMeasure P
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : HasLaw (fun ω i ↦ X i ω) (Measure.pi μ) P
⊢ ∀ (i : ι), AEMeasurable (X i) P

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : ContinuousENorm E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : OpensMeasurableSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : ContinuousENorm F
inst✝⁴ : MeasurableSpace F
inst✝³ : OpensMeasurableSpace F
inst✝² : SMul E F
inst✝¹ : ContinuousSMul E F
inst✝ : ENormSMulClass E F
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
⊢ Continuous (Function.uncurry fun x1 x2 ↦ x1 • x2)

Tactic:
fun_prop

Goal state after:
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✝ : OpensMeasurableSpace E
hZ : AEMeasurable Z μ'
x✝ : ι
⊢ AEMeasurable Z μ'

Tactic:
fun_prop

Goal state after:
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
⊢ AEMeasurable (fun ω ↦ ↑(f ω)) (Measure.map Z μ')

Tactic:
fun_prop

Goal state after:
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
i : ι
⊢ AEMeasurable (fun ω ↦ ↑(f ω)) (Measure.map (X i) μ')

Tactic:
fun_prop

Goal state after:
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
⊢ ∀ (x : ι), AEMeasurable (fun a ↦ ↑(f (X x a))) μ'

Tactic:
fun_prop

Goal state after:
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✝³ : PseudoEMetricSpace E
inst✝² : BorelSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
X : ι → Ω' → E
h : TendstoInMeasure μ' X l Z
hX : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
ns : ℕ → ι
hns : Tendsto ns atTop l
ms : ℕ → ℕ
hms1 : Tendsto ms atTop atTop
hms2 : ∀ᵐ (x : Ω') ∂μ', Tendsto (fun i ↦ (X ∘ ns) (ms i) x) atTop (𝓝 (Z x))
⊢ ∀ (i : ℕ), AEMeasurable (X (ns (ms i))) μ'

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case hφ
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ AEMeasurable (fun ω x ↦ X x ω) μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
this :
  ∀ (F : E → ℝ),
    (∃ C, ∀ (x y : E), dist (F x) (F y) ≤ C) →
      (∃ L, LipschitzWith L F) →
        Tendsto (fun n ↦ ∫ (ω : E), F ω ∂Measure.map (Y n) μ'') l (𝓝 (∫ (ω : E), F ω ∂Measure.map Z μ'))
⊢ Tendsto (fun n ↦ ⟨Measure.map (Y n) μ'', ⋯⟩) l (𝓝 ⟨Measure.map Z μ', ⋯⟩)

Tactic:
tendsto_iff_forall_lipschitz_integral_tendsto

Goal state after:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
this :
  ∀ (F : E → ℝ),
    (∃ C, ∀ (x y : E), dist (F x) (F y) ≤ C) →
      (∃ L, LipschitzWith L F) →
        Tendsto (fun n ↦ ∫ (ω : E), F ω ∂Measure.map (Y n) μ'') l (𝓝 (∫ (ω : E), F ω ∂Measure.map Z μ'))
⊢ ∀ (f : E → ℝ),
    (∃ C, ∀ (x y : E), dist (f x) (f y) ≤ C) →
      (∃ L, LipschitzWith L f) →
        Tendsto (fun i ↦ ∫ (ω : E), f ω ∂↑⟨Measure.map (Y i) μ'', ⋯⟩) l (𝓝 (∫ (ω : E), f ω ∂↑⟨Measure.map Z μ', ⋯⟩))
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case hfm
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ AEStronglyMeasurable (fun x ↦ ∏ i, f i (x i)) (Measure.pi fun i ↦ Measure.map (X i) μ)

Tactic:
exact Finset.aestronglyMeasurable_fun_prod Finset.univ fun i _ ↦
    (hf i).comp_quasiMeasurePreserving (Measure.quasiMeasurePreserving_eval _ i)

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_5
𝓧 : Type u_6
m mΩ : MeasurableSpace Ω
P : Measure Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
A : Set Ω
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ mΩ
f : 𝓧 → E
hA1 : Indep m (MeasurableSpace.comap X m𝓧) P
hX : AEMeasurable X P
hA2 : MeasurableSet A
hf : AEStronglyMeasurable f (Measure.map X P)
⊢ AEStronglyMeasurable id (Measure.map (A.indicator 1) P)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : X ⟂ᵢ[μ] Y
h_ident : IdentDistrib (fun ω ↦ (X ω, Y ω)) (fun ω ↦ (X' ω, Y' ω)) μ μ'
⊢ (Measure.map X μ).prod (Measure.map Y μ) = (Measure.map X' μ').prod (Measure.map Y' μ')

Tactic:
exact congr (congrArg Measure.prod <| (h_ident.comp measurable_fst).map_eq)
      (h_ident.comp measurable_snd).map_eq

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
⊢ AEStronglyMeasurable (fun x ↦ F (Y n x)) μ''

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
⊢ AEStronglyMeasurable (fun x ↦ F (X n x)) μ''

Tactic:
fun_prop

Goal state after: