awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
x : β
n : ℕ
this : edist ((approxOn f hf s y₀ h₀ n : (a : β) → E) x) (f x) ≤ edist (f x) y₀
⊢ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖₊ ≤ ‖f x - y₀‖₊
have this₁ : (↑‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖₊ : ℝ≥0∞) ≤ (↑‖f x - y₀‖₊ : ℝ≥0∞)
Tactic: simp only [edist_nndist, nndist_eq_nnnorm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)
have pos : ∀ (hp_zero : p = 0),
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
pos :
  ∀ (hp_zero : p = 0),
    Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)
have neg : ∀ (hp_zero : ¬p = 0),
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)
have hp : 0 < p.toReal
Tactic: have hp : 0 < p.toReal := toReal_pos hp_zero hp_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
this :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)
have simp : Tendsto (β := ℝ≥0∞)
  (fun (n : ℕ) ↦
    (∫⁻ (x : β), ‖HSub.hSub (α := (a : β) → E) (⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) f x‖ₑ ^ p.toReal ∂μ) ^
      (1 / p.toReal))
  atTop (𝓝 0)
Tactic: simp only [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
this :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      (∫⁻ (x : β), ‖HSub.hSub (α := (a : β) → E) (⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) f x‖ₑ ^ p.toReal ∂μ) ^
        (1 / p.toReal))
    atTop (𝓝 0)
have h : 0 = HPow.hPow (α := ℝ≥0∞) 0 (1 / p.toReal)
Tactic: convert! continuous_rpow_const.continuousAt.tendsto.comp this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((⇑(approxOn f hf s y₀ h₀ n) : (a : β) → E) - f) p μ) atTop (𝓝 0)
have neg : Tendsto (β := ℝ≥0∞)
  (fun (n : ℕ) ↦ ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
  atTop (𝓝 0)
Tactic: suffices Tendsto (fun n => ∫⁻ x, ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0) by
    simp only [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_ne_top]
    convert! continuous_rpow_const.continuousAt.tendsto.comp this
    simp [zero_rpow_of_pos (_root_.inv_pos.mpr hp)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
    atTop (𝓝 0)
have hF_meas : ∀ (n : ℕ),
  Measurable (β := ℝ≥0∞) fun (x : β) ↦
    ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal
Tactic: have hF_meas n : Measurable fun x => ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal := by
    simpa only [← edist_eq_enorm_sub] using
      (approxOn f hf s y₀ h₀ n).measurable_bind (fun y x => edist y (f x) ^ p.toReal) fun y =>
        (measurable_edist_right.comp hf).pow_const p.toReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (x : β) ↦
      ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
    atTop (𝓝 0)
have h_bound : ∀ (n : ℕ),
  (ae μ).EventuallyLE (β := ℝ≥0∞)
    (fun (x : β) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal) fun (x : β) ↦
    ‖f x - y₀‖ₑ ^ p.toReal
Tactic: have h_bound n :
    (fun x ↦ ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal) ≤ᵐ[μ] (‖f · - y₀‖ₑ ^ p.toReal) :=
    .of_forall fun x => rpow_le_rpow (coe_mono (nnnorm_approxOn_le hf h₀ x n)) toReal_nonneg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (x : β) ↦
      ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal
h_bound :
  ∀ (n : ℕ),
    (ae μ).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal)
      fun (x : β) ↦ ‖f x - y₀‖ₑ ^ p.toReal
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
    atTop (𝓝 0)
have h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
Tactic: have h_fin : (∫⁻ a : β, ‖f a - y₀‖ₑ ^ p.toReal ∂μ) ≠ ⊤ :=
    (lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_zero hp_ne_top hi).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (x : β) ↦
      ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal
h_bound :
  ∀ (n : ℕ),
    (ae μ).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal)
      fun (x : β) ↦ ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
⊢ ∀ᵐ (a : β) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (x : ℕ) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ x : (a : β) → E) a : E) (f a)‖ₑ ^ p.toReal) atTop (𝓝 0)
have h : ∀ (a : β) (ha : f a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
  Tendsto (β := ℝ≥0∞)
    (fun (x : ℕ) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ x : (a : β) → E) a : E) (f a)‖ₑ ^ p.toReal) atTop (𝓝 0)
Tactic: filter_upwards [hμ] with a ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (x : β) ↦
      ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal
h_bound :
  ∀ (n : ℕ),
    (ae μ).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal)
      fun (x : β) ↦ ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
a : β
ha : f a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (β := ℝ≥0∞)
    (fun (x : ℕ) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ x : (a : β) → E) a : E) (f a)‖ₑ ^ p.toReal) atTop (𝓝 0)
have this : Tendsto (fun (n : ℕ) ↦ HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) a : E) (f a)) atTop (𝓝 (f a - f a))
Tactic: have : Tendsto (fun n => (approxOn f hf s y₀ h₀ n) a - f a) atTop (𝓝 (f a - f a)) :=
      (tendsto_approxOn hf h₀ ha).sub tendsto_const_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (x : β) ↦
      ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal
h_bound :
  ∀ (n : ℕ),
    (ae μ).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal)
      fun (x : β) ↦ ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
