awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ AEStronglyMeasurable (m₀ := mE) F (Measure.map (Y n) μ'')

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ AEMeasurable (X n) μ''

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ AEStronglyMeasurable (m₀ := mE) F (Measure.map (X n) μ'')

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
bc :
  norm (E := ℝ) (∫ (a : Ω''), F (Y n a) - F (X n a) ∂μ'') ≤
    (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖}
⊢ |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
        (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)| ≤
    (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖}

Tactic:
rw [integral_map (by fun_prop) (by fun_prop), integral_map (by fun_prop) (by fun_prop),
      ← integral_sub h_int_Y h_int_X, ← Real.norm_eq_abs]

Premises used: MeasureTheory.integral_map, MeasureTheory.integral_sub, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ norm (E := ℝ) (∫ (a : Ω''), F (Y n a) - F (X n a) ∂μ'') ≤ ∫ (a : Ω''), ‖F (Y n a) - F (X n a)‖ ∂μ''

Tactic:
norm_integral_le_integral_norm _

Premises used: MeasureTheory.norm_integral_le_integral_norm
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
symm :
  HAdd.hAdd (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
      (∫ (a : Ω'') in {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, ‖F (Y n a) - F (X n a)‖ ∂μ'') =
    ∫ (a : Ω''), ‖F (Y n a) - F (X n a)‖ ∂μ''
⊢ ∫ (a : Ω''), ‖F (Y n a) - F (X n a)‖ ∂μ'' =
    HAdd.hAdd (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
      (∫ (a : Ω'') in {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, ‖F (Y n a) - F (X n a)‖ ∂μ'')

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
simp_rw :
  HAdd.hAdd (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
      (∫ (a : Ω'') in {x : Ω'' | ¬‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'') =
    ∫ (a : Ω''), ‖F (Y n a) - F (X n a)‖ ∂μ''
⊢ HAdd.hAdd (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
      (∫ (a : Ω'') in {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, ‖F (Y n a) - F (X n a)‖ ∂μ'') =
    ∫ (a : Ω''), ‖F (Y n a) - F (X n a)‖ ∂μ''

Tactic:
simp_rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ HAdd.hAdd (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
      (∫ (a : Ω'') in {x : Ω'' | ¬‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'') =
    ∫ (a : Ω''), ‖F (Y n a) - F (X n a)‖ ∂μ''

Tactic:
integral_add_compl₀ ?_ h_int_sub

Premises used: Set.Mem, setOf, MeasureTheory.integral_add_compl₀
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
refine : NullMeasurableSet {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} μ''
⊢ HAdd.hAdd (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
      (∫ (a : Ω'') in {x : Ω'' | ¬‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'') =
    ∫ (a : Ω''), ‖F (Y n a) - F (X n a)‖ ∂μ''

Tactic:
refine integral_add_compl₀ ?_ h_int_sub

Premises used: MeasureTheory.integral_add_compl₀
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
funProp : mE ≤ mE
funProp₁ : MeasurableEmbedding (β := ℝ) fun (x2 : E) ↦ ‖x2‖
⊢ AEMeasurable (β := ℝ) (fun (x : Ω'') ↦ ‖Y n x - X n x‖) μ''

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ AEMeasurable (β := ℝ) (fun (x : Ω'') ↦ ε / 2) μ''

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ NullMeasurableSet {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} μ''

Tactic:
exact nullMeasurableSet_lt (by fun_prop) (by fun_prop)

Premises used: nullMeasurableSet_lt
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
h₁ :
  LE.le (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
    (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, (↑L : ℝ) * (ε / 2) ∂μ'')
h₂ :
  LE.le (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
    (∫ (a : Ω'') in {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, M ∂μ'')
⊢ HAdd.hAdd (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
      (∫ (a : Ω'') in {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, ‖F (Y n a) - F (X n a)‖ ∂μ'') ≤
    HAdd.hAdd (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, (↑L : ℝ) * (ε / 2) ∂μ'')
      (∫ (a : Ω'') in {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, M ∂μ'')

Tactic:
gcongr ?_ + ?_
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ LE.le (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
    (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, (↑L : ℝ) * (ε / 2) ∂μ'')

Tactic:
setIntegral_mono_on₀ h_int_sub.integrableOn integrableOn_const ?_ ?_

Premises used: MeasureTheory.setIntegral_mono_on₀, MeasureTheory.integrableOn_const, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
h₁ : NullMeasurableSet {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} μ''
h₂ :
  ∀ (x : Ω''),
    Membership.mem (γ := Set Ω'') {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} x → ‖F (Y n x) - F (X n x)‖ ≤ (↑L : ℝ) * (ε / 2)
⊢ LE.le (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
    (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, (↑L : ℝ) * (ε / 2) ∂μ'')

Tactic:
refine setIntegral_mono_on₀ h_int_sub.integrableOn integrableOn_const ?_ ?_

Premises used: MeasureTheory.setIntegral_mono_on₀, MeasureTheory.integrableOn_const, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) 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)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ ∀ (x : Ω''),
    Membership.mem (γ := Set Ω'') {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} x → ‖F (Y n x) - F (X n x)‖ ≤ (↑L : ℝ) * (ε / 2)

Tactic:
fun x hx ↦ hF_lip.norm_sub_le_of_le hx.le

Premises used: LipschitzWith.norm_sub_le_of_le, LT.lt.le