awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 bc : ε / 2 * μ''.real {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} ≤ ε / 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)‖) μ''
⊢ ε / 2 * μ''.real {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} ≤ ε / 2
have h₁ : 0 ≤ ε / 2
Tactic: grw [measureReal_le_one, mul_one]
-- 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₁ : 0 ≤ ε / 2
⊢ ε / 2 * μ''.real {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} ≤ ε / 2
have bc : ε / 2 * 1 ≤ ε / 2
Tactic: grw [measureReal_le_one, mul_one]
-- 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₁ : 0 ≤ ε / 2
bc : ε / 2 * 1 ≤ ε / 2
⊢ ε / 2 * μ''.real {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} ≤ ε / 2
have bc₁ : ε / 2 ≤ ε / 2
Tactic: grw [measureReal_le_one, mul_one]
-- 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
h_le :
  ∀ (n : ι),
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| ≤
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|
⊢ Tendsto
    (fun (n : ι) ↦
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|)
    l (𝓝 ((↑L : ℝ) * ε / 2))
have suffices : Tendsto
  (fun (n : ι) ↦
    (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
      |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|)
  l (𝓝 ((↑L : ℝ) * ε / 2 + M * 0 + 0))
Tactic: suffices Tendsto (fun n ↦ L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖}
        + |∫ ω, F ω ∂(μ''.map (X n)) - ∫ ω, F ω ∂(μ'.map Z)|) l (𝓝 (L * ε / 2 + M * 0 + 0)) by
      simpa
-- 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
h_le :
  ∀ (n : ι),
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| ≤
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|
⊢ Tendsto
    (fun (n : ι) ↦
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|)
    l (𝓝 ((↑L : ℝ) * ε / 2 + M * 0 + 0))
have refine_1 : Tendsto (fun (n : ι) ↦ (↑L : ℝ) * (ε / 2)) l (𝓝 ((↑L : ℝ) * ε / 2))
Tactic: refine (Tendsto.add ?_ (Tendsto.const_mul _ ?_)).add ?_
-- 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
h_le :
  ∀ (n : ι),
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| ≤
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|
refine_1 : Tendsto (fun (n : ι) ↦ (↑L : ℝ) * (ε / 2)) l (𝓝 ((↑L : ℝ) * ε / 2))
⊢ Tendsto
    (fun (n : ι) ↦
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|)
    l (𝓝 ((↑L : ℝ) * ε / 2 + M * 0 + 0))
have refine_2 : Tendsto (β := ℝ) (fun (n : ι) ↦ μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖}) l (𝓝 0)
Tactic: refine (Tendsto.add ?_ (Tendsto.const_mul _ ?_)).add ?_
-- 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
h_le :
  ∀ (n : ι),
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| ≤
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|
refine_1 : Tendsto (fun (n : ι) ↦ (↑L : ℝ) * (ε / 2)) l (𝓝 ((↑L : ℝ) * ε / 2))
refine_2 : Tendsto (β := ℝ) (fun (n : ι) ↦ μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖}) l (𝓝 0)
⊢ Tendsto
    (fun (n : ι) ↦
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|)
    l (𝓝 ((↑L : ℝ) * ε / 2 + M * 0 + 0))
have refine_3 : Tendsto (β := ℝ)
  (fun (n : ι) ↦
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
        (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|)
  l (𝓝 0)
Tactic: refine (Tendsto.add ?_ (Tendsto.const_mul _ ?_)).add ?_
-- 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
h_le :
  ∀ (n : ι),
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| ≤
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|
⊢ Tendsto (fun (n : ι) ↦ (↑L : ℝ) * (ε / 2)) l (𝓝 ((↑L : ℝ) * ε / 2))
have refine_1 : Tendsto (fun (n : ι) ↦ (↑L : ℝ) * (ε / 2)) l (𝓝 ((↑L : ℝ) * (ε / 2)))
Tactic: rw [mul_div_assoc]
-- 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
h_le :
  ∀ (n : ι),
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| ≤
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|
⊢ Tendsto (β := ℝ) (fun (n : ι) ↦ μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖}) l (𝓝 0)
have hXY₁ : ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ''.real {x : Ω'' | ε ≤ ‖(Y - X) i x‖}) l (𝓝 0)
Tactic: simp only [tendstoInMeasure_iff_measureReal_norm, Pi.zero_apply, sub_zero] at hXY
Cleared hypotheses: hXY
-- 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
h_le :
  ∀ (n : ι),
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| ≤
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|
⊢ Tendsto (β := ℝ)
    (fun (n : ι) ↦
      |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|)
    l (𝓝 0)
have hXZ₁ : Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) μ'') sorry) l
  (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') sorry))
Tactic: replace hXZ := hXZ.tendsto
-- 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_1 : 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
h_le :
  ∀ (n : ι),
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| ≤
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|
hXZ :
  Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) μ'') ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯))
⊢ Tendsto (β := ℝ)
    (fun (n : ι) ↦
      |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|)
    l (𝓝 0)
have hXZ₁ : ∀ (f : E → ℝ),
  (∃ (C : ℝ), ∀ (x y : E), dist (f x) (f y) ≤ C) →
    (∃ (L : NNReal), LipschitzWith L f) →
      Tendsto (β := ℝ)
        (fun (i : ι) ↦
          ∫ (ω : E),
            f
              ω ∂(↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X i) μ'') sorry) :
              Measure E))
        l
        (𝓝
          (∫ (ω : E),
            f ω ∂(↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') sorry) : Measure E)))
Tactic: simp_rw [tendsto_iff_forall_lipschitz_integral_tendsto] at hXZ
Cleared hypotheses: hXZ
-- 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
h_le :
  ∀ (n : ι),
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| ≤
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|
⊢ ∀ᶠ (n : ι) in l,
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| <
      (↑L : ℝ) * ε
have h_tendsto : Tendsto
  (fun (n : ι) ↦
    (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
      |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|)
  l (𝓝 ((↑L : ℝ) * ε / 2))
Tactic: have h_tendsto :
      Tendsto (fun n ↦ L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖}
        + |∫ ω, F ω ∂(μ''.map (X n)) - ∫ ω, F ω ∂(μ'.map Z)|) l (𝓝 (L * ε / 2)) := by
    suffices Tendsto (fun n ↦ L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖}
        + |∫ ω, F ω ∂(μ''.map (X n)) - ∫ ω, F ω ∂(μ'.map Z)|) l (𝓝 (L * ε / 2 + M * 0 + 0)) by
      simpa
    refine (Tendsto.add ?_ (Tendsto.const_mul _ ?_)).add ?_
    · rw [mul_div_assoc]
      exact tendsto_const_nhds
    · simp only [tendstoInMeasure_iff_measureReal_norm, Pi.zero_apply, sub_zero] at hXY
      exact hXY (ε / 2) (by positivity)
    · replace hXZ := hXZ.tendsto
      simp_rw [tendsto_iff_forall_lipschitz_integral_tendsto] at hXZ
      simpa [tendsto_iff_dist_tendsto_zero] using hXZ F ⟨M, hF_bounded⟩ ⟨L, hF_lip⟩