awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
h0 : Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0
⊢ 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) ↔ (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
have mp : 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) → (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
h0 : Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0
mp : 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) → (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
⊢ 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) ↔ (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
have mpr : (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) → 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
h0 : Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0
h : 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
⊢ (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
have h₁ : ∀ (a : α),
  0 a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a →
    ∀ (h2 : Eq.{u_2 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a)),
      (↑(↑0 : α →ₘ[μ] E) : α → E) a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a
Tactic: filter_upwards [h, h0] with _ _ h2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
h0 : Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0
h : (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
⊢ 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
have h₁ : ∀ (a : α),
  (↑(↑0 : α →ₘ[μ] E) : α → E) a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a →
    ∀ (h2 : Eq.{u_2 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a)), 0 a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a
Tactic: filter_upwards [h, h0] with _ _ h2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
⊢ AddLeftMono ↥(Lp E p μ)
have refine : ∀ (f g₁ g₂ : ↥(Lp E p μ)) (hg₁₂ : g₁ ≤ g₂), f + g₁ ≤ f + g₂
Tactic: refine ⟨fun f g₁ g₂ hg₁₂ => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
f g₁ g₂ : ↥(Lp E p μ)
hg₁₂ : g₁ ≤ g₂
⊢ f + g₁ ≤ f + g₂
have rw : ∀ (hg₁₂ : (↑(↑g₁ : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g₂ : α →ₘ[μ] E) : α → E)),
  (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E)
Tactic: rw [← coeFn_le] at hg₁₂ ⊢
Cleared hypotheses: hg₁₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
f g₁ g₂ : ↥(Lp E p μ)
hg₁₂ : (↑(↑g₁ : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g₂ : α →ₘ[μ] E) : α → E)
⊢ (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E)
have h : ∀ (a : α) (h1 : (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g₁ : α →ₘ[μ] E) : α → E)) a)
  (h2 : (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g₂ : α →ₘ[μ] E) : α → E)) a)
  (h3 : (↑(↑g₁ : α →ₘ[μ] E) : α → E) a ≤ (↑(↑g₂ : α →ₘ[μ] E) : α → E) a),
  (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) a ≤ (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E) a
Tactic: filter_upwards [coeFn_add f g₁, coeFn_add f g₂, hg₁₂] with _ h1 h2 h3
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
f g₁ g₂ : ↥(Lp E p μ)
hg₁₂ : (↑(↑g₁ : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g₂ : α →ₘ[μ] E) : α → E)
a : α
h1 : (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g₁ : α →ₘ[μ] E) : α → E)) a
h2 : (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g₂ : α →ₘ[μ] E) : α → E)) a
h3 : (↑(↑g₁ : α →ₘ[μ] E) : α → E) a ≤ (↑(↑g₂ : α →ₘ[μ] E) : α → E) a
⊢ (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) a ≤ (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E) a
have h : (↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑g₁ : α →ₘ[μ] E) : α → E) a ≤
  (↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑g₂ : α →ₘ[μ] E) : α → E) a
