awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
hp : p ≠ ∞
f_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ IsBounded (range g)
have I3 : eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε
Tactic: have I3 : eLpNorm (f - t.indicator fun _y => c) p μ ≤ ε := by
    convert!
      (hδ _ _
          (f_mem.aestronglyMeasurable.sub
            (aestronglyMeasurable_const.indicator s_closed.measurableSet))
          ((aestronglyMeasurable_const.indicator s_closed.measurableSet).sub
            (aestronglyMeasurable_const.indicator ht))
          I2 I1).le using 2
    simp only [sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
hp : p ≠ ∞
f_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
I3 : eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ IsBounded (range g)
have refine : IsBounded (range f)
Tactic: refine ⟨f, I3, f_cont, f_mem, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
⊢ ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal p) μ
have I : 0 < ε ^ (1 / p)
Tactic: have I : 0 < ε ^ (1 / p) := Real.rpow_pos_of_pos hε _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
⊢ ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal p) μ
have A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
Tactic: have A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0 := by
    simp only [Ne, ENNReal.ofReal_eq_zero, not_le, I]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
⊢ ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal p) μ
have B : ENNReal.ofReal p ≠ 0
Tactic: have B : ENNReal.ofReal p ≠ 0 := by simpa only [Ne, ENNReal.ofReal_eq_zero, not_le] using hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
⊢ ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal p) μ
have rcases : ∀ (g : α →ᵇ E) (hg : eLpNorm (f - (⇑g : (a : α) → E)) (↑p.toNNReal : ℝ≥0∞) μ ≤ ENNReal.ofReal (ε ^ (1 / p)))
  (g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (↑p.toNNReal : ℝ≥0∞) μ),
  ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal p) μ
Tactic: rcases hf.exists_boundedContinuous_eLpNorm_sub_le ENNReal.coe_ne_top A with ⟨g, hg, g_mem⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α →ᵇ E
hg : eLpNorm (f - (⇑g : (a : α) → E)) (↑p.toNNReal : ℝ≥0∞) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (↑p.toNNReal : ℝ≥0∞) μ
⊢ ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal p) μ
have hg₁ : eLpNorm (f - (⇑g : (a : α) → E)) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
Tactic: change eLpNorm _ (ENNReal.ofReal p) _ ≤ _ at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α →ᵇ E
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (↑p.toNNReal : ℝ≥0∞) μ
hg : eLpNorm (f - (⇑g : (a : α) → E)) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
⊢ ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal p) μ
have refine : ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε
Tactic: refine ⟨g, ?_, g_mem⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α →ᵇ E
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (↑p.toNNReal : ℝ≥0∞) μ
hg : eLpNorm (f - (⇑g : (a : α) → E)) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
⊢ ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε
have rwa : ∀ (hg : HPow.hPow (α := ℝ) (∫ (a : α), ‖HSub.hSub (β := α → E) f (⇑g : (a : α) → E) a‖ ^ p ∂μ) p⁻¹ ≤ ε ^ p⁻¹),
  LE.le (α := ℝ) 0 (∫ (a : α), ‖HSub.hSub (β := α → E) f (⇑g : (a : α) → E) a‖ ^ p ∂μ)
Tactic: rwa [(hf.sub g_mem).eLpNorm_eq_integral_rpow_norm B ENNReal.coe_ne_top,
    ENNReal.ofReal_le_ofReal_iff I.le, one_div, ENNReal.toReal_ofReal hp.le,
    Real.rpow_le_rpow_iff _ hε.le (inv_pos.2 hp)] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ (g : α →ᵇ E),
    ∫⁻ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ₑ ∂μ ≤ ε ∧
      Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
have simp : ∀ (hf : MemLp f 1 μ),
  ∃ (g : α →ᵇ E),
    eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)) 1 μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) 1 μ
Tactic: simp only [← memLp_one_iff_integrable, ← eLpNorm_one_eq_lintegral_enorm] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
f : α → E
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ∂μ ≤ ε ∧
      Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
have simp : ∀ (hf : MemLp f (ENNReal.ofReal 1) μ),
  ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ∂μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal 1) μ
Tactic: simp only [← memLp_one_iff_integrable, ← ENNReal.ofReal_one]
    at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
f : ↥(Lp E p μ)
⊢ f ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(boundedContinuousFunction E p μ) : Set ↥(Lp E p μ))
have refine : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ y ∈ (↑(boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)), y ∈ Metric.closedEBall f ε
Tactic: refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedEBall).2 fun ε hε ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ y ∈ (↑(boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)), y ∈ Metric.closedEBall f ε
have obtain : ∀ (g : α →ᵇ E) (hg : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (⇑g : (a : α) → E)) p μ ≤ ε)
  (g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) p μ),
  ∃ y ∈ (↑(boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)), y ∈ Metric.closedEBall f ε
