awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
x : α
simp_rw : s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x ≤ ‖f x‖ₑ
⊢ LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ ‖s.indicator f x‖ₑ) x) ((fun (x : α) ↦ ‖f x‖ₑ) x)

Tactic:
simp_rw [enorm_indicator_eq_indicator_enorm]

Premises used: enorm_indicator_eq_indicator_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
x : α
⊢ s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x ≤ ‖f x‖ₑ

Tactic:
Set.indicator_le_self s _ x

Premises used: Set.indicator_le_self
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
x : α
⊢ s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x ≤ ‖f x‖ₑ

Tactic:
exact Set.indicator_le_self s _ x

Premises used: Set.indicator_le_self
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
inl : eLpNormEssSup.{u_1, u_7} (ε := ε) (m0 := m0) (s.indicator fun (x : α) ↦ c) 0 ≤ ‖c‖ₑ
inr : ∀ (hμ0 : μ ≠ 0), eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ ≤ ‖c‖ₑ
⊢ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ ≤ ‖c‖ₑ

Tactic:
obtain rfl | hμ0 := eq_or_ne μ 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
⊢ eLpNormEssSup.{u_1, u_7} (ε := ε) (m0 := m0) (s.indicator fun (x : α) ↦ c) 0 ≤ ‖c‖ₑ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
hμ0 : μ ≠ 0
⊢ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ ≤ ‖c‖ₑ

Tactic:
(eLpNormEssSup_indicator_le s fun _ => c).trans (eLpNormEssSup_const c hμ0).le

Premises used: MeasureTheory.eLpNormEssSup_const, Eq.le, LE.le.trans, MeasureTheory.eLpNormEssSup_indicator_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
hμ0 : μ ≠ 0
⊢ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ ≤ ‖c‖ₑ

Tactic:
exact (eLpNormEssSup_indicator_le s fun _ => c).trans (eLpNormEssSup_const c hμ0).le

Premises used: MeasureTheory.eLpNormEssSup_const, Eq.le, LE.le.trans, MeasureTheory.eLpNormEssSup_indicator_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ = ‖c‖ₑ

Tactic:
le_antisymm (eLpNormEssSup_indicator_const_le s c) ?_

Premises used: le_antisymm, MeasureTheory.eLpNormEssSup_indicator_const_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
refine : ‖c‖ₑ ≤ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ
⊢ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ = ‖c‖ₑ

Tactic:
refine le_antisymm (eLpNormEssSup_indicator_const_le s c) ?_

Premises used: le_antisymm, MeasureTheory.eLpNormEssSup_indicator_const_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
by_contra! : ∀ (h : eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ < ‖c‖ₑ), False
⊢ ‖c‖ₑ ≤ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ

Tactic:
by_contra! h
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h : eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ < ‖c‖ₑ
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) a) < ‖c‖ₑ} : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
have h' := ae_iff.mp (ae_lt_of_essSup_lt h)
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h : eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ < ‖c‖ₑ
h' :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) a) < ‖c‖ₑ} : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ‖c‖ₑ ≤ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) a)} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
push Not at h'

Premises used: Not
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h : eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ < ‖c‖ₑ
h' :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ‖c‖ₑ ≤ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) a)} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
hμs (measure_mono_null (fun x hx_mem => ?_) h')

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h : eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ < ‖c‖ₑ
h' :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ‖c‖ₑ ≤ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) a)} : ℝ≥0∞) (0 : ℝ≥0∞)
refine :
  ∀ (x : α) (hx_mem : x ∈ s),
    Membership.mem (γ := Set α) {a : α | ‖c‖ₑ ≤ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) a)} x
⊢ False

Tactic:
refine hμs (measure_mono_null (fun x hx_mem => ?_) h')

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h : eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ < ‖c‖ₑ
h' :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ‖c‖ₑ ≤ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) a)} : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx_mem : x ∈ s
rw : ‖c‖ₑ ≤ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) x)
rw₁ rw₂ : ‖c‖ₑ ≤ ‖c‖ₑ
⊢ Membership.mem (γ := Set α) {a : α | ‖c‖ₑ ≤ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) a)} x

Tactic:
rw [Set.mem_setOf_eq, Set.indicator_of_mem hx_mem]

