awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
⊢ (↑(Submodule.toAddSubgroup (module_M := Lp.instModule)
          (LinearMap.range (M := C(α, E)) (↑(toLp p μ 𝕜) : C(α, E) →ₗ[𝕜] ↥(Lp E p μ)))) :
      Set ↥(Lp E p μ)) =
    (↑(Lp.boundedContinuousFunction E p μ) : Set ↥(Lp E p μ))
have this : Function.Surjective (α := C(α, E)) (β := α →ᵇ E) (⇑(linearIsometryBoundedOfCompact α E 𝕜) : (a : C(α, E)) → α →ᵇ E)
Tactic: have := (linearIsometryBoundedOfCompact α E 𝕜).surjective
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
this :
  Function.Surjective (α := C(α, E)) (β := α →ᵇ E) (⇑(linearIsometryBoundedOfCompact α E 𝕜) : (a : C(α, E)) → α →ᵇ E)
⊢ (↑(Submodule.toAddSubgroup (module_M := Lp.instModule)
          (LinearMap.range (M := C(α, E)) (↑(toLp p μ 𝕜) : C(α, E) →ₗ[𝕜] ↥(Lp E p μ)))) :
      Set ↥(Lp E p μ)) =
    (↑(Lp.boundedContinuousFunction E p μ) : Set ↥(Lp E p μ))
have h : (↑(Lp.boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)) =
  Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
Tactic: convert! Function.Surjective.range_comp this (BoundedContinuousFunction.toLp (E := E) p μ 𝕜)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
this :
  Function.Surjective (α := C(α, E)) (β := α →ᵇ E) (⇑(linearIsometryBoundedOfCompact α E 𝕜) : (a : C(α, E)) → α →ᵇ E)