Tactic: obtain ⟨g, hg, g_mem⟩ :
      ∃ g : α →ᵇ E, eLpNorm ((f : α → E) - (g : α → E)) p μ ≤ ε ∧ MemLp g p μ :=
    (Lp.memLp f).exists_boundedContinuous_eLpNorm_sub_le hp hε.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (⇑g : (a : α) → E)) p μ ≤ ε
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) p μ
⊢ ∃ y ∈ (↑(boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)), y ∈ Metric.closedEBall f ε
have refine : MemLp.toLp (⇑g : (a : α) → E) g_mem ∈ Metric.closedEBall f ε
Tactic: refine ⟨g_mem.toLp _, ⟨g, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (⇑g : (a : α) → E)) p μ ≤ ε
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) p μ
⊢ MemLp.toLp (⇑g : (a : α) → E) g_mem ∈ Metric.closedEBall f ε
have rwa : edist f (MemLp.toLp (⇑g : (a : α) → E) g_mem) ≤ ε
Tactic: rwa [Metric.mem_closedEBall', ← Lp.toLp_coeFn f (Lp.memLp f), Lp.edist_toLp_toLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : SecondCountableTopologyEither α E
inst_7 : Fact (1 ≤ p)
hp : p ≠ ∞
inst_8 : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm ((↑(↑f : α →ₘ[μ] E) : α → E) - (⇑g : (a : α) → E)) p μ ≤ ε
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) p μ
rwa : edist f (MemLp.toLp (⇑g : (a : α) → E) g_mem) ≤ ε
⊢ MemLp.toLp (⇑g : (a : α) → E) g_mem ∈ Metric.closedEBall f ε
have rwa₁ : edist (MemLp.toLp (↑(↑f : α →ₘ[μ] E) : α → E) sorry) (MemLp.toLp (⇑g : (a : α) → E) g_mem) ≤ ε
Tactic: rwa [Metric.mem_closedEBall', ← Lp.toLp_coeFn f (Lp.memLp f), Lp.edist_toLp_toLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
inst_9 : NormedSpace ℝ E
inst_10 : CompactSpace α
inst_11 : μ.WeaklyRegular
inst_12 : IsFiniteMeasure μ
hp : p ≠ ∞
⊢ DenseRange (X := ↥(Lp E p μ)) (α := C(α, E)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ))
have refine : Subset (α := Set ↥(Lp E p μ))
  (range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))
  (range (ι := C(α, E)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)))
Tactic: refine (BoundedContinuousFunction.toLp_denseRange _ _ 𝕜 hp).mono ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
inst_9 : NormedSpace ℝ E
inst_10 : CompactSpace α
inst_11 : μ.WeaklyRegular
inst_12 : IsFiniteMeasure μ
hp : p ≠ ∞
⊢ Subset (α := Set ↥(Lp E p μ))
    (range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))
    (range (ι := C(α, E)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)))
have refine : ∀ (f : α →ᵇ E),
  Membership.mem (α := ↥(Lp E p μ)) (γ := Set ↥(Lp E p μ))
    (range (ι := C(α, E)) (⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)))
    ((BoundedContinuousFunction.toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
Tactic: refine range_subset_iff.2 fun f ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
i : ι
hX : ∀ (j : ι), IdentDistrib (X i) (X j) (μ i) (μ j)
hZ : IdentDistrib (X i) Z (μ i) μ'
⊢ Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) (μ n)) ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯))
have h : ∀ (j : ι), Eq (α := Measure E) (Measure.map (X j) (μ j)) (Measure.map Z μ')
Tactic: convert! tendsto_const_nhds with j
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X Y : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
T : Ω' → E
hXY : ∀ (i : ι), X i =ᶠ[ae (μ i)] Y i
hZT : Z =ᶠ[ae μ'] T
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
⊢ Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (Y n) (μ n)) ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') ⋯))
have h₁ : ∀ (n : ι),
  Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (Y n) (μ n)) sorry =
    Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) (μ n)) sorry
Tactic: convert! h.tendsto using 2 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_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X Y : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
T : Ω' → E
hXY : ∀ (i : ι), X i =ᶠ[ae (μ i)] Y i
hZT : Z =ᶠ[ae μ'] T
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
h₁ :
  ∀ (n : ι),
    Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (Y n) (μ n)) ⋯ =
      Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) (μ n)) ⋯
⊢ Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (Y n) (μ n)) ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') ⋯))
have h₂ : Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') sorry =
  Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') sorry
Tactic: convert! h.tendsto using 2 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_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X Y : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
T : Ω' → E
hXY : ∀ (i : ι), X i =ᶠ[ae (μ i)] Y i
hZT : Z =ᶠ[ae μ'] T
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
⊢ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') ⋯ =
    Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯
have h₁ : Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') sorry =
  Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') sorry
Tactic: rw! [Measure.map_congr hZT]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : IsEmpty E
⊢ Tendsto (β := ProbabilityMeasure E)
    (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) (μ n)) ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯))
have simp : Tendsto (β := ProbabilityMeasure E) (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) 0 sorry) l
  (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) 0 sorry))
Tactic: simp only [Subsingleton.elim _ (0 : Measure E)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_2 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_3 : TopologicalSpace E
inst_4 : HasOuterApproxClosed E
inst_5 : BorelSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
W : Ω'' → E
inst_6 : l.NeBot
h1 : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
h2 : TendstoInDistribution (Ω := Ω) (mE := mE) X l W μ μ''
⊢ Eq (α := Measure E) (Measure.map Z μ') (Measure.map W μ'')
have h_eq : Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') sorry =
  Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map W μ'') sorry
Tactic: have h_eq := tendsto_nhds_unique h1.tendsto h2.tendsto