awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : p = ∞
pos : eLpNorm (s.indicator f) ∞ μ = eLpNorm f ∞ (μ.restrict s)
pos₁ : eLpNormEssSup (s.indicator f) μ = eLpNormEssSup f (μ.restrict s)
pos₂ : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖s.indicator f x‖ₑ) μ) (essSup (fun (x : α) ↦ ‖f x‖ₑ) (μ.restrict s))
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
have pos₃ : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x) μ)
  (essSup (fun (a : α) ↦ ‖f a‖ₑ) (μ.restrict s))
Tactic: simp_rw [hp_top, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm,
       enorm_indicator_eq_indicator_enorm, ENNReal.essSup_indicator_eq_essSup_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
have neg : (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
  (∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
Tactic: simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
have neg : (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
  (∫⁻ (a : α), s.indicator (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) a ∂μ) ^ (1 / p.toReal)
Tactic: rw [← lintegral_indicator hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (a : α), s.indicator (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) a ∂μ) ^ (1 / p.toReal)
have neg : Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ ‖s.indicator f x‖ₑ ^ p.toReal) fun (a : α) ↦
  s.indicator (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) a
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ ‖s.indicator f x‖ₑ ^ p.toReal) fun (a : α) ↦
    s.indicator (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) a
have neg : Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (α := ℝ≥0∞) (s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x) p.toReal)
  fun (a : α) ↦ s.indicator (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) a
Tactic: simp_rw [enorm_indicator_eq_indicator_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (α := ℝ≥0∞) (s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x) p.toReal)
    fun (a : α) ↦ s.indicator (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) a
have neg : HPow.hPow (α := ℝ≥0∞) 0 p.toReal = 0
Tactic: rw [eq_comm, ← Function.comp_def (fun x : ℝ≥0∞ => x ^ p.toReal), Set.indicator_comp_of_zero,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
⊢ eLpNorm (s.indicator f) p μ ≤ eLpNorm f p μ
have refine : ∀ (x : α), ‖s.indicator f x‖ₑ ≤ ‖f x‖ₑ
Tactic: refine eLpNorm_mono_ae' <| .of_forall fun x ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
x : α
⊢ ‖s.indicator f x‖ₑ ≤ ‖f x‖ₑ
have rw : s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x ≤ ‖f x‖ₑ
Tactic: rw [enorm_indicator_eq_indicator_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
⊢ eLpNormEssSup (s.indicator f) μ ≤ eLpNormEssSup f μ
have refine : ∀ (x : α), LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ ‖s.indicator f x‖ₑ) x) ((fun (x : α) ↦ ‖f x‖ₑ) x)
Tactic: refine essSup_mono_ae (Eventually.of_forall fun x => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
x : α
⊢ LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ ‖s.indicator f x‖ₑ) x) ((fun (x : α) ↦ ‖f x‖ₑ) x)
have simp_rw : s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x ≤ ‖f x‖ₑ
Tactic: simp_rw [enorm_indicator_eq_indicator_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
c : ε
⊢ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ ≤ ‖c‖ₑ
have inl : eLpNormEssSup.{u_1, u_7} (ε := ε) (m0 := m0) (s.indicator fun (x : α) ↦ c) 0 ≤ ‖c‖ₑ
Tactic: obtain rfl | hμ0 := eq_or_ne μ 0
Cleared hypotheses: μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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‖ₑ
⊢ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ ≤ ‖c‖ₑ
have inr : ∀ (hμ0 : μ ≠ 0), eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ ≤ ‖c‖ₑ
Tactic: obtain rfl | hμ0 := eq_or_ne μ 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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‖ₑ
have refine : ‖c‖ₑ ≤ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ
Tactic: refine le_antisymm (eLpNormEssSup_indicator_const_le s c) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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∞)
⊢ ‖c‖ₑ ≤ eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ
have by_contra! : ∀ (h : eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ < ‖c‖ₑ), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (hypothesis)
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‖ₑ
⊢ False
have h' : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (hypothesis)
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∞)
⊢ False
have h'₁ : 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'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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
have refine : ∀ (x : α) (hx_mem : x ∈ s),
  Membership.mem (γ := Set α) {a : α | ‖c‖ₑ ≤ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) a)} x
