awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
hr₁ : 0 < r
hr₂ : r < ∞
hrp : r.toReal < p.toReal
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inr : eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r.toReal μ ≤
  (↑c : ℝ≥0∞) * eLpNorm' f p.toReal μ * eLpNorm' g q.toReal μ
Tactic: rw [eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
hr₁ : 0 < r
hr₂ : r < ∞
hrp : r.toReal < p.toReal
inr :
  eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r.toReal μ ≤
    (↑c : ℝ≥0∞) * eLpNorm' f p.toReal μ * eLpNorm' g q.toReal μ
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inr₁ : q ≠ 0
Tactic: rw [eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
hr₁ : 0 < r
hr₂ : r < ∞
hrp : r.toReal < p.toReal
inr :
  eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r.toReal μ ≤
    (↑c : ℝ≥0∞) * eLpNorm' f p.toReal μ * eLpNorm' g q.toReal μ
inr₁ : q ≠ 0
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inr₂ : q ≠ ∞
Tactic: rw [eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
hr₁ : 0 < r
hr₂ : r < ∞
hrp : r.toReal < p.toReal
inr :
  eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r.toReal μ ≤
    (↑c : ℝ≥0∞) * eLpNorm' f p.toReal μ * eLpNorm' g q.toReal μ
inr₁ : q ≠ 0
inr₂ : q ≠ ∞
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inr₃ : p ≠ 0
Tactic: rw [eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
hr₁ : 0 < r
hr₂ : r < ∞
hrp : r.toReal < p.toReal
inr :
  eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r.toReal μ ≤
    (↑c : ℝ≥0∞) * eLpNorm' f p.toReal μ * eLpNorm' g q.toReal μ
inr₁ : q ≠ 0
inr₂ : q ≠ ∞
inr₃ : p ≠ 0
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inr₄ : p ≠ ∞
Tactic: rw [eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
hr₁ : 0 < r
hr₂ : r < ∞
hrp : r.toReal < p.toReal
inr :
  eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r.toReal μ ≤
    (↑c : ℝ≥0∞) * eLpNorm' f p.toReal μ * eLpNorm' g q.toReal μ
inr₁ : q ≠ 0
inr₂ : q ≠ ∞
inr₃ : p ≠ 0
inr₄ : p ≠ ∞
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inr₅ : r ≠ 0
Tactic: rw [eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr_1 : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
hr : 0 < r.toReal
hr₁ : 0 < r
hr₂ : r < ∞
hrp : r.toReal < p.toReal
inr :
  eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r.toReal μ ≤
    (↑c : ℝ≥0∞) * eLpNorm' f p.toReal μ * eLpNorm' g q.toReal μ
inr₁ : q ≠ 0
inr₂ : q ≠ ∞
inr₃ : p ≠ 0
inr₄ : p ≠ ∞
inr₅ : r ≠ 0
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤ (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ
have inr₆ : r ≠ ∞
Tactic: rw [eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p q r : ℝ≥0∞
f : α → E
g : α → F
b : E → F → G
c : ℝ≥0
hf : MemLp f p μ
hg : MemLp g q μ
h : AEStronglyMeasurable.{u_1, u_4} (β := G) (fun (x : α) ↦ b (f x) (g x)) μ
hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr : p.HolderTriple q r
⊢ MemLp.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ
have refine : eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ < ∞
Tactic: refine ⟨h, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p q r : ℝ≥0∞
f : α → E
g : α → F
b : E → F → G
c : ℝ≥0
hf : MemLp f p μ
hg : MemLp g q μ
h : AEStronglyMeasurable.{u_1, u_4} (β := G) (fun (x : α) ↦ b (f x) (g x)) μ
hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr : p.HolderTriple q r
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ < ∞
have apply : (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g q μ < ∞
Tactic: apply (eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm hf.1 hg.1 b c hb (hpqr := hpqr)).trans_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) (p i) μ
⊢ MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ
have pos : ∀ (hμ : μ = 0), MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) (p i) μ
pos : ∀ (hμ : μ = 0), MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ
⊢ MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ
have neg : ∀ (hμ : ¬μ = 0), MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, MemLp (f i) (p i) μ), MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
hf : ∀ i_1 ∈ cons i s hi, MemLp (f i_1) (p i_1) μ
⊢ MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ cons i s hi, f i) (∑ i ∈ cons i s hi, (p i)⁻¹)⁻¹ μ
have cons : MemLp (f i * ∏ x ∈ s, f x) (∑ i ∈ cons i s hi, (p i)⁻¹)⁻¹ μ
Tactic: rw [prod_cons]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ s, MemLp (f i) (p i) μ
⊢ MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) (p i) μ),
  MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ
Tactic: induction s using cons_induction with
  | empty =>
    by_cases hμ : μ = 0 <;>
      simp [MemLp, eLpNormEssSup_const, hμ, aestronglyMeasurable_const, Pi.one_def]
  | cons i s hi ih =>
    rw [prod_cons]
    exact (ih <| forall_of_forall_cons hf).mul (hf i <| mem_cons_self ..) (hpqr := ⟨by simp⟩)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ s, MemLp (f i) (p i) μ
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) (p i) μ),
    MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ
⊢ MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
have cons : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (ih : ∀ (hf : ∀ i ∈ s, MemLp (f i) (p i) μ), MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ)
  (hf : ∀ i_1 ∈ cons i s hi, MemLp (f i_1) (p i_1) μ),
  MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ cons i s hi, f i) (∑ i ∈ cons i s hi, (p i)⁻¹)⁻¹ μ