a : β
ha : f a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
this :
  Tendsto (fun (n : ℕ) ↦ HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) a : E) (f a)) atTop (𝓝 (f a - f a))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (x : ℕ) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ x : (a : β) → E) a : E) (f a)‖ₑ ^ p.toReal) atTop (𝓝 0)
have h : 0 = (↑‖f a - f a‖₊ : ℝ≥0∞) ^ p.toReal
Tactic: convert! continuous_rpow_const.continuousAt.tendsto.comp (tendsto_coe.mpr this.nnnorm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (x : β) ↦
      ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal
h_bound :
  ∀ (n : ℕ),
    (ae μ).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal)
      fun (x : β) ↦ ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : β), ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖ₑ ^ p.toReal ∂μ)
    atTop (𝓝 0)
have h_lim : ∀ᵐ (a : β) ∂μ,
  Tendsto (β := ℝ≥0∞)
    (fun (x : ℕ) ↦ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ x : (a : β) → E) a : E) (f a)‖ₑ ^ p.toReal) atTop (𝓝 0)
Tactic: have h_lim :
    ∀ᵐ a : β ∂μ, Tendsto (‖approxOn f hf s y₀ h₀ · a - f a‖ₑ ^ p.toReal) atTop (𝓝 0) := by
    filter_upwards [hμ] with a ha
    have : Tendsto (fun n => (approxOn f hf s y₀ h₀ n) a - f a) atTop (𝓝 (f a - f a)) :=
      (tendsto_approxOn hf h₀ ha).sub tendsto_const_nhds
    convert! continuous_rpow_const.continuousAt.tendsto.comp (tendsto_coe.mpr this.nnnorm)
    simp [zero_rpow_of_pos hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) p μ
n : ℕ
⊢ MemLp.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) p μ
have refine : eLpNorm.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) p μ < ∞
Tactic: refine ⟨(approxOn f fmeas s y₀ h₀ n).aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) p μ
n : ℕ
this :
  eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
      μ <
    ∞
⊢ eLpNorm.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) p μ < ∞
have this₁ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p μ
Tactic: have : MemLp (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ :=
      ⟨(approxOn f fmeas s y₀ h₀ n - const β y₀).aestronglyMeasurable, this⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) p μ
n : ℕ
this_1 :
  eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
      μ <
    ∞
this :
  MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p μ
⊢ eLpNorm.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) p μ < ∞
have h : (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) =
  HAdd.hAdd (α := β → E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀)
    fun (x : β) ↦ y₀
Tactic: convert! eLpNorm_add_lt_top this hi₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) p μ
n : ℕ
this_1 :
  eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
      μ <
    ∞
this :
  MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p μ
⊢ (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) =
    HAdd.hAdd (α := β → E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀)
      fun (x : β) ↦ y₀
have h : ∀ (x : β),
  (approxOn f fmeas s y₀ h₀ n : (a : β) → E) x =
    HAdd.hAdd (α := β → E) (β := β → E)
      (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) (fun (x : β) ↦ y₀) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) p μ
n : ℕ
⊢ eLpNorm.{u_2, u_4} (ε := E) (⇑(approxOn f fmeas s y₀ h₀ n) : (a : β) → E) p μ < ∞
have suffices : eLpNorm.{u_2, u_4} (ε := E) (fun (x : β) ↦ HSub.hSub (α := E) ((approxOn f fmeas s y₀ h₀ n : (a : β) → E) x : E) y₀) p
    μ <
  ∞
Tactic: suffices eLpNorm (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ < ⊤ by
    have : MemLp (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ :=
      ⟨(approxOn f fmeas s y₀ h₀ n - const β y₀).aestronglyMeasurable, this⟩
    convert! eLpNorm_add_lt_top this hi₀
    ext x
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) p μ
n : ℕ
⊢ Measurable (β := ℝ) fun (x : β) ↦ ‖f x - y₀‖
have simp : Measurable (β := ℝ) fun (x : β) ↦ dist (f x) y₀
Tactic: simp only [← dist_eq_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) p μ
n : ℕ
⊢ Measurable (β := ℝ) fun (x : β) ↦ dist (f x) y₀
have funProp : inst_1 ≤ inst_1
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) p μ
n : ℕ
funProp : inst_1 ≤ inst_1
⊢ Measurable (β := ℝ) fun (x : β) ↦ dist (f x) y₀
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (x2 : E) ↦ dist x2 y₀
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) p μ
n : ℕ
⊢ MemLp (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖) p μ
have h_meas : Measurable (β := ℝ) fun (x : β) ↦ ‖f x - y₀‖
Tactic: have h_meas : Measurable fun x => ‖f x - y₀‖ := by
      simp only [← dist_eq_norm]
      fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (goal)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
p : ℝ≥0∞
inst_3 : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
hi₀ : MemLp.{u_2, u_4} (ε := E) (fun (x : β) ↦ y₀) p μ
n : ℕ
h_meas : Measurable (β := ℝ) fun (x : β) ↦ ‖f x - y₀‖
⊢ MemLp (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖) p μ
have refine : eLpNorm (ε := ℝ) (fun (x : β) ↦ ‖f x - y₀‖) p μ < ∞
Tactic: refine ⟨h_meas.aemeasurable.aestronglyMeasurable, ?_⟩