Premises used: Set.mem_setOf_eq, Set.indicator_of_mem
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
e_a :
  Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) x) ^ p.toReal)
    fun (x : α) ↦ s.indicator (fun (x : α) ↦ ‖c‖ₑ ^ p.toReal) x
⊢ (∫⁻ (x : α), enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) x) ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α), s.indicator (fun (x : α) ↦ ‖c‖ₑ ^ p.toReal) x ∂μ) ^ (1 / p.toReal)

Tactic:
congr 2
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) x) ^ p.toReal)
    fun (x : α) ↦ s.indicator (fun (x : α) ↦ ‖c‖ₑ ^ p.toReal) x

Tactic:
(Set.comp_indicator_const c (fun x ↦ (‖x‖ₑ) ^ p.toReal) ?_)

Premises used: ENorm.enorm, ENNReal.toReal, HPow.hPow, Set.comp_indicator_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
e_a : Eq (α := ℝ≥0∞) ((fun (x : ε) ↦ ‖x‖ₑ ^ p.toReal) 0) 0
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) x) ^ p.toReal)
    fun (x : α) ↦ s.indicator (fun (x : α) ↦ ‖c‖ₑ ^ p.toReal) x

Tactic:
refine (Set.comp_indicator_const c (fun x ↦ (‖x‖ₑ) ^ p.toReal) ?_)

Premises used: ENorm.enorm, ENNReal.toReal, HPow.hPow, Set.comp_indicator_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ Eq (α := ℝ≥0∞) ((fun (x : ε) ↦ ‖x‖ₑ ^ p.toReal) 0) 0

Tactic:
simp [hp_pos]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
hz : 0 ≤ 1 / p.toReal
⊢ (∫⁻ (x : α), s.indicator (fun (x : α) ↦ ‖c‖ₑ ^ p.toReal) x ∂μ) ^ (1 / p.toReal) =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
rw [lintegral_indicator_const₀ hs, ENNReal.mul_rpow_of_nonneg, ← ENNReal.rpow_mul,
        mul_one_div_cancel hp_pos.ne', ENNReal.rpow_one]

Premises used: ENNReal.rpow_mul, ENNReal.mul_rpow_of_nonneg, ENNReal.rpow_one, mul_one_div_cancel, LT.lt.ne', MeasureTheory.lintegral_indicator_const₀
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ 0 ≤ 1 / p.toReal

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : MeasurableSet s
hp : p ≠ 0
hp_top : p ≠ ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
eLpNorm_indicator_const₀ hs.nullMeasurableSet hp hp_top

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.eLpNorm_indicator_const₀
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hp : p ≠ 0
pos :
  ∀ (hp_top : p = ∞),
    eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ =
      ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
neg :
  ∀ (hp_top : ¬p = ∞),
    eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ =
      ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
by_cases hp_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hp : p ≠ 0
hp_top : p = ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
simp [hp_top, eLpNormEssSup_indicator_const_eq s c hμs]

Premises used: MeasureTheory.eLpNormEssSup_indicator_const_eq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hp : p ≠ 0
hp_top : ¬p = ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
eLpNorm_indicator_const hs hp hp_top

Premises used: MeasureTheory.eLpNorm_indicator_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hp : p ≠ 0
hp_top : ¬p = ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
exact eLpNorm_indicator_const hs hp hp_top

Premises used: MeasureTheory.eLpNorm_indicator_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
inl :
  eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) 0 μ ≤
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / ENNReal.toReal 0)
inr :
  ∀ (hp : p ≠ 0),
    eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ ≤
      ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ ≤
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
obtain rfl | hp := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) 0 μ ≤
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / ENNReal.toReal 0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
hp : p ≠ 0
inr :
  ∀ (hp : Ne (α := ℝ≥0∞) ∞ 0),
    eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) ∞ μ ≤
      ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / ENNReal.toReal ∞)
inr₁ :
  ∀ (h'p : p ≠ ∞),
    eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ ≤
      ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ ≤
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
obtain rfl | h'p := eq_or_ne p ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hp : Ne (α := ℝ≥0∞) ∞ 0
inr : eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ ≤ ‖c‖ₑ
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) ∞ μ ≤
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / ENNReal.toReal ∞)