Tactic: induction s using cons_induction with
  | empty =>
    by_cases hμ : μ = 0 <;>
      simp [MemLp, eLpNormEssSup_const, hμ, aestronglyMeasurable_const, Pi.one_def]
  | cons i s hi ih =>
    rw [prod_cons]
    exact (ih <| forall_of_forall_cons hf).mul (hf i <| mem_cons_self ..) (hpqr := ⟨by simp⟩)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Count (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ @eLpNorm _ _ _ inst f p (dirac i) = ‖f i‖ₑ
have simp_rw : (if p = ∞ then eLpNormEssSup (m0 := inst) f (dirac i) else @eLpNorm' _ _ _ inst f p.toReal (dirac i)) = ‖f i‖ₑ
Tactic: simp_rw [eLpNorm, if_neg hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Count (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ (if p = ∞ then eLpNormEssSup (m0 := inst) f (dirac i) else @eLpNorm' _ _ _ inst f p.toReal (dirac i)) = ‖f i‖ₑ
have pos : p = ∞ → eLpNormEssSup (m0 := inst) f (dirac i) = ‖f i‖ₑ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Count (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
pos : p = ∞ → eLpNormEssSup (m0 := inst) f (dirac i) = ‖f i‖ₑ
⊢ (if p = ∞ then eLpNormEssSup (m0 := inst) f (dirac i) else @eLpNorm' _ _ _ inst f p.toReal (dirac i)) = ‖f i‖ₑ
have neg : ¬p = ∞ → @eLpNorm' _ _ _ inst f p.toReal (dirac i) = ‖f i‖ₑ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Count (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ ‖f i‖ₑ = @eLpNorm _ _ _ inst f p (dirac i)
have rw : ‖f i‖ₑ = ‖f i‖ₑ
Tactic: rw [eLpNorm_dirac f i hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Count (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ ‖f i‖ₑ ≤ @eLpNorm _ _ _ inst f p count
have eLpNorm : ‖f i‖ₑ = @eLpNorm _ _ _ inst f p (dirac i)
Tactic: calc
    ‖f i‖ₑ = eLpNorm f p (dirac i) := by rw [eLpNorm_dirac f i hp]
      _ = eLpNorm f p (count.restrict {i}) := by simp
      _ ≤ eLpNorm f p count := eLpNorm_restrict_le ..
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Count (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
eLpNorm : ‖f i‖ₑ = @MeasureTheory.eLpNorm _ _ _ inst f p (dirac i)
⊢ ‖f i‖ₑ ≤ @MeasureTheory.eLpNorm _ _ _ inst f p count
have eLpNorm₁ : @MeasureTheory.eLpNorm _ _ _ inst f p (dirac i) = @MeasureTheory.eLpNorm _ _ _ inst f p (Measure.restrict count {i})
Tactic: calc
    ‖f i‖ₑ = eLpNorm f p (dirac i) := by rw [eLpNorm_dirac f i hp]
      _ = eLpNorm f p (count.restrict {i}) := by simp
      _ ≤ eLpNorm f p count := eLpNorm_restrict_le ..
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Count (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst_3 : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
⊢ @eLpNorm _ _ _ inst f p count < ∞
have haveI : ∀ (this : Fintype α), @eLpNorm _ _ _ inst f p count < ∞
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Count (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst_3 : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
⊢ @eLpNorm _ _ _ inst f p count < ∞
have refine_1 : ∀ (x : α), ‖f x‖ₑ ≤ enorm (E := ℝ≥0∞) ((fun (x : α) ↦ (Finset.sup Finset.univ fun (x : α) ↦ ‖f x‖ₑ : ℝ≥0∞)) x)
Tactic: refine (eLpNorm_mono_enorm (g := fun _ ↦ Finset.univ.sup (‖f ·‖ₑ)) ?_).trans_lt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Count (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst_3 : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
refine_1 :
  ∀ (x : α), ‖f x‖ₑ ≤ enorm (E := ℝ≥0∞) ((fun (x : α) ↦ (Finset.sup Finset.univ fun (x : α) ↦ ‖f x‖ₑ : ℝ≥0∞)) x)
⊢ @eLpNorm _ _ _ inst f p count < ∞
have refine_2 : @eLpNorm _ ℝ≥0∞ _ inst (fun (x : α) ↦ Finset.sup Finset.univ fun (x : α) ↦ ‖f x‖ₑ) p count < ∞
Tactic: refine (eLpNorm_mono_enorm (g := fun _ ↦ Finset.univ.sup (‖f ·‖ₑ)) ?_).trans_lt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Defs (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
⊢ eLpNorm f p μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
have rw : eLpNorm' f p.toReal μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
Tactic: rw [eLpNorm_eq_eLpNorm' hp_ne_zero hp_ne_top, eLpNorm'_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Defs (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
rw : eLpNorm' f p.toReal μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
⊢ eLpNorm f p μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
have rw₁ : (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
Tactic: rw [eLpNorm_eq_eLpNorm' hp_ne_zero hp_ne_top, eLpNorm'_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Defs (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
μ : Measure α
f : α → ε
⊢ eLpNorm f 1 μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
have simp_rw : (∫⁻ (x : α), ‖f x‖ₑ ^ ENNReal.toReal 1 ∂μ) ^ (1 / ENNReal.toReal 1) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
Tactic: simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal one_ne_zero ENNReal.coe_ne_top,
    ENNReal.toReal_one, one_div_one, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Defs (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
μ : Measure α
f : α → ε
simp_rw : (∫⁻ (x : α), ‖f x‖ₑ ^ ENNReal.toReal 1 ∂μ) ^ (1 / ENNReal.toReal 1) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
⊢ eLpNorm f 1 μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
have simp_rw₁ : (∫⁻ (x : α), HPow.hPow (β := ℝ) ‖f x‖ₑ 1 ∂μ) ^ (1 / 1) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
Tactic: simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal one_ne_zero ENNReal.coe_ne_top,
    ENNReal.toReal_one, one_div_one, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Defs (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
μ : Measure α
f : α → ε
simp_rw : (∫⁻ (x : α), ‖f x‖ₑ ^ ENNReal.toReal 1 ∂μ) ^ (1 / ENNReal.toReal 1) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
simp_rw₁ : (∫⁻ (x : α), HPow.hPow (β := ℝ) ‖f x‖ₑ 1 ∂μ) ^ (1 / 1) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
⊢ eLpNorm f 1 μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
have simp_rw₂ : HPow.hPow (β := ℝ) (∫⁻ (x : α), HPow.hPow (β := ℝ) ‖f x‖ₑ 1 ∂μ) 1 = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
Tactic: simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal one_ne_zero ENNReal.coe_ne_top,
    ENNReal.toReal_one, one_div_one, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Defs (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = eLpNorm' f q μ ^ q
have rw : q ≠ 0
Tactic: rw [eLpNorm'_eq_lintegral_enorm, ← ENNReal.rpow_mul, one_div, inv_mul_cancel₀, 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 ε
f : α → ε
s : Set α
hs : MeasurableSet s
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
have pos : ∀ (hp_zero : p = 0), eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
Tactic: by_cases hp_zero : p = 0
-- 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
pos : ∀ (hp_zero : p = 0), eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
have neg : ∀ (hp_zero : ¬p = 0), eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
Tactic: by_cases hp_zero : p = 0
-- 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
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
have pos : ∀ (hp_top : p = ∞), eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
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 ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
pos : ∀ (hp_top : p = ∞), eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
have neg : ∀ (hp_top : ¬p = ∞), eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
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 ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : p = ∞
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
have pos : eLpNorm (s.indicator f) ∞ μ = eLpNorm f ∞ (μ.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 = ∞
pos : eLpNorm (s.indicator f) ∞ μ = eLpNorm f ∞ (μ.restrict s)
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
have pos₁ : eLpNormEssSup (s.indicator f) μ = eLpNormEssSup f (μ.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 = ∞
pos : eLpNorm (s.indicator f) ∞ μ = eLpNorm f ∞ (μ.restrict s)
pos₁ : eLpNormEssSup (s.indicator f) μ = eLpNormEssSup f (μ.restrict s)
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
have pos₂ : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖s.indicator f x‖ₑ) μ) (essSup (fun (x : α) ↦ ‖f x‖ₑ) (μ.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]