-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNorm_indicator_const_le (c : G) (p : ℝ≥0∞) :
    eLpNorm (s.indicator fun _ => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Proof state:
case inl
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
⊢ eLpNorm (s.indicator fun x => c) 0 μ ≤ ‖c‖ₑ * μ s ^ (1 / ENNReal.toReal 0)

Tactic:
simp only [eLpNorm_exponent_zero, zero_le']

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hp : ⊤ ≠ 0
⊢ eLpNormEssSup (s.indicator fun x => c) μ ≤ ‖c‖ₑ

Tactic:
exact eLpNormEssSup_indicator_const_le _ _

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hp : ⊤ ≠ 0
⊢ eLpNorm (s.indicator fun x => c) ⊤ μ ≤ ‖c‖ₑ * μ s ^ (1 / ⊤.toReal)

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

Result:
case inr.inl
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hp : ⊤ ≠ 0
⊢ eLpNormEssSup (s.indicator fun x => c) μ ≤ ‖c‖ₑ

Proof state:
case inr.inr
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ⊤
t : Set α := toMeasurable μ s
⊢ eLpNorm (s.indicator fun x => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
calc
  eLpNorm (s.indicator fun _ => c) p μ ≤ eLpNorm (t.indicator fun _ => c) p μ :=
    eLpNorm_mono (norm_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]

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ⊤
⊢ eLpNorm (s.indicator fun x => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
let t := toMeasurable μ s

Result:
case inr.inr
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ⊤
t : Set α := toMeasurable μ s
⊢ eLpNorm (s.indicator fun x => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Proof state:
case inr
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
p : ℝ≥0∞
hp : p ≠ 0
⊢ eLpNorm (s.indicator fun x => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

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

Result:
case inr.inl
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hp : ⊤ ≠ 0
⊢ eLpNorm (s.indicator fun x => c) ⊤ μ ≤ ‖c‖ₑ * μ s ^ (1 / ⊤.toReal)

case inr.inr
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ⊤
⊢ eLpNorm (s.indicator fun x => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Proof state:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
p : ℝ≥0∞
⊢ eLpNorm (s.indicator fun x => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
obtain rfl | hp := eq_or_ne p 0

Result:
case inl
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
⊢ eLpNorm (s.indicator fun x => c) 0 μ ≤ ‖c‖ₑ * μ s ^ (1 / ENNReal.toReal 0)

case inr
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
p : ℝ≥0∞
hp : p ≠ 0
⊢ eLpNorm (s.indicator fun x => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Proof state:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ⊤
t : Set α := toMeasurable μ s
⊢ ‖c‖ₑ * μ t ^ (1 / p.toReal) = ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
rw [measure_toMeasurable]

Result:
no goals