awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (hypothesis)
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)) μ''
⊢ |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 ω‖}
have h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
Tactic: have h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ'' := by
      rw [integrable_norm_iff (by fun_prop)]
      exact h_int_Y.sub h_int_X
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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)‖) μ''
⊢ |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 ω‖}
have bc : norm (E := ℝ) (∫ (a : Ω''), F (Y n a) - F (X n a) ∂μ'') ≤
  (↑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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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)‖) μ''
⊢ ∫ (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)‖ ∂μ'')
have 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)‖ ∂μ''
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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 : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, ‖F (Y n a) - F (X n a)‖ ∂μ'') =
    ∫ (a : Ω''), ‖F (Y n a) - F (X n a)‖ ∂μ''
have 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)‖ ∂μ''
Tactic: simp_rw [← not_lt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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)‖ ∂μ''
have refine : NullMeasurableSet {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} μ''
Tactic: refine integral_add_compl₀ ?_ h_int_sub
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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 : Ω'') ↦ ‖Y n x - X n x‖) μ''
have funProp : mE ≤ mE
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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
⊢ AEMeasurable (β := ℝ) (fun (x : Ω'') ↦ ‖Y n x - X n x‖) μ''
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (x2 : E) ↦ ‖x2‖
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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 : Ω'' | ε / 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 ∂μ'')
have 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) ∂μ'')
Tactic: gcongr ?_ + ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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) ∂μ'')
⊢ 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 ∂μ'')
have 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 ∂μ'')
Tactic: gcongr ?_ + ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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) ∂μ'')
have h₁ : NullMeasurableSet {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} μ''
Tactic: refine setIntegral_mono_on₀ h_int_sub.integrableOn integrableOn_const ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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} μ''
⊢ 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) ∂μ'')
have h₂ : ∀ (x : Ω''),
  Membership.mem (γ := Set Ω'') {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} x → ‖F (Y n x) - F (X n x)‖ ≤ (↑L : ℝ) * (ε / 2)
Tactic: refine setIntegral_mono_on₀ h_int_sub.integrableOn integrableOn_const ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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 : Ω'' | ε / 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 ∂μ'')
have h₂ : ∀ (a : Ω''), ‖F (Y n a) - F (X n a)‖ ≤ M
Tactic: refine setIntegral_mono h_int_sub.integrableOn integrableOn_const fun a ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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}, (↑L : ℝ) * (ε / 2) ∂μ'')
      (∫ (a : Ω'') in {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, M ∂μ'') =
    (↑L : ℝ) * (ε / 2) * μ''.real {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖}
have simp : μ''.real {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} * ((↑L : ℝ) * (ε / 2)) + μ''.real {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖} * M =
  (↑L : ℝ) * (ε / 2) * μ''.real {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} + M * μ''.real {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}
Tactic: simp only [integral_const, MeasurableSet.univ, measureReal_restrict_apply, Set.univ_inter,
        smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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)‖) μ''
⊢ (↑L : ℝ) * (ε / 2) * μ''.real {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} ≤
    (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖}
have rw : (↑L : ℝ) * (ε / 2 * μ''.real {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} ≤
  (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖}
Tactic: rw [mul_assoc]