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
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 ω)|
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))
⊢ ∀ᶠ (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_lt : (↑L : ℝ) * ε / 2 < (↑L : ℝ) * ε
Tactic: have h_lt : L * ε / 2 < L * ε := half_lt_self (by positivity)
-- 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 ω)|
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))
h_lt : (↑L : ℝ) * ε / 2 < (↑L : ℝ) * ε
⊢ ∀ᶠ (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 : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x : ι |
      Membership.mem (γ := Set ι)
          {x : ι |
            (fun (a : ι) ↦
                (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y a ω - X a ω‖} +
                    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X a) μ'') fun (ω : E) ↦ F ω)
                        (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| <
                  (↑L : ℝ) * ε)
              x}
          x →
        Membership.mem (γ := Set ι)
          {x : ι |
            (fun (n : ι) ↦
                |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
                      (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| <
                  (↑L : ℝ) * ε)
              x}
          x}
    a
Tactic: filter_upwards [h_tendsto.eventually_lt_const h_lt] with n hn using (h_le n).trans_lt hn
-- 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
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
⊢ TendstoInDistribution (E := E × E') (Ω := fun (n : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
    (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'
have hX : ∀ (i : ι), AEMeasurable (X i) μ''
Tactic: have hX : ∀ i, AEMeasurable (X i) μ'' := hXZ.forall_aemeasurable
-- 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
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
⊢ TendstoInDistribution (E := E × E') (Ω := fun (n : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
    (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'
have refine_1 : TendstoInDistribution (E := E × E') (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
  (fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'
Tactic: refine tendstoInDistribution_of_tendstoInMeasure_sub (X := fun n ω ↦ (X n ω, c))
    (fun n ω ↦ (X n ω, Y n ω)) (fun ω ↦ (Z ω, c)) ?_ ?_ (fun i ↦ (hX i).prodMk (hY_meas i))
-- 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
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
refine_1 :
  TendstoInDistribution (E := E × E') (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
    (fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'
⊢ TendstoInDistribution (E := E × E') (Ω := fun (n : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
    (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'
have refine_2 : TendstoInMeasure μ''
  (HSub.hSub (α := ι → Ω'' → E × E') (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) l 0
Tactic: refine tendstoInDistribution_of_tendstoInMeasure_sub (X := fun n ω ↦ (X n ω, c))
    (fun n ω ↦ (X n ω, Y n ω)) (fun ω ↦ (Z ω, c)) ?_ ?_ (fun i ↦ (hX i).prodMk (hY_meas i))
-- 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
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
this : TendstoInMeasure (E := E × E') μ'' (fun (n : ι) (ω : Ω'') ↦ (0, Y n ω - c)) l 0
⊢ TendstoInMeasure μ''
    (HSub.hSub (α := ι → Ω'' → E × E') (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) l 0
have h : ∀ (n : ι) (ω : Ω''),
  (HSub.hSub (α := ι → Ω'' → E × E') (β := ι → Ω'' → E × E') (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω))
        (fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) n ω).1 =
    0
Tactic: convert! this with n ω
-- 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
E' : Type u_6
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
⊢ TendstoInMeasure μ''
    (HSub.hSub (α := ι → Ω'' → E × E') (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) fun (n : ι) (ω : Ω'') ↦ (X n ω, c)) l 0
have refine_2 : TendstoInMeasure (E := E × E') μ'' (fun (n : ι) (ω : Ω'') ↦ (0, Y n ω - c)) l 0
Tactic: suffices TendstoInMeasure μ'' (fun n ω ↦ ((0 : E), Y n ω - c)) l 0 by
      convert! this with n ω
      simp
-- 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
Z : Ω' → E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
E' : Type u_6
F : Type u_7
mE' : MeasurableSpace E'
inst_5 : SeminormedAddCommGroup E'
inst_6 : SecondCountableTopology E'
inst_7 : BorelSpace E'
inst_8 : TopologicalSpace F
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
g : E × E' → F
hg : Continuous[instTopologicalSpaceProd, inst_8] g
inst_11 : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
c : E'
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hY_tendsto : TendstoInMeasure μ'' Y l fun (x : Ω'') ↦ c
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
⊢ TendstoInDistribution.{u_1, u_7, u_3, u_4} (E := F) (Ω := fun (n : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := inst_9)
    (fun (n : ι) (ω : Ω'') ↦ g (X n ω, Y n ω)) l (fun (ω : Ω') ↦ g (Z ω, c)) (fun (x : ι) ↦ μ'') μ'
have refine : TendstoInDistribution (E := E × E') (Ω := fun (n : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := Prod.instMeasurableSpace)
  (fun (n : ι) (ω : Ω'') ↦ (X n ω, Y n ω)) l (fun (ω : Ω') ↦ (Z ω, c)) (fun (x : ι) ↦ μ'') μ'
Tactic: refine TendstoInDistribution.continuous_comp hg ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
have pos : ∀ (hε_top : ε = ∞),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
Tactic: by_cases hε_top : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
pos :
  ∀ (hε_top : ε = ∞),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
have neg : ∀ (hε_top : ¬ε = ∞),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
Tactic: by_cases hε_top : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
have h1 : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0)
Tactic: have h1 : Tendsto (fun n ↦ μ {ω | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0) := h 1 (by simp) (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
h1 : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
have pos : LE.le.{u_2} (α := ι → ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) fun (n : ι) ↦
  (μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)}
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h1 (fun _ ↦ zero_le) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
h1 : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0)
n : ι
⊢ LE.le (α := (fun (a : ι) ↦ ℝ≥0∞) n)
    ((fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞)) n)
    ((fun (n : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)} : ℝ≥0∞)) n)
have pos : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ∞ ≤ edist (f n x) (g x)} : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)} : ℝ≥0∞)
Tactic: simp only [hε_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
h1 : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0)
n : ι
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ∞ ≤ edist (f n x) (g x)} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)} : ℝ≥0∞)
have pos : ∀ (a : α), LE.le (α := ℝ≥0∞) 1 ∞
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddCommGroup E
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ≥0∞),
      0 < ε → ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)
have simp_rw : TendstoInMeasure μ f l g ↔
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
Tactic: simp_rw [← edist_eq_enorm_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)
have rw : (∀ (ε : ℝ≥0∞),
    0 < ε → ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)) ↔
  ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)
Tactic: rw [tendstoInMeasure_iff_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
⊢ (∀ (ε : ℝ≥0∞),
      0 < ε →
        ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)) ↔
    ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)
have a : ∀ (ε : ℝ≥0∞) (hε : 0 < ε) (hε_top : ε ≠ ∞),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0) ↔
    Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)
Tactic: congr! with ε hε hε_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ),
      0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
have refine_1 : ∀ (h : TendstoInMeasure μ f l g) (ε : ℝ) (hε : 0 < ε),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
Tactic: refine ⟨fun h ε hε ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
refine_1 :
  ∀ (h : TendstoInMeasure μ f l g) (ε : ℝ) (hε : 0 < ε),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ),
      0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
have refine_2 : ∀
  (h :
    ∀ (ε : ℝ),
      0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)),
  TendstoInMeasure μ f l g
Tactic: refine ⟨fun h ε hε ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
have h₁ : ∀ (i : ι) (a : α), ε ≤ dist (f i a) (g a) ↔ ENNReal.ofReal ε ≤ edist (f i a) (g a)
Tactic: convert! h (ENNReal.ofReal ε) (ENNReal.ofReal_pos.mpr hε) with i a
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
a : α
⊢ ε ≤ dist (f i a) (g a) ↔ ENNReal.ofReal ε ≤ edist (f i a) (g a)
have h₁ : ε ≤ dist (f i a) (g a) ↔ ENNReal.ofReal ε ≤ ENNReal.ofReal (dist (f i a) (g a))
Tactic: rw [edist_dist, ENNReal.ofReal_le_ofReal_iff (by positivity)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
a : α
h₁ : ε ≤ dist (f i a) (g a) ↔ ENNReal.ofReal ε ≤ ENNReal.ofReal (dist (f i a) (g a))
⊢ ε ≤ dist (f i a) (g a) ↔ ENNReal.ofReal ε ≤ edist (f i a) (g a)
have h₂ : ε ≤ dist (f i a) (g a) ↔ ε ≤ dist (f i a) (g a)
Tactic: rw [edist_dist, ENNReal.ofReal_le_ofReal_iff (by positivity)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ),
    0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g
have refine_2 : ∀ (ε : ℝ≥0∞) (hε : 0 < ε) (hε_top : ε ≠ ∞),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
Tactic: refine tendstoInMeasure_of_ne_top fun ε hε hε_top ↦ ?_