awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
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 < ε
obtain :
  ∀ (δ : ℝ≥0) (hδ : 0 < δ) (hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → (↑(‖c‖₊ * x ^ (1 / p.toReal)) : ℝ≥0∞) ≤ ε),
    ∃ (η : ℝ≥0), 0 < η ∧ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
⊢ ∃ (η : ℝ≥0), 0 < η ∧ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε

Tactic:
obtain ⟨δ, hδ, hδε'⟩ := NNReal.nhds_zero_basis.eventually_iff.mp (this.eventually_le_const hε')

Premises used: Filter.Tendsto.eventually_le_const, Iff.mp, Filter.HasBasis.eventually_iff, NNReal.nhds_zero_basis
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
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∞) ≤ ε
obtain : ∀ (η : ℝ≥0) (hη : 0 < η) (hηδ : η < δ), ∃ (η : ℝ≥0), 0 < η ∧ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
⊢ ∃ (η : ℝ≥0), 0 < η ∧ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε

Tactic:
obtain ⟨η, hη, hηδ⟩ := exists_between hδ

Premises used: exists_between
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
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) ≤ ε

Tactic:
⟨η, hη, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
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ηδ : η < δ
refine : ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε
⊢ ∃ (η : ℝ≥0), 0 < η ∧ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε

Tactic:
refine ⟨η, hη, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
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ηδ : η < δ
⊢ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε

Tactic:
simpa only [← ENNReal.coe_rpow_of_nonneg _ hp₀', enorm, ← ENNReal.coe_mul] using hδε' hηδ

Premises used: ENNReal.coe_rpow_of_nonneg, ENNReal.coe_mul, ENorm.enorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
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
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 μ ≤ ε
⊢ ∃ (η : ℝ≥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ηδ

Premises used: HDiv.hDiv, ENNReal.toReal, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
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 μ ≤ ε

Tactic:
⟨η, hη_pos, fun s hs => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
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) ≤ ε
inr :
  ∀ (s : Set α) (hs : (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞)),
    eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε
⊢ ∃ (η : ℝ≥0),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε

Tactic:
refine ⟨η, hη_pos, fun s hs => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
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) ≤ ε
inr₁ :
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal)
inr₂ inr₃ : ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ‖c‖ₑ * (↑η : ℝ≥0∞) ^ (1 / p.toReal)
⊢ eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ε

Tactic:
grw [eLpNorm_indicator_const_le, ← hη_le, hs]

Premises used: MeasureTheory.eLpNorm_indicator_const_le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
E : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup E
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
⊢ MemLp f ∞ μ

Tactic:
have := memLp_top_of_bound h2f C hfC
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
E : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup E
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
this : MemLp f ∞ μ
⊢ MemLp f p μ

Tactic:
this.mono_exponent_of_measure_support_ne_top
    (fun x ↦ image_eq_zero_of_notMem_tsupport) (hf.measure_lt_top.ne) le_top

Premises used: MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top, image_eq_zero_of_notMem_tsupport, IsCompact.measure_lt_top, le_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
E : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup E
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
this : MemLp f ∞ μ
⊢ MemLp f p μ

Tactic:
exact this.mono_exponent_of_measure_support_ne_top
    (fun x ↦ image_eq_zero_of_notMem_tsupport) (hf.measure_lt_top.ne) le_top

Premises used: MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top, image_eq_zero_of_notMem_tsupport, IsCompact.measure_lt_top, le_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
E : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup E
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ≥0∞
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ₑ ≤ C
hC : C ≠ ∞
⊢ MemLp f ∞ μ

Tactic:
have : MemLp f ∞ μ :=
    ⟨h2f, eLpNormEssSup_le_of_ae_enorm_bound hfC |>.trans_lt hC.lt_top⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
E : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup E
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ≥0∞
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ₑ ≤ C
hC : C ≠ ∞
this : MemLp f ∞ μ
⊢ MemLp f p μ

Tactic:
this.mono_exponent_of_measure_support_ne_top
    (fun x ↦ image_eq_zero_of_notMem_tsupport) hf.measure_ne_top le_top