Tactic:
simp only [eLpNorm_exponent_top, ENNReal.toReal_top, _root_.div_zero, ENNReal.rpow_zero,
      mul_one]

Premises used: MeasureTheory.eLpNorm_exponent_top, ENNReal.rpow_zero, mul_one, ENNReal.toReal_top, div_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hp : Ne (α := ℝ≥0∞) ∞ 0
⊢ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ ≤ ‖c‖ₑ

Tactic:
eLpNormEssSup_indicator_const_le _ _

Premises used: MeasureTheory.eLpNormEssSup_indicator_const_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
hp : Ne (α := ℝ≥0∞) ∞ 0
⊢ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ ≤ ‖c‖ₑ

Tactic:
exact eLpNormEssSup_indicator_const_le _ _

Premises used: MeasureTheory.eLpNormEssSup_indicator_const_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ∞
t : Set α := toMeasurable μ s
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ ≤
    eLpNorm.{u_1, u_7} (ε := ε) (t.indicator fun (x : α) ↦ c) p μ

Tactic:
eLpNorm_mono_enorm (enorm_indicator_le_of_subset (subset_toMeasurable _ _) _)

Premises used: enorm_indicator_le_of_subset, MeasureTheory.subset_toMeasurable, MeasureTheory.eLpNorm_mono_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ∞
t : Set α := toMeasurable μ s
⊢ eLpNorm.{u_1, u_7} (ε := ε) (t.indicator fun (x : α) ↦ c) p μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (1 / p.toReal)

Tactic:
eLpNorm_indicator_const (measurableSet_toMeasurable ..) hp h'p

Premises used: MeasureTheory.measurableSet_toMeasurable, MeasureTheory.eLpNorm_indicator_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ∞
t : Set α := toMeasurable μ s
rw rw₁ :
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (1 / p.toReal) =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
rw [measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ∞
t : Set α := toMeasurable μ s
eLpNorm :
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (1 / p.toReal) =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ MeasureTheory.eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ ≤
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
calc
    eLpNorm (s.indicator fun _ => c) p μ ≤ eLpNorm (t.indicator fun _ ↦ c) p μ :=
      eLpNorm_mono_enorm (enorm_indicator_le_of_subset (subset_toMeasurable _ _) _)
    _ = ‖c‖ₑ * μ t ^ (1 / p.toReal) :=
      eLpNorm_indicator_const (measurableSet_toMeasurable ..) hp h'p
    _ = ‖c‖ₑ * μ s ^ (1 / p.toReal) := by rw [measure_toMeasurable]

Premises used: enorm_indicator_le_of_subset, Set.indicator, HDiv.hDiv, MeasureTheory.subset_toMeasurable, ENNReal.toReal, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.eLpNorm_mono_enorm, OfNat.ofNat, DFunLike.coe, MeasureTheory.eLpNorm_indicator_const, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
hs : MeasurableSet s
hf : MemLp f p μ
⊢ eLpNorm f p μ < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
hs : MeasurableSet s
⊢ MemLp (s.indicator f) p μ ↔ MemLp f p (μ.restrict s)

Tactic:
simp [MemLp, aestronglyMeasurable_indicator_iff hs, eLpNorm_indicator_eq_eLpNorm_restrict hs]

Premises used: MeasureTheory.MemLp, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict, aestronglyMeasurable_indicator_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) p (μ.restrict s)
⊢ MemLp.{u_1, u_4} (ε := E) (s.indicator fun (x : α) ↦ c) p μ

Tactic:
rw [memLp_indicator_iff_restrict hs]

Premises used: MeasureTheory.memLp_indicator_iff_restrict
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inl : MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ 0) p (μ.restrict s)
inr :
  ∀ (hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) p (μ.restrict s)
⊢ MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) p (μ.restrict s)

Tactic:
obtain rfl | hμ := hμsc

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
⊢ MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ 0) p (μ.restrict s)

Tactic:
MemLp.zero

Premises used: MeasureTheory.MemLp.zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
⊢ MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ 0) p (μ.restrict s)

Tactic:
exact MemLp.zero

Premises used: MeasureTheory.MemLp.zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have := Fact.mk hμ.lt_top