Tactic: rw [h1, h2, Pi.add_apply, Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
inst_3 : Fact (1 ≤ p)
inst_4 : ClosedIciTopology E
f : ℕ → ↥(Lp E p μ)
f₀ : ↥(Lp E p μ)
hf : ∀ (n : ℕ), 0 ≤ f n
h_tendsto : Filter.Tendsto f Filter.atTop (nhds f₀)
⊢ Membership.mem (γ := Set ↥(Lp E p μ)) {x : ↥(Lp E p μ) | 0 ≤ x} f₀
have simp : ∀ (hf : ∀ (n : ℕ), 0 ≤ᶠ[ae μ] (↑(↑(f n) : α →ₘ[μ] E) : α → E)),
  Membership.mem (γ := Set ↥(Lp E p μ)) {x : ↥(Lp E p μ) | 0 ≤ᶠ[ae μ] (↑(↑x : α →ₘ[μ] E) : α → E)} f₀
Tactic: simp only [← coeFn_nonneg] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
inst_3 : Fact (1 ≤ p)
inst_4 : ClosedIciTopology E
f : ℕ → ↥(Lp E p μ)
f₀ : ↥(Lp E p μ)
h_tendsto : Filter.Tendsto f Filter.atTop (nhds f₀)
hf : ∀ (n : ℕ), 0 ≤ᶠ[ae μ] (↑(↑(f n) : α →ₘ[μ] E) : α → E)
⊢ Membership.mem (γ := Set ↥(Lp E p μ)) {x : ↥(Lp E p μ) | 0 ≤ᶠ[ae μ] (↑(↑x : α →ₘ[μ] E) : α → E)} f₀
have obtain : ∀ (φ : ℕ → ℕ)
  (hφ :
    ∀ᵐ (x : α) ∂μ,
      Filter.Tendsto (fun (i : ℕ) ↦ (↑(↑(f (φ i)) : α →ₘ[μ] E) : α → E) x) Filter.atTop
        (nhds ((↑(↑f₀ : α →ₘ[μ] E) : α → E) x))),
  Membership.mem (γ := Set ↥(Lp E p μ)) {x : ↥(Lp E p μ) | 0 ≤ᶠ[ae μ] (↑(↑x : α →ₘ[μ] E) : α → E)} f₀
Tactic: obtain ⟨φ, -, hφ⟩ := tendstoInMeasure_of_tendsto_Lp h_tendsto |>.exists_seq_tendsto_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
inst_3 : Fact (1 ≤ p)
inst_4 : ClosedIciTopology E
f : ℕ → ↥(Lp E p μ)
f₀ : ↥(Lp E p μ)
h_tendsto : Filter.Tendsto f Filter.atTop (nhds f₀)
hf : ∀ (n : ℕ), 0 ≤ᶠ[ae μ] (↑(↑(f n) : α →ₘ[μ] E) : α → E)
φ : ℕ → ℕ
hφ :
  ∀ᵐ (x : α) ∂μ,
    Filter.Tendsto (fun (i : ℕ) ↦ (↑(↑(f (φ i)) : α →ₘ[μ] E) : α → E) x) Filter.atTop
      (nhds ((↑(↑f₀ : α →ₘ[μ] E) : α → E) x))
⊢ Membership.mem (γ := Set ↥(Lp E p μ)) {x : ↥(Lp E p μ) | 0 ≤ᶠ[ae μ] (↑(↑x : α →ₘ[μ] E) : α → E)} f₀
have h : ∀ (x : α) (hx : Membership.mem (γ := Set α) (⋂ (i : ℕ), {x : α | 0 x ≤ (↑(↑(f i) : α →ₘ[μ] E) : α → E) x}) x)
  (hφx :
    Filter.Tendsto (fun (i : ℕ) ↦ (↑(↑(f (φ i)) : α →ₘ[μ] E) : α → E) x) Filter.atTop
      (nhds ((↑(↑f₀ : α →ₘ[μ] E) : α → E) x))),
  0 x ≤ (↑(↑f₀ : α →ₘ[μ] E) : α → E) x
Tactic: filter_upwards [countable_iInter_mem.mpr hf, hφ] with x hx hφx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f g : α →ₘ[μ] E
hf : Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) f
hg : Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) g
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) (f ⊔ g)
have rw : ∀ (hf : MemLp (↑f : α → E) p μ) (hg : MemLp (↑g : α → E) p μ), MemLp (↑(f ⊔ g) : α → E) p μ
Tactic: rw [mem_Lp_iff_memLp] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f g : α →ₘ[μ] E
hf : Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) f
hg : Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) g
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) (f ⊓ g)
have rw : ∀ (hf : MemLp (↑f : α → E) p μ) (hg : MemLp (↑g : α → E) p μ), MemLp (↑(f ⊓ g) : α → E) p μ
Tactic: rw [mem_Lp_iff_memLp] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : |f| ≤ |g|
⊢ ‖f‖ ≤ ‖g‖
have hfg₁ : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
Tactic: rw [← coeFn_le] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
⊢ ‖f‖ ≤ ‖g‖
have simp_rw : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) p μ
Tactic: simp_rw [Lp.norm_def, ENNReal.toReal_le_toReal (Lp.eLpNorm_ne_top f) (Lp.eLpNorm_ne_top g)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
⊢ eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) p μ
have refine : ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖
Tactic: refine eLpNorm_mono_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
⊢ ∀ᵐ (x : α) ∂μ, ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖
have h : ∀ (x : α) (hx : (↑(↑|f| : α →ₘ[μ] E) : α → E) x ≤ (↑(↑|g| : α →ₘ[μ] E) : α → E) x)
  (hxf : (↑(↑|f| : α →ₘ[μ] E) : α → E) x = |(↑(↑f : α →ₘ[μ] E) : α → E) x|)
  (hxg : (↑(↑|g| : α →ₘ[μ] E) : α → E) x = |(↑(↑g : α →ₘ[μ] E) : α → E) x|),
  ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖
Tactic: filter_upwards [hfg, Lp.coeFn_abs f, Lp.coeFn_abs g] with x hx hxf hxg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpOrder (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
x : α
hx : (↑(↑|f| : α →ₘ[μ] E) : α → E) x ≤ (↑(↑|g| : α →ₘ[μ] E) : α → E) x
hxf : (↑(↑|f| : α →ₘ[μ] E) : α → E) x = |(↑(↑f : α →ₘ[μ] E) : α → E) x|
hxg : (↑(↑|g| : α →ₘ[μ] E) : α → E) x = |(↑(↑g : α →ₘ[μ] E) : α → E) x|
⊢ ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖
have hx₁ : |(↑(↑f : α →ₘ[μ] E) : α → E) x| ≤ |(↑(↑g : α →ₘ[μ] E) : α → E) x|
Tactic: rw [hxf, hxg] at hx
Cleared hypotheses: hx, hxf, hxg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
f : α → ε
hq0_lt : 0 < q
hfq : eLpNorm' f q μ < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ < ∞
have rw : eLpNorm' f q μ ^ q < ∞
Tactic: rw [lintegral_rpow_enorm_eq_rpow_eLpNorm' hq0_lt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hfp : eLpNorm f p μ < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞
have hq0_lt : 0 < p.toReal
Tactic: apply lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hfp : eLpNorm f p μ < ∞
hq0_lt : 0 < p.toReal
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞
have hfq : eLpNorm' f p.toReal μ < ∞
Tactic: apply lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞
⊢ eLpNorm f p μ < ∞
have hp' : 0 < p.toReal
Tactic: have hp' := ENNReal.toReal_pos hp_ne_zero hp_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞
hp' : 0 < p.toReal
⊢ eLpNorm f p μ < ∞
have this : 0 < 1 / p.toReal
Tactic: have : 0 < 1 / p.toReal := div_pos zero_lt_one hp'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
⊢ eLpNorm' f 0 μ = 1
have rw : (∫⁻ (a : α), HPow.hPow (β := ℝ) ‖f a‖ₑ 0 ∂μ) ^ (1 / 0) = 1
Tactic: rw [eLpNorm', div_zero, ENNReal.rpow_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
rw : (∫⁻ (a : α), HPow.hPow (β := ℝ) ‖f a‖ₑ 0 ∂μ) ^ (1 / 0) = 1
⊢ eLpNorm' f 0 μ = 1
have rw₁ : HPow.hPow (β := ℝ) (∫⁻ (a : α), HPow.hPow (β := ℝ) ‖f a‖ₑ 0 ∂μ) 0 = 1
Tactic: rw [eLpNorm', div_zero, ENNReal.rpow_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
rw : (∫⁻ (a : α), HPow.hPow (β := ℝ) ‖f a‖ₑ 0 ∂μ) ^ (1 / 0) = 1
rw₁ : HPow.hPow (β := ℝ) (∫⁻ (a : α), HPow.hPow (β := ℝ) ‖f a‖ₑ 0 ∂μ) 0 = 1
⊢ eLpNorm' f 0 μ = 1
have rw₂ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [eLpNorm', div_zero, ENNReal.rpow_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
hq0_ne : q ≠ 0
hμ : μ ≠ 0
⊢ eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
have inl : ∀ (hq0 : 0 ≤ q), eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
Tactic: rcases le_or_gt 0 q with hq0 | hq_neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
hq0_ne : q ≠ 0
hμ : μ ≠ 0
inl : ∀ (hq0 : 0 ≤ q), eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
⊢ eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
have inr : ∀ (hq_neg : q < 0), eLpNorm'.{u_1, u_7} (ε := ε) 0 q μ = 0
Tactic: rcases le_or_gt 0 q with hq0 | hq_neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
⊢ eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
have pos : ∀ (h0 : p = 0), eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
pos : ∀ (h0 : p = 0), eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
⊢ eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
have neg : ∀ (h0 : ¬p = 0), eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
h0 : ¬p = 0
⊢ eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
have pos : ∀ (h_top : p = ∞), eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
h0 : ¬p = 0
pos : ∀ (h_top : p = ∞), eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
⊢ eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
have neg : ∀ (h_top : ¬p = ∞), eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm.{u_1, u_7} (ε := ε) 0 p μ = 0
have h0₁ : p ≠ 0
Tactic: rw [← Ne] at h0
Cleared hypotheses: h0, h_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
⊢ eLpNorm.{u_1, u_7} (ε := ε) 0 p μ < ∞
have rw : LT.lt (α := ℝ≥0∞) 0 ∞
Tactic: rw [eLpNorm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
f : α → ε
⊢ @eLpNorm _ _ _ m0 f p 0 = 0
have pos : ∀ (h0 : p = 0), @eLpNorm _ _ _ m0 f p 0 = 0
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
f : α → ε
pos : ∀ (h0 : p = 0), @eLpNorm _ _ _ m0 f p 0 = 0
⊢ @eLpNorm _ _ _ m0 f p 0 = 0
have neg : ∀ (h0 : ¬p = 0), @eLpNorm _ _ _ m0 f p 0 = 0
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
f : α → ε
h0 : ¬p = 0
⊢ @eLpNorm _ _ _ m0 f p 0 = 0
have pos : ∀ (h_top : p = ∞), @eLpNorm _ _ _ m0 f p 0 = 0
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
f : α → ε
h0 : ¬p = 0
pos : ∀ (h_top : p = ∞), @eLpNorm _ _ _ m0 f p 0 = 0
⊢ @eLpNorm _ _ _ m0 f p 0 = 0
have neg : ∀ (h_top : ¬p = ∞), @eLpNorm _ _ _ m0 f p 0 = 0
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
f : α → ε
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ @eLpNorm _ _ _ m0 f p 0 = 0
have h0₁ : p ≠ 0
Tactic: rw [← Ne] at h0
Cleared hypotheses: h0, h_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (-f) p μ = eLpNorm f p μ
have pos : ∀ (h0 : p = 0), eLpNorm (-f) p μ = eLpNorm f p μ
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
pos : ∀ (h0 : p = 0), eLpNorm (-f) p μ = eLpNorm f p μ
⊢ eLpNorm (-f) p μ = eLpNorm f p μ
have neg : ∀ (h0 : ¬p = 0), eLpNorm (-f) p μ = eLpNorm f p μ
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
⊢ eLpNorm (-f) p μ = eLpNorm f p μ
have pos : ∀ (h_top : p = ∞), eLpNorm (-f) p μ = eLpNorm f p μ
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
pos : ∀ (h_top : p = ∞), eLpNorm (-f) p μ = eLpNorm f p μ
⊢ eLpNorm (-f) p μ = eLpNorm f p μ
have neg : ∀ (h_top : ¬p = ∞), eLpNorm (-f) p μ = eLpNorm f p μ
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
⊢ eLpNorm'.{u_1, u_2} (ε := ε) (fun (x : α) ↦ c) q μ =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
have rw : (‖c‖ₑ ^ q) ^ (1 / q) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q) =
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
Tactic: rw [eLpNorm'_eq_lintegral_enorm, lintegral_const,
    ENNReal.mul_rpow_of_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ 1 / q)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
⊢ (‖c‖ₑ ^ q) ^ (1 / q) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q) =
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / q)
have e_a : (‖c‖ₑ ^ q) ^ (1 / q) = ‖c‖ₑ
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
⊢ (‖c‖ₑ ^ q) ^ (1 / q) = ‖c‖ₑ
have e_a : ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ
Tactic: rw [← ENNReal.rpow_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
hq_cancel : q * (1 / q) = 1
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ
have rw : HPow.hPow (β := ℝ) ‖c‖ₑ 1 = ‖c‖ₑ
Tactic: rw [hq_cancel, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
hq_cancel : q * (1 / q) = 1
rw : HPow.hPow (β := ℝ) ‖c‖ₑ 1 = ‖c‖ₑ
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ
have rw₁ : ‖c‖ₑ = ‖c‖ₑ
Tactic: rw [hq_cancel, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ
have e_a : q * (1 / q) = 1
Tactic: suffices hq_cancel : q * (1 / q) = 1 by rw [hq_cancel, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
⊢ q * (1 / q) = 1
have e_a : q * q⁻¹ = 1
Tactic: rw [one_div, mul_inv_cancel₀ (ne_of_lt hq_pos).symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Basic (goal)
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
c : ε
hq_pos : 0 < q
e_a : q * q⁻¹ = 1
⊢ q * (1 / q) = 1
have e_a₁ : Eq (α := ℝ) 1 1
Tactic: rw [one_div, mul_inv_cancel₀ (ne_of_lt hq_pos).symm]