awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
⊢ eLpNorm f p μ < ∞
have hq0 : q ≠ 0
Tactic: have hq0 : q ≠ 0 := by
    by_contra hq_eq_zero
    obtain rfl : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) zero_le
    rw [ENNReal.toReal_zero] at hp_pos
    exact (lt_irrefl _) hp_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
⊢ eLpNorm f p μ < ∞
have hpq_real : p.toReal ≤ q.toReal
Tactic: have hpq_real : p.toReal ≤ q.toReal := ENNReal.toReal_mono hq_top hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
⊢ eLpNorm f p μ < ∞
have neg : eLpNorm' f p.toReal μ < ∞
Tactic: rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
⊢ eLpNorm' f p.toReal μ < ∞
have hfq_lt_top₁ : eLpNorm' f q.toReal μ < ∞
Tactic: rw [eLpNorm_eq_eLpNorm' hq0 hq_top] at hfq_lt_top
Cleared hypotheses: hfq_lt_top, hp0, hp_top, hp_pos, hq_top, hq0, hpq_real
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
⊢ (toMeasurable μ s).indicator f = f
have apply : Function.support f ⊆ toMeasurable μ s
Tactic: apply Set.indicator_eq_self.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
⊢ Function.support f ⊆ toMeasurable μ s
have apply : ∀ (x : α) (hx : x ∉ toMeasurable μ s), x ∉ s
Tactic: apply Function.support_subset_iff'.2 fun x hx ↦ hf x ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
x : α
hx : x ∉ toMeasurable μ s
⊢ x ∉ s
have contrapose : ∀ (hx : x ∈ s), x ∈ toMeasurable μ s
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
⊢ MemLp f p μ
have this : (toMeasurable μ s).indicator f = f
Tactic: have : (toMeasurable μ s).indicator f = f := by
    apply Set.indicator_eq_self.2
    apply Function.support_subset_iff'.2 fun x hx ↦ hf x ?_
    contrapose hx
    exact subset_toMeasurable μ s hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ MemLp f p μ
have rw : ∀ (hfq : MemLp f q (μ.restrict (toMeasurable μ s))) (hf : ∀ x ∉ s, f x = 0)
  (hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (hpq : p ≤ q)
  (this : (toMeasurable μ s).indicator f = f), MemLp f p (μ.restrict (toMeasurable μ s))
Tactic: rw [← this, memLp_indicator_iff_restrict (measurableSet_toMeasurable μ s)] at hfq ⊢
Cleared hypotheses: hfq, hf, hs, hpq, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ MemLp f p (μ.restrict (toMeasurable μ s))
have this₁ : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have : Fact (μ (toMeasurable μ s) < ∞) := ⟨by simpa [lt_top_iff_ne_top] using hs⟩
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) p μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g p μ
have eLpNorm : eLpNorm (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) p μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g p μ
Tactic: calc
    eLpNorm (fun x => b (f x) (g x)) p μ ≤ eLpNorm (fun x => (c : ℝ) • ‖f x‖ * ‖g x‖) p μ :=
      eLpNorm_mono_ae_real h
    _ ≤ c * eLpNorm f ∞ μ * eLpNorm g p μ := ?_
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) p μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g p μ
have simp : ‖(↑c : ℝ)‖ₑ * eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g p μ
Tactic: simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm_const_smul]
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ ‖(↑c : ℝ)‖ₑ * eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g p μ
have rw : (↑c : ℝ≥0∞) * eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ (↑c : ℝ≥0∞) * (eLpNorm f ∞ μ * eLpNorm g p μ)
Tactic: rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ (↑c : ℝ≥0∞) * eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ (↑c : ℝ≥0∞) * (eLpNorm f ∞ μ * eLpNorm g p μ)
have bc : eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ
Tactic: gcongr
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ
have bc : eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) 0 μ ≤ eLpNorm f ∞ μ * eLpNorm g 0 μ
Tactic: obtain (rfl | rfl | hp) := ENNReal.trichotomy p
Cleared hypotheses: p
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
bc : eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) 0 μ ≤ eLpNorm f ∞ μ * eLpNorm g 0 μ
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ
have bc₁ : eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) ∞ μ ≤ eLpNorm f ∞ μ * eLpNorm g ∞ μ
Tactic: obtain (rfl | rfl | hp) := ENNReal.trichotomy p
Cleared hypotheses: p
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
bc : eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) 0 μ ≤ eLpNorm f ∞ μ * eLpNorm g 0 μ
bc₁ : eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) ∞ μ ≤ eLpNorm f ∞ μ * eLpNorm g ∞ μ
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ
have bc₂ : ∀ (hp : 0 < p.toReal), eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ
Tactic: obtain (rfl | rfl | hp) := ENNReal.trichotomy p
-- 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
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) ∞ μ ≤ eLpNorm f ∞ μ * eLpNorm g ∞ μ
have bc : eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) ∞ μ ≤
  eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖) ∞ μ * eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖g x‖) ∞ μ
Tactic: rw [← eLpNorm_norm f, ← eLpNorm_norm g]
-- 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
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) ∞ μ ≤
    eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖) ∞ μ * eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖g x‖) ∞ μ
have bc : essSup (fun (x : α) ↦ ‖f x‖ₑ * ‖g x‖ₑ) μ ≤
  HMul.hMul (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) (essSup (fun (x : α) ↦ ‖g x‖ₑ) μ)
