awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ p ≤ c ^ p * ‖g a‖ₑ ^ p
have aux : ∀ (x : α), c ^ p * ‖g x‖ₑ ^ p = (c * ‖g x‖ₑ) ^ p
Tactic: have aux (x) : (↑c) ^ p * ‖g x‖ₑ ^ p = (↑c * ‖g x‖ₑ) ^ p := by
    simp [ENNReal.mul_rpow_eq_ite, hp']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
have pos : ∀ (h0 : p = 0), eLpNorm f p μ ≤ c • eLpNorm g p μ
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
pos : ∀ (h0 : p = 0), eLpNorm f p μ ≤ c • eLpNorm g p μ
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
have neg : ∀ (h0 : ¬p = 0), eLpNorm f p μ ≤ c • eLpNorm g p μ
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
have pos : ∀ (h_top : p = ∞), eLpNorm f p μ ≤ c • eLpNorm g p μ
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
pos : ∀ (h_top : p = ∞), eLpNorm f p μ ≤ c • eLpNorm g p μ
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
have neg : ∀ (h_top : ¬p = ∞), eLpNorm f p μ ≤ c • eLpNorm g p μ
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
have pos : eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ
Tactic: rw [h_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
have neg : eLpNorm' f p.toReal μ ≤ c • eLpNorm' g p.toReal μ
Tactic: simp_rw [eLpNorm_eq_eLpNorm' h0 h_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
have pos : ∀ (h0 : p = 0), eLpNorm f p μ ≤ c • eLpNorm g p μ
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
pos : ∀ (h0 : p = 0), eLpNorm f p μ ≤ c • eLpNorm g p μ
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
have neg : ∀ (h0 : ¬p = 0), eLpNorm f p μ ≤ c • eLpNorm g p μ
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
have pos : ∀ (h_top : p = ∞), eLpNorm f p μ ≤ c • eLpNorm g p μ
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
pos : ∀ (h_top : p = ∞), eLpNorm f p μ ≤ c • eLpNorm g p μ
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
have neg : ∀ (h_top : ¬p = ∞), eLpNorm f p μ ≤ c • eLpNorm g p μ
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
have pos : eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ
Tactic: rw [h_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
have neg : eLpNorm' f p.toReal μ ≤ c • eLpNorm' g p.toReal μ
Tactic: simp_rw [eLpNorm_eq_eLpNorm' h0 h_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_7
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a ≤ b * c ↔ a = 0 ∧ c = 0
have mp : a ≤ b * c → a = 0 ∧ c = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_7
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
mp : a ≤ b * c → a = 0 ∧ c = 0
⊢ a ≤ b * c ↔ a = 0 ∧ c = 0
have mpr : a = 0 ∧ c = 0 → a ≤ b * c
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖
hc : c < 0
p : ℝ≥0∞
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0
have h₁ : (∀ᵐ (x : α) ∂μ, f x = 0) ∧ ∀ᵐ (x : α) ∂μ, g x = 0
Tactic: simp_rw [le_mul_iff_eq_zero_of_nonneg_of_neg_of_nonneg (norm_nonneg _) hc (norm_nonneg _),
    norm_eq_zero, eventually_and] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
hc : c < 0
p : ℝ≥0∞
h : (∀ᵐ (x : α) ∂μ, f x = 0) ∧ ∀ᵐ (x : α) ∂μ, g x = 0
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0
have h₁ : f =ᶠ[ae μ] 0 ∧ g =ᶠ[ae μ] 0
Tactic: change f =ᵐ[μ] 0 ∧ g =ᵐ[μ] 0 at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
⊢ eLpNorm f p μ ≤ c * eLpNorm g p μ
have pos : ∀ (h₀ : p = 0), eLpNorm f p μ ≤ c * eLpNorm g p μ
Tactic: by_cases h₀ : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
pos : ∀ (h₀ : p = 0), eLpNorm f p μ ≤ c * eLpNorm g p μ
⊢ eLpNorm f p μ ≤ c * eLpNorm g p μ
have neg : ∀ (h₀ : ¬p = 0), eLpNorm f p μ ≤ c * eLpNorm g p μ
Tactic: by_cases h₀ : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
⊢ eLpNorm f p μ ≤ c * eLpNorm g p μ
have neg : (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
  if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ
Tactic: simp only [eLpNorm, h₀, ↓reduceIte, mul_ite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ
have pos : ∀ (hp' : p = ∞),
  (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ
Tactic: by_cases hp' : p = ⊤
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
pos :
  ∀ (hp' : p = ∞),
    (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
      if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ
have neg : ∀ (hp' : ¬p = ∞),
  (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ
Tactic: by_cases hp' : p = ⊤
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤ eLpNorm f p μ
have rw : ∫⁻ (a : α), s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) a ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ
Tactic: rw [ENNReal.smul_def, smul_eq_mul, eLpNorm_eq_lintegral_rpow_enorm_toReal hp hp',
    one_div, ENNReal.le_rpow_inv_iff (ENNReal.toReal_pos hp hp'),
    ENNReal.mul_rpow_of_nonneg _ _ ENNReal.toReal_nonneg, ← ENNReal.rpow_mul,
    inv_mul_cancel₀ (ENNReal.toReal_pos hp hp').ne', ENNReal.rpow_one, ← setLIntegral_const,
    ← lintegral_indicator hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ∫⁻ (a : α), s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) a ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ
have refine : ∀ᵐ (a : α) ∂μ, s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) a ≤ ‖f a‖ₑ ^ p.toReal
Tactic: refine lintegral_mono_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ∀ᵐ (a : α) ∂μ, s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) a ≤ ‖f a‖ₑ ^ p.toReal
have h : ∀ (x : α) (hx : x ∈ s → C ≤ ‖f x‖₊), s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal
Tactic: filter_upwards [hf] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
⊢ s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal
have pos : ∀ (hxs : x ∈ s), s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
pos : ∀ (hxs : x ∈ s), s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal
⊢ s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal
have neg : ∀ (hxs : x ∉ s), s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
hxs : x ∈ s
⊢ s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal
have pos : ∀ (hx : C ≤ ‖f x‖₊), (↑C : ℝ≥0∞) ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal
Tactic: simp only [Set.indicator_of_mem, hxs, true_implies] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hxs : x ∈ s
hx : C ≤ ‖f x‖₊
⊢ (↑C : ℝ≥0∞) ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal
have pos : (↑C : ℝ≥0∞) ≤ ‖f x‖ₑ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
have rw : Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ ‖f x‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) p μ
have this : ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
Tactic: have : ∀ x, ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖ := by
    intro x
    rw [one_mul]
    exact RCLike.norm_re_le_norm (f x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) p μ
have refine : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ
Tactic: refine hf.of_le_mul ?_ (Eventually.of_forall this)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
have rw : Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ ‖f x‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) p μ
have this : ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
Tactic: have : ∀ x, ‖RCLike.im (f x)‖ ≤ 1 * ‖f x‖ := by
    intro x
    rw [one_mul]
    exact RCLike.norm_im_le_norm (f x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) p μ
have refine : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ
Tactic: refine hf.of_le_mul ?_ (Eventually.of_forall this)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst_2 : IsFiniteMeasure ν
⊢ MemLp (ε := ε) (fun (x : α × β) ↦ f x.1) p (μ.prod ν)
have hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ)
Tactic: have hf' : MemLp f p (ν .univ • μ) := hf.smul_measure (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst_2 : IsFiniteMeasure ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ)
⊢ MemLp (ε := ε) (fun (x : α × β) ↦ f x.1) p (μ.prod ν)
have change : MemLp (f ∘ Prod.fst) p (μ.prod ν)
Tactic: change MemLp (f ∘ Prod.fst) p (μ.prod ν)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst_2 : IsFiniteMeasure ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ)
⊢ MemLp (f ∘ Prod.fst) p (μ.prod ν)
have rw : MemLp (m0 := mα) f p (Measure.map Prod.fst (μ.prod ν))
Tactic: rw [← memLp_map_measure_iff ?_ (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst_2 : IsFiniteMeasure ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ)
rw : MemLp (m0 := mα) f p (Measure.map Prod.fst (μ.prod ν))
⊢ MemLp (f ∘ Prod.fst) p (μ.prod ν)
have rw₁ : AEStronglyMeasurable (m₀ := mα) f (Measure.map Prod.fst (μ.prod ν))
Tactic: rw [← memLp_map_measure_iff ?_ (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst_2 : IsFiniteMeasure μ
inst_3 : SFinite ν
⊢ MemLp (ε := ε) (fun (x : α × β) ↦ f x.2) p (μ.prod ν)
have hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ν)
Tactic: have hf' : MemLp f p (μ .univ • ν) := hf.smul_measure (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst_2 : IsFiniteMeasure μ
inst_3 : SFinite ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ν)
⊢ MemLp (ε := ε) (fun (x : α × β) ↦ f x.2) p (μ.prod ν)
have change : MemLp (f ∘ Prod.snd) p (μ.prod ν)
Tactic: change MemLp (f ∘ Prod.snd) p (μ.prod ν)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst_2 : IsFiniteMeasure μ
inst_3 : SFinite ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ν)
⊢ MemLp (f ∘ Prod.snd) p (μ.prod ν)
have rw : MemLp (m0 := mβ) f p (Measure.map Prod.snd (μ.prod ν))
Tactic: rw [← memLp_map_measure_iff ?_ (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst_2 : IsFiniteMeasure μ
inst_3 : SFinite ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ν)
rw : MemLp (m0 := mβ) f p (Measure.map Prod.snd (μ.prod ν))
⊢ MemLp (f ∘ Prod.snd) p (μ.prod ν)
have rw₁ : AEStronglyMeasurable (m₀ := mβ) f (Measure.map Prod.snd (μ.prod ν))
Tactic: rw [← memLp_map_measure_iff ?_ (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.SMul (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
⊢ eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ
have inl : eLpNorm' (HSMul.hSMul (α := 𝕜) 0 f) q μ = enorm.{u_3} (E := 𝕜) 0 * eLpNorm' f q μ
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.SMul (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
𝕜 : Type u_3
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 F
inst_3 : NormSMulClass 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
inl : eLpNorm' (HSMul.hSMul (α := 𝕜) 0 f) q μ = enorm.{u_3} (E := 𝕜) 0 * eLpNorm' f q μ
⊢ eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ
have inr : ∀ (hc : c ≠ 0), eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ
Tactic: obtain rfl | hc := eq_or_ne c 0