⊢ (↑(Lp.boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
have h : (↑(Submodule.toAddSubgroup (module_M := Lp.instModule)
        (LinearMap.range (M := α →ᵇ E) (↑(BoundedContinuousFunction.toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ)))) :
    Set ↥(Lp E p μ)) =
  Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
Tactic: rw [← BoundedContinuousFunction.range_toLp p μ (𝕜 := 𝕜), Submodule.coe_toAddSubgroup,
    LinearMap.coe_range, ContinuousLinearMap.coe_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
this :
  Function.Surjective (α := C(α, E)) (β := α →ᵇ E) (⇑(linearIsometryBoundedOfCompact α E 𝕜) : (a : C(α, E)) → α →ᵇ E)
h :
  (↑(Submodule.toAddSubgroup (module_M := Lp.instModule)
          (LinearMap.range (M := α →ᵇ E) (↑(BoundedContinuousFunction.toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ)))) :
      Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
⊢ (↑(Lp.boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
have h₁ : (↑(LinearMap.range (M := α →ᵇ E) (↑(BoundedContinuousFunction.toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ))) :
    Set ↥(Lp E p μ)) =
  Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
Tactic: rw [← BoundedContinuousFunction.range_toLp p μ (𝕜 := 𝕜), Submodule.coe_toAddSubgroup,
    LinearMap.coe_range, ContinuousLinearMap.coe_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
this :
  Function.Surjective (α := C(α, E)) (β := α →ᵇ E) (⇑(linearIsometryBoundedOfCompact α E 𝕜) : (a : C(α, E)) → α →ᵇ E)
h :
  (↑(Submodule.toAddSubgroup (module_M := Lp.instModule)
          (LinearMap.range (M := α →ᵇ E) (↑(BoundedContinuousFunction.toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ)))) :
      Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
h₁ :
  (↑(LinearMap.range (M := α →ᵇ E) (↑(BoundedContinuousFunction.toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ))) :
      Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
⊢ (↑(Lp.boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
have h₂ : Eq (α := Set ↥(Lp E p μ))
  (Set.range (ι := α →ᵇ E)
    (⇑(↑(BoundedContinuousFunction.toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ)) : (a : α →ᵇ E) → ↥(Lp E p μ)))
  (Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))
Tactic: rw [← BoundedContinuousFunction.range_toLp p μ (𝕜 := 𝕜), Submodule.coe_toAddSubgroup,
    LinearMap.coe_range, ContinuousLinearMap.coe_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
this :
  Function.Surjective (α := C(α, E)) (β := α →ᵇ E) (⇑(linearIsometryBoundedOfCompact α E 𝕜) : (a : C(α, E)) → α →ᵇ E)
h :
  (↑(Submodule.toAddSubgroup (module_M := Lp.instModule)
          (LinearMap.range (M := α →ᵇ E) (↑(BoundedContinuousFunction.toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ)))) :
      Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
h₁ :
  (↑(LinearMap.range (M := α →ᵇ E) (↑(BoundedContinuousFunction.toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ))) :
      Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
h₂ :
  Eq (α := Set ↥(Lp E p μ))
    (Set.range (ι := α →ᵇ E)
      (⇑(↑(BoundedContinuousFunction.toLp p μ 𝕜) : (α →ᵇ E) →ₗ[𝕜] ↥(Lp E p μ)) : (a : α →ᵇ E) → ↥(Lp E p μ)))
    (Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))
⊢ (↑(Lp.boundedContinuousFunction E p μ) : Set ↥(Lp E p μ)) =
    Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ))
have h₃ : Eq (α := Set ↥(Lp E p μ))
  (Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))
  (Set.range (ι := α →ᵇ E) (⇑(BoundedContinuousFunction.toLp p μ 𝕜) : (a : α →ᵇ E) → ↥(Lp E p μ)))
Tactic: rw [← BoundedContinuousFunction.range_toLp p μ (𝕜 := 𝕜), Submodule.coe_toAddSubgroup,
    LinearMap.coe_range, ContinuousLinearMap.coe_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
β : Type u_4
inst_10 : μ.IsOpenPosMeasure
g : β → C(α, E)
f : C(α, E)
hg : Summable g
hg2 :
  HasSum (α := ↥(Lp E p μ)) ((⇑(toLp p μ 𝕜) : (a : C(α, E)) → ↥(Lp E p μ)) ∘ g : β → ↥(Lp E p μ))
    ((toLp p μ 𝕜 : (a : C(α, E)) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
⊢ HasSum g f
have h : f = ∑' (b : β), g b
Tactic: convert! Summable.hasSum hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
inst_6 : Fact (1 ≤ p)
𝕜 : Type u_4
inst_7 : NontriviallyNormedField 𝕜
inst_8 : NormedSpace 𝕜 E
⊢ norm (E := C(α, E) →L[𝕜] ↥(Lp E p μ)) (toLp p μ 𝕜) ≤ (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹
have rw : norm (E := (α →ᵇ E) →L[𝕜] ↥(Lp E p μ)) (BoundedContinuousFunction.toLp p μ 𝕜) ≤
  (↑(measureUnivNNReal μ) : ℝ) ^ p.toReal⁻¹
Tactic: rw [toLp_norm_eq_toLp_norm_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
inst_6 : Fact (1 ≤ p)
𝕜' : Type u_5
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' E
f : C(α, E)
⊢ MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) p μ
have this : MemLp.{u_1, u_2} (ε := E) (↑(↑((toLp p μ 𝕜' : (a : C(α, E)) → ↥(Lp E p μ)) f) : α →ₘ[μ] E) : α → E) p μ
Tactic: have := Lp.mem_Lp_iff_memLp.mp (Subtype.val_prop (f.toLp p μ 𝕜'))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
inst_6 : Fact (1 ≤ p)
𝕜' : Type u_5
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' E
f : C(α, E)
this : MemLp.{u_1, u_2} (ε := E) (↑(↑((toLp p μ 𝕜' : (a : C(α, E)) → ↥(Lp E p μ)) f) : α →ₘ[μ] E) : α → E) p μ
⊢ MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) p μ
have rwa : ∀ (this : MemLp (↑(toAEEqFun μ f) : α → E) p μ), MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) p μ
Tactic: rwa [coe_toLp, memLp_congr_ae (coeFn_toAEEqFun _ _)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
inst_6 : Fact (1 ≤ p)
𝕜' : Type u_5
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' E
f : C(α, E)
this : MemLp.{u_1, u_2} (ε := E) (↑(↑((toLp p μ 𝕜' : (a : C(α, E)) → ↥(Lp E p μ)) f) : α →ₘ[μ] E) : α → E) p μ
rwa : ∀ (this : MemLp (↑(toAEEqFun μ f) : α → E) p μ), MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) p μ
⊢ MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) p μ
have rwa₁ : ∀ (this : MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) p μ), MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) p μ
Tactic: rwa [coe_toLp, memLp_congr_ae (coeFn_toAEEqFun _ _)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic (goal)
Goal:
M : Type u_1
α : Type u_3
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_2 : SMul M α
inst_3 : SMulInvariantMeasure M α μ
inst_4 : MeasurableConstSMul M α
c : Mᵈᵐᵃ
f : ↥(Lp E p μ)
⊢ c • -f = -(c • f)
have mk : ∀ (val : α →ₘ[μ] E) (a : { f : α → E // AEStronglyMeasurable f μ })
  (property :
    Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ)
      (Quot.mk
        (⇑(Measure.aeEqSetoid E μ) :
          { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
        a)),
  c •
      -Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a)
          property =
    -(c •
        Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μ) :
              { f : α → E // AEStronglyMeasurable f μ } → { f : α → E // AEStronglyMeasurable f μ } → Prop)
            a)
          property)
Tactic: rcases f with ⟨⟨_⟩, _⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
have inl : ∀ (hp : Ne (α := ℝ≥0∞) 0 ∞),
  ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) 0 μ ≤ ε
Tactic: rcases eq_or_ne p 0 with (rfl | h'p)
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
inl :
  ∀ (hp : Ne (α := ℝ≥0∞) 0 ∞),
    ∃ (η : ℝ≥0),
      0 < η ∧
        ∀ (s : Set α),
          (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) 0 μ ≤ ε
⊢ ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
have inr : ∀ (h'p : p ≠ 0),
  ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
Tactic: rcases eq_or_ne p 0 with (rfl | h'p)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
⊢ ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
have hp₀ : 0 < p
Tactic: have hp₀ : 0 < p := bot_lt_iff_ne_bot.2 h'p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
⊢ ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
have hp₀' : 0 ≤ 1 / p.toReal
Tactic: have hp₀' : 0 ≤ 1 / p.toReal := div_nonneg zero_le_one ENNReal.toReal_nonneg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
⊢ ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
have hp₀'' : 0 < p.toReal
Tactic: have hp₀'' : 0 < p.toReal := ENNReal.toReal_pos hp₀.ne' hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ Tendsto (fun (x : ℝ≥0) ↦ (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞)) (𝓝 0) (𝓝 (↑0 : ℝ≥0∞))
have rw : Tendsto (β := ℝ≥0) (fun (x : ℝ≥0) ↦ ‖c‖₊ * x ^ (1 / p.toReal)) (𝓝 0) (𝓝 0)
Tactic: rw [ENNReal.tendsto_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ Tendsto (β := ℝ≥0) (fun (x : ℝ≥0) ↦ ‖c‖₊ * x ^ (1 / p.toReal)) (𝓝 0) (𝓝 0)
have h : 0 = ‖c‖₊ * HPow.hPow (α := ℝ≥0) 0 (1 / p.toReal)
Tactic: convert! (NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ ∃ (η : ℝ≥0), 0 < η ∧ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
have this : Tendsto (fun (x : ℝ≥0) ↦ (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞)) (𝓝 0) (𝓝 (↑0 : ℝ≥0∞))
Tactic: have :
      Filter.Tendsto (fun x : ℝ≥0 => ((‖c‖₊ * x ^ (1 / p.toReal) : ℝ≥0) : ℝ≥0∞)) (𝓝 0)
        (𝓝 (0 : ℝ≥0)) := by
      rw [ENNReal.tendsto_coe]
      convert! (NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _
      simp [hp₀''.ne']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun (x : ℝ≥0) ↦ (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞)) (𝓝 0) (𝓝 (↑0 : ℝ≥0∞))
⊢ ∃ (η : ℝ≥0), 0 < η ∧ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
have hε' : 0 < ε
Tactic: have hε' : 0 < ε := hε.bot_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun (x : ℝ≥0) ↦ (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞)) (𝓝 0) (𝓝 (↑0 : ℝ≥0∞))
hε' : 0 < ε
⊢ ∃ (η : ℝ≥0), 0 < η ∧ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
have obtain : ∀ (δ : ℝ≥0) (hδ : 0 < δ) (hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞) ≤ ε),
  ∃ (η : ℝ≥0), 0 < η ∧ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
Tactic: obtain ⟨δ, hδ, hδε'⟩ := NNReal.nhds_zero_basis.eventually_iff.mp (this.eventually_le_const hε')
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun (x : ℝ≥0) ↦ (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞)) (𝓝 0) (𝓝 (↑0 : ℝ≥0∞))
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞) ≤ ε
⊢ ∃ (η : ℝ≥0), 0 < η ∧ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
have obtain : ∀ (η : ℝ≥0) (hη : 0 < η) (hηδ : η < δ), ∃ (η : ℝ≥0), 0 < η ∧ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
Tactic: obtain ⟨η, hη, hηδ⟩ := exists_between hδ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun (x : ℝ≥0) ↦ (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞)) (𝓝 0) (𝓝 (↑0 : ℝ≥0∞))
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞) ≤ ε
η : ℝ≥0
hη : 0 < η
hηδ : η < δ
⊢ ∃ (η : ℝ≥0), 0 < η ∧ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
have refine : ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
Tactic: refine ⟨η, hη, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
have inr : ∀ (η : ℝ≥0) (hη_pos : 0 < η) (hη_le : ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε),
  ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
Tactic: obtain ⟨η, hη_pos, hη_le⟩ : ∃ η : ℝ≥0, 0 < η ∧ ‖c‖ₑ * (η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε := by
    have :
      Filter.Tendsto (fun x : ℝ≥0 => ((‖c‖₊ * x ^ (1 / p.toReal) : ℝ≥0) : ℝ≥0∞)) (𝓝 0)
        (𝓝 (0 : ℝ≥0)) := by
      rw [ENNReal.tendsto_coe]
      convert! (NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _
      simp [hp₀''.ne']
    have hε' : 0 < ε := hε.bot_lt
    obtain ⟨δ, hδ, hδε'⟩ := NNReal.nhds_zero_basis.eventually_iff.mp (this.eventually_le_const hε')
    obtain ⟨η, hη, hηδ⟩ := exists_between hδ
    refine ⟨η, hη, ?_⟩
    simpa only [← ENNReal.coe_rpow_of_nonneg _ hp₀', enorm, ← ENNReal.coe_mul] using hδε' hηδ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
η : ℝ≥0
hη_pos : 0 < η
hη_le : ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
⊢ ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
have inr : ∀ (s : Set α) (hs : (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞)),
  eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
Tactic: refine ⟨η, hη_pos, fun s hs => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
η : ℝ≥0
hη_pos : 0 < η
hη_le : ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞)
⊢ eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
have inr : ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤ ε
Tactic: grw [eLpNorm_indicator_const_le, ← hη_le, hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
η : ℝ≥0
hη_pos : 0 < η
hη_le : ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞)
inr : ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤ ε
⊢ eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
have inr₁ : ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal)
Tactic: grw [eLpNorm_indicator_const_le, ← hη_le, hs]