Tactic: refine hμs (measure_mono_null (fun x hx_mem => ?_) h')
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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
⊢ Membership.mem (γ := Set α) {a : α | ‖c‖ₑ ≤ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) a)} x
have rw : ‖c‖ₑ ≤ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) x)
Tactic: rw [Set.mem_setOf_eq, Set.indicator_of_mem hx_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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)
⊢ Membership.mem (γ := Set α) {a : α | ‖c‖ₑ ≤ enorm.{u_7} (E := ε) (s.indicator (fun (x : α) ↦ c) a)} x
have rw₁ : ‖c‖ₑ ≤ ‖c‖ₑ
Tactic: rw [Set.mem_setOf_eq, Set.indicator_of_mem hx_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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
⊢ (∫⁻ (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)
have 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
Tactic: congr 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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
have e_a : Eq (α := ℝ≥0∞) ((fun (x : ε) ↦ ‖x‖ₑ ^ p.toReal) 0) 0
Tactic: refine (Set.comp_indicator_const c (fun x ↦ (‖x‖ₑ) ^ p.toReal) ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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
⊢ (∫⁻ (x : α), s.indicator (fun (x : α) ↦ ‖c‖ₑ ^ p.toReal) x ∂μ) ^ (1 / p.toReal) =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have hz : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have 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)
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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)
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have 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)
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
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)
have 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)
Tactic: obtain rfl | hp := eq_or_ne p 0
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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)
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ ≤
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have 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)
Tactic: obtain rfl | hp := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
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)
have 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 ∞)
Tactic: obtain rfl | h'p := eq_or_ne p ∞
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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 ∞)
⊢ eLpNorm.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) p μ ≤
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have 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)
Tactic: obtain rfl | h'p := eq_or_ne p ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
c : ε
s : Set α
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 ∞)
have inr : eLpNormEssSup.{u_1, u_7} (ε := ε) (s.indicator fun (x : α) ↦ c) μ ≤ ‖c‖ₑ
Tactic: simp only [eLpNorm_exponent_top, ENNReal.toReal_top, _root_.div_zero, ENNReal.rpow_zero,
      mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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
⊢ ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (1 / p.toReal) =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have 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)
Tactic: rw [measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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 μ ≤
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have 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)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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∞)
⊢ MemLp.{u_1, u_4} (ε := E) (s.indicator fun (x : α) ↦ c) p μ
have rw : MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) p (μ.restrict s)
Tactic: rw [memLp_indicator_iff_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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∞)
⊢ MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) p (μ.restrict s)
have inl : MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ 0) p (μ.restrict s)
Tactic: obtain rfl | hμ := hμsc
Cleared hypotheses: c, hμsc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
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)
⊢ MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) p (μ.restrict s)
have inr : ∀ (hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) p (μ.restrict s)
Tactic: obtain rfl | hμ := hμsc
Cleared hypotheses: hμsc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (hypothesis)
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∞)
⊢ MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) p (μ.restrict s)
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have := Fact.mk hμ.lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
⊢ eLpNormEssSup (s.piecewise (β := fun (a : α) ↦ ε) f g) μ =
    max (eLpNormEssSup f (μ.restrict s)) (eLpNormEssSup g (μ.restrict sᶜ))
have simp : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ) μ)
  (essSup (s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) fun (x : α) ↦ ‖g x‖ₑ) μ)
Tactic: simp only [eLpNormEssSup, ← ENNReal.essSup_piecewise hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ) μ)
    (essSup (s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) fun (x : α) ↦ ‖g x‖ₑ) μ)
have e_f : ∀ (x : α),
  ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ =
    s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
x : α
⊢ ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ =
    s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x
have pos : ∀ (hx : x ∈ s),
  ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ =
    s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x
Tactic: by_cases hx : x ∈ s