Premises used: MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top, image_eq_zero_of_notMem_tsupport, le_top, IsCompact.measure_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
E : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup E
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ≥0∞
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ₑ ≤ C
hC : C ≠ ∞
this : MemLp f ∞ μ
⊢ MemLp f p μ

Tactic:
exact this.mono_exponent_of_measure_support_ne_top
    (fun x ↦ image_eq_zero_of_notMem_tsupport) hf.measure_ne_top le_top

Premises used: MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top, image_eq_zero_of_notMem_tsupport, le_top, IsCompact.measure_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
E : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup E
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
⊢ MemLp f ∞ μ

Tactic:
have := hf.memLp_top_of_hasCompactSupport h'f μ
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
E : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup E
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
this : MemLp f ∞ μ
⊢ MemLp f p μ

Tactic:
this.mono_exponent_of_measure_support_ne_top
    (fun x ↦ image_eq_zero_of_notMem_tsupport) (h'f.measure_lt_top.ne) le_top

Premises used: MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top, image_eq_zero_of_notMem_tsupport, IsCompact.measure_lt_top, le_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
E : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup E
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
this : MemLp f ∞ μ
⊢ MemLp f p μ

Tactic:
exact this.mono_exponent_of_measure_support_ne_top
    (fun x ↦ image_eq_zero_of_notMem_tsupport) (h'f.measure_lt_top.ne) le_top

Premises used: MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top, image_eq_zero_of_notMem_tsupport, IsCompact.measure_lt_top, le_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c c' : E
simp_rw :
  MemLp.toLp (HAdd.hAdd (α := α → E) (s.indicator fun (x : α) ↦ c) (s.indicator fun (x : α) ↦ c')) ⋯ =
    MemLp.toLp (fun (a : α) ↦ HAdd.hAdd (α := E) (s.indicator (fun (x : α) ↦ c) a) (s.indicator (fun (x : α) ↦ c') a)) ⋯
⊢ HAdd.hAdd (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := s) p hs hμs c') =
    indicatorConstLp (s := s) p hs hμs (c + c')

Tactic:
simp_rw [indicatorConstLp, ← MemLp.toLp_add, indicator_add]

Premises used: MeasureTheory.indicatorConstLp, MeasureTheory.MemLp.toLp_add, Set.indicator_add
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c c' : E
⊢ MemLp.toLp (HAdd.hAdd (α := α → E) (s.indicator fun (x : α) ↦ c) (s.indicator fun (x : α) ↦ c')) ⋯ =
    MemLp.toLp (fun (a : α) ↦ HAdd.hAdd (α := E) (s.indicator (fun (x : α) ↦ c) a) (s.indicator (fun (x : α) ↦ c') a)) ⋯

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c c' : E
simp_rw :
  MemLp.toLp (HSub.hSub (α := α → E) (s.indicator fun (x : α) ↦ c) (s.indicator fun (x : α) ↦ c')) ⋯ =
    MemLp.toLp (fun (a : α) ↦ HSub.hSub (α := E) (s.indicator (fun (x : α) ↦ c) a) (s.indicator (fun (x : α) ↦ c') a)) ⋯
⊢ HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := s) p hs hμs c') =
    indicatorConstLp (s := s) p hs hμs (c - c')

Tactic:
simp_rw [indicatorConstLp, ← MemLp.toLp_sub, indicator_sub]

Premises used: MeasureTheory.indicatorConstLp, Set.indicator_sub, MeasureTheory.MemLp.toLp_sub
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c c' : E
⊢ MemLp.toLp (HSub.hSub (α := α → E) (s.indicator fun (x : α) ↦ c) (s.indicator fun (x : α) ↦ c')) ⋯ =
    MemLp.toLp (fun (a : α) ↦ HSub.hSub (α := E) (s.indicator (fun (x : α) ↦ c) a) (s.indicator (fun (x : α) ↦ c') a)) ⋯

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] s.indicator fun (x : α) ↦ c

Tactic:
MemLp.coeFn_toLp (memLp_indicator_const p hs c (Or.inr hμs))

Premises used: MeasureTheory.memLp_indicator_const, MeasureTheory.MemLp.coeFn_toLp, Or.inr
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) x = c

Tactic:
indicatorConstLp_coeFn.mono fun _x hx hxs => hx.trans (Set.indicator_of_mem hxs _)

Premises used: Filter.Eventually.mono, Set.indicator_of_mem, MeasureTheory.indicatorConstLp_coeFn, Eq.trans
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ ∀ᵐ (x : α) ∂μ, x ∉ s → (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) x = 0

Tactic:
indicatorConstLp_coeFn.mono fun _x hx hxs => hx.trans (Set.indicator_of_notMem hxs _)

Premises used: Filter.Eventually.mono, Set.indicator_of_notMem, MeasureTheory.indicatorConstLp_coeFn, Eq.trans
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
rw :
  (eLpNorm (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ] E) : α → E) p μ).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ).toReal = ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₂ :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₃ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real s ^ (1 / p.toReal)
rw₄ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) ^ (1 / p.toReal)
rw₅ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal
rw₆ rw₇ :
  ‖c‖ * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)).toReal
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const hs hp_ne_zero hp_ne_top, ENNReal.toReal_mul, measureReal_def,
    ENNReal.toReal_rpow, toReal_enorm]

Premises used: toReal_enorm, ENNReal.toReal_mul, MeasureTheory.measureReal_def, ENNReal.toReal_rpow, MeasureTheory.eLpNorm_congr_ae, MeasureTheory.indicatorConstLp_coeFn, MeasureTheory.eLpNorm_indicator_const, MeasureTheory.Lp.norm_def
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hμs_ne_zero : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : (eLpNorm (↑(↑(indicatorConstLp (s := s) ∞ hs hμs c) : α →ₘ[μ] E) : α → E) ∞ μ).toReal = ‖c‖
rw₁ : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) ∞ μ).toReal = ‖c‖
rw₂ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / ENNReal.toReal ∞)).toReal = ‖c‖
rw₃ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / 0)).toReal = ‖c‖
rw₄ : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) (β := ℝ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) 0).toReal = ‖c‖
rw₅ : (‖c‖ₑ * 1).toReal = ‖c‖
rw₆ : ‖c‖ₑ.toReal = ‖c‖
rw₇ rw₈ : ‖c‖ = ‖c‖
⊢ norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖

Tactic:
rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero, ENNReal.toReal_top,
    _root_.div_zero, ENNReal.rpow_zero, mul_one, toReal_enorm]

Premises used: toReal_enorm, ENNReal.rpow_zero, MeasureTheory.eLpNorm_indicator_const', mul_one, ENNReal.toReal_top, ENNReal.top_ne_zero, MeasureTheory.eLpNorm_congr_ae, div_zero, MeasureTheory.indicatorConstLp_coeFn, MeasureTheory.Lp.norm_def
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_pos : p ≠ 0
hμs_pos : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀ (hp_top : p = ∞), norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
neg :
  ∀ (hp_top : ¬p = ∞), norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
by_cases hp_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_pos : p ≠ 0
hμs_pos : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hp_top : p = ∞
pos : norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
rw [hp_top, ENNReal.toReal_top, _root_.div_zero, Real.rpow_zero, mul_one]

Premises used: Real.rpow_zero, mul_one, ENNReal.toReal_top, div_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_pos : p ≠ 0
hμs_pos : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hp_top : p = ∞
⊢ norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖

Tactic:
norm_indicatorConstLp_top hμs_pos

Premises used: MeasureTheory.norm_indicatorConstLp_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_pos : p ≠ 0
hμs_pos : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hp_top : p = ∞
⊢ norm (E := ↥(Lp E ∞ μ)) (indicatorConstLp (s := s) ∞ hs hμs c) = ‖c‖

Tactic:
exact norm_indicatorConstLp_top hμs_pos

Premises used: MeasureTheory.norm_indicatorConstLp_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_pos : p ≠ 0
hμs_pos : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hp_top : ¬p = ∞
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
norm_indicatorConstLp hp_pos hp_top

Premises used: MeasureTheory.norm_indicatorConstLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp_pos : p ≠ 0
hμs_pos : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hp_top : ¬p = ∞
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) = ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
exact norm_indicatorConstLp hp_pos hp_top

Premises used: MeasureTheory.norm_indicatorConstLp