Tactic: simp_rw [eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm, enorm_mul, enorm_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ
have hp₁ : 0 < p
Tactic: obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ
have hp₂ : p < ∞
Tactic: obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ eLpNorm (ε := ℝ) (fun (i : α) ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ
have bc : ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤
  (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * (∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹) ^ p.toReal
Tactic: simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp₁.ne' hp₂.ne, eLpNorm_exponent_top,
    eLpNormEssSup, one_div, ENNReal.rpow_inv_le_iff hp, enorm_mul, enorm_norm]
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤
    (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * (∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹) ^ p.toReal
have bc : ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤
  ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) p.toReal * ‖g a‖ₑ ^ p.toReal ∂μ
Tactic: rw [ENNReal.mul_rpow_of_nonneg (hz := hp.le), ENNReal.rpow_inv_rpow hp.ne',
    ← lintegral_const_mul'' _ (by fun_prop)]
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) p.toReal * ‖g a‖ₑ ^ p.toReal ∂μ
have bc : ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤ ∫⁻ (a : α), (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * ‖g a‖ₑ) ^ p.toReal ∂μ
Tactic: simp only [← ENNReal.mul_rpow_of_nonneg (hz := hp.le)]
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤ ∫⁻ (a : α), (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * ‖g a‖ₑ) ^ p.toReal ∂μ
have bc : ∀ᵐ (a : α) ∂μ, (‖f a‖ₑ * ‖g a‖ₑ) ^ p.toReal ≤ (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * ‖g a‖ₑ) ^ p.toReal
Tactic: apply lintegral_mono_ae
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ ∀ᵐ (a : α) ∂μ, (‖f a‖ₑ * ‖g a‖ₑ) ^ p.toReal ≤ (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * ‖g a‖ₑ) ^ p.toReal
have h₁ : ∀ (x : α) (hb : ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) (hf : ‖f x‖ₑ ≤ eLpNormEssSup f μ),
  (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ≤ (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * ‖g x‖ₑ) ^ p.toReal
Tactic: filter_upwards [h, enorm_ae_le_eLpNormEssSup f μ] with x hb hf
-- 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 : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
x : α
hb : ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hf : ‖f x‖ₑ ≤ eLpNormEssSup f μ
⊢ (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ≤ (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ * ‖g x‖ₑ) ^ p.toReal
have h₁ : ‖f x‖ₑ ≤ essSup (fun (x : α) ↦ ‖f x‖ₑ) μ
Tactic: gcongr
-- 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 : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ ∀ᵐ (x : α) ∂μ, ‖flip b (g x) (f x)‖₊ ≤ c * ‖g x‖₊ * ‖f x‖₊
have h₁ : ∀ (x : α), c * ‖g x‖₊ * ‖f x‖₊ = c * ‖f x‖₊ * ‖g x‖₊
Tactic: convert! h using 3 with x
-- 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 : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ (↑c : ℝ≥0∞) * eLpNorm g ∞ μ * eLpNorm f p μ = (↑c : ℝ≥0∞) * eLpNorm f p μ * eLpNorm g ∞ μ
have simp : (↑c : ℝ≥0∞) * (eLpNorm g ∞ μ * eLpNorm f p μ) = (↑c : ℝ≥0∞) * (eLpNorm f p μ * eLpNorm g ∞ μ)
Tactic: simp only [mul_assoc]
-- 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 : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ (↑c : ℝ≥0∞) * (eLpNorm g ∞ μ * eLpNorm f p μ) = (↑c : ℝ≥0∞) * (eLpNorm f p μ * eLpNorm g ∞ μ)
have rw : (↑c : ℝ≥0∞) * (eLpNorm f p μ * eLpNorm g ∞ μ) = (↑c : ℝ≥0∞) * (eLpNorm f p μ * eLpNorm g ∞ μ)
Tactic: rw [mul_comm (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 : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ eLpNorm'.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) r μ ≤
    eLpNorm' (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) r μ
have simp : (∫⁻ (a : α), ‖b (f a) (g a)‖ₑ ^ r ∂μ) ^ (1 / r) ≤ (∫⁻ (a : α), ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r ∂μ) ^ (1 / r)
Tactic: simp only [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 : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ (∫⁻ (a : α), ‖b (f a) (g a)‖ₑ ^ r ∂μ) ^ (1 / r) ≤ (∫⁻ (a : α), ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r ∂μ) ^ (1 / r)
have h₁ : ∫⁻ (a : α), ‖b (f a) (g a)‖ₑ ^ r ∂μ ≤ ∫⁻ (a : α), ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r ∂μ
Tactic: gcongr ?_ ^ _
-- 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 : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ ∫⁻ (a : α), ‖b (f a) (g a)‖ₑ ^ r ∂μ ≤ ∫⁻ (a : α), ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r ∂μ
have h₁ : ∀ (a : α) (ha : ‖b (f a) (g a)‖₊ ≤ c * ‖f a‖₊ * ‖g a‖₊), ‖b (f a) (g a)‖ₑ ^ r ≤ ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r
Tactic: refine lintegral_mono_ae <| h.mono fun a ha ↦ ?_
-- 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 : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
a : α
ha : ‖b (f a) (g a)‖₊ ≤ c * ‖f a‖₊ * ‖g a‖₊
⊢ ‖b (f a) (g a)‖ₑ ^ r ≤ ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ ^ r
have h₁ : ‖b (f a) (g a)‖ₑ ≤ ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ
Tactic: gcongr
-- 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 : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
a : α
ha : ‖b (f a) (g a)‖₊ ≤ c * ‖f a‖₊ * ‖g a‖₊
⊢ ‖b (f a) (g a)‖ₑ ≤ ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖ₑ
have h₁ : ‖b (f a) (g a)‖₊ ≤ ‖(↑c : ℝ) • ‖f a‖ * ‖g a‖‖₊
Tactic: simp only [enorm_eq_nnnorm, ENNReal.coe_le_coe]