awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
μ : Measure E
inst_3 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
⊢ LE.le (α := ℝ) (∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ)
    (∫ (a : E),
      HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂) ∂μ)
have hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : E) ↦ ‖a‖ ^ k * ‖f a‖
Tactic: apply integral_mono_of_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
μ : Measure E
inst_3 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : E) ↦ ‖a‖ ^ k * ‖f a‖
⊢ LE.le (α := ℝ) (∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ)
    (∫ (a : E),
      HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂) ∂μ)
have hgi : Integrable (ε := ℝ)
  (fun (a : E) ↦
    HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂))
  μ
Tactic: apply integral_mono_of_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
μ : Measure E
inst_3 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : E) ↦ ‖a‖ ^ k * ‖f a‖
hgi :
  Integrable (ε := ℝ)
    (fun (a : E) ↦
      HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂))
    μ
⊢ LE.le (α := ℝ) (∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ)
    (∫ (a : E),
      HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂) ∂μ)
have h : (ae μ).EventuallyLE (β := ℝ) (fun (a : E) ↦ ‖a‖ ^ k * ‖f a‖) fun (a : E) ↦
  HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂)
Tactic: apply integral_mono_of_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
μ : Measure E
inst_3 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : E) ↦ ‖a‖ ^ k * ‖f a‖
have hf₁ : ∀ (a : E),
  Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ LE.le (α := ℝ) (0 x) ((fun (a : E) ↦ ‖a‖ ^ k * ‖f a‖) x)) x} a
Tactic: filter_upwards with v using by positivity
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
μ : Measure E
inst_3 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
hf₁ :
  ∀ (a : E),
    Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ LE.le (α := ℝ) (0 x) ((fun (a : E) ↦ ‖a‖ ^ k * ‖f a‖) x)) x} a
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : E) ↦ ‖a‖ ^ k * ‖f a‖
have hf₂ : ∀ (a : E), 0 a ≤ ‖a‖ ^ k * ‖f a‖
Tactic: filter_upwards with v using by positivity
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
μ : Measure E
inst_3 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (a : E) ↦ ‖a‖ ^ k * ‖f a‖) fun (a : E) ↦
    HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂)
have h : ∀ (v : E),
  ‖v‖ ^ k * ‖f v‖ ≤
    HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖v‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂)
Tactic: filter_upwards with v
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
⊢ ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
have h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
Tactic: have h_one_add (x : E) : 0 < 1 + ‖x‖ := lt_add_of_pos_of_le zero_lt_one (norm_nonneg x)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
have hp_pos : 0 < (↑p : ℝ)
Tactic: have hp_pos : 0 < (p : ℝ) := by simpa [zero_lt_iff] using hp
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
⊢ ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
have coe : ∀ (l : ℕ) (hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ),
  ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
Tactic: rcases hμ.exists_integrable with ⟨l, hl⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
l : ℕ
hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ
k : ℕ := ⌈(↑l : ℝ) / (↑p : ℝ)⌉₊
⊢ ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
have hlk : (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)
Tactic: have hlk : l ≤ k * (p : ℝ) := by simpa [div_le_iff₀ hp_pos] using Nat.le_ceil (l / p : ℝ)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
l : ℕ
hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ
k : ℕ := ⌈(↑l : ℝ) / (↑p : ℝ)⌉₊
hlk : (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)
⊢ ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
have h : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
Tactic: use k
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
l : ℕ
hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ
k : ℕ := ⌈(↑l : ℝ) / (↑p : ℝ)⌉₊
hlk : (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)
this : HasFiniteIntegral (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))) μ
⊢ eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
have this₁ : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ₑ ∂μ < ∞
Tactic: rw [hasFiniteIntegral_iff_enorm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
l : ℕ
hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ
k : ℕ := ⌈(↑l : ℝ) / (↑p : ℝ)⌉₊
hlk : (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ₑ ∂μ < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
have rw : ∫⁻ (a : E), ‖HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂μ < ∞
Tactic: rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp ENNReal.coe_ne_top]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
l : ℕ
hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ
k : ℕ := ⌈(↑l : ℝ) / (↑p : ℝ)⌉₊
hlk : (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : E), ‖HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂μ < ∞
have simp : ∫⁻ (a : E), ‖HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ) ∂μ < ∞
Tactic: simp only [ENNReal.coe_toReal]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
l : ℕ
hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ
k : ℕ := ⌈(↑l : ℝ) / (↑p : ℝ)⌉₊
hlk : (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : E), ‖HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ) ∂μ < ∞
have refine : ∀ (x : E), ‖(1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ₑ = ‖HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ)
Tactic: refine Eq.subst (motive := (∫⁻ x, · x ∂μ < ⊤)) (funext fun x ↦ ?_) this
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
l : ℕ
hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ
k : ℕ := ⌈(↑l : ℝ) / (↑p : ℝ)⌉₊
hlk : (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ₑ ∂μ < ∞
x : E
⊢ ‖(1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ₑ = ‖HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ)
have rw : ‖HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)) ^ (↑p : ℝ)‖ₑ = ‖HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ)
Tactic: rw [← neg_mul, Real.rpow_mul (h_one_add x).le]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
l : ℕ
hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ
k : ℕ := ⌈(↑l : ℝ) / (↑p : ℝ)⌉₊
hlk : (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)
⊢ eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
have h : HasFiniteIntegral (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))) μ
Tactic: suffices HasFiniteIntegral (fun x ↦ ((1 + ‖x‖) ^ (-(k * p) : ℝ))) μ by
        rw [hasFiniteIntegral_iff_enorm] at this
        rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp ENNReal.coe_ne_top]
        simp only [ENNReal.coe_toReal]
        refine Eq.subst (motive := (∫⁻ x, · x ∂μ < ⊤)) (funext fun x ↦ ?_) this
        rw [← neg_mul, Real.rpow_mul (h_one_add x).le]
        exact Real.enorm_rpow_of_nonneg (by positivity) NNReal.zero_le_coe
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
l : ℕ
hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ
k : ℕ := ⌈(↑l : ℝ) / (↑p : ℝ)⌉₊
hlk : (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))) μ
have h : ∀ (x : E), ‖(1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ ≤ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))
Tactic: refine hl.hasFiniteIntegral.mono' (ae_of_all μ fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
l : ℕ
hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ
k : ℕ := ⌈(↑l : ℝ) / (↑p : ℝ)⌉₊
hlk : (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)
x : E
⊢ ‖(1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ ≤ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))
have h : (1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ))) ≤ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))
Tactic: rw [Real.norm_of_nonneg (Real.rpow_nonneg (h_one_add x).le _)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
l : ℕ
hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ
k : ℕ := ⌈(↑l : ℝ) / (↑p : ℝ)⌉₊
hlk : (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)
x : E
⊢ (1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ))) ≤ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))
have h : 1 ≤ 1 + ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
⊢ ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
have x : (↑p : ℝ≥0∞) = 0 ∨ (↑p : ℝ≥0∞) ≠ 0
Tactic: cases eq_or_ne (p : ℝ≥0∞) 0 with
    | inl hp => exact ⟨0, by simp [hp]⟩
    | inr hp =>
      have h_one_add (x : E) : 0 < 1 + ‖x‖ := lt_add_of_pos_of_le zero_lt_one (norm_nonneg x)
      have hp_pos : 0 < (p : ℝ) := by simpa [zero_lt_iff] using hp
      rcases hμ.exists_integrable with ⟨l, hl⟩
      let k := ⌈(l / p : ℝ)⌉₊
      have hlk : l ≤ k * (p : ℝ) := by simpa [div_le_iff₀ hp_pos] using Nat.le_ceil (l / p : ℝ)
      use k
      suffices HasFiniteIntegral (fun x ↦ ((1 + ‖x‖) ^ (-(k * p) : ℝ))) μ by
        rw [hasFiniteIntegral_iff_enorm] at this
        rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp ENNReal.coe_ne_top]
        simp only [ENNReal.coe_toReal]
        refine Eq.subst (motive := (∫⁻ x, · x ∂μ < ⊤)) (funext fun x ↦ ?_) this
        rw [← neg_mul, Real.rpow_mul (h_one_add x).le]
        exact Real.enorm_rpow_of_nonneg (by positivity) NNReal.zero_le_coe
      refine hl.hasFiniteIntegral.mono' (ae_of_all μ fun x ↦ ?_)
      rw [Real.norm_of_nonneg (Real.rpow_nonneg (h_one_add x).le _)]
      gcongr
      simp
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
have top : ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) ∞ μ < ∞
Tactic: cases p with
  | top => exact ⟨0, eLpNormEssSup_lt_top_of_ae_bound (C := 1) (by simp)⟩
  | coe p =>
    cases eq_or_ne (p : ℝ≥0∞) 0 with
    | inl hp => exact ⟨0, by simp [hp]⟩
    | inr hp =>
      have h_one_add (x : E) : 0 < 1 + ‖x‖ := lt_add_of_pos_of_le zero_lt_one (norm_nonneg x)
      have hp_pos : 0 < (p : ℝ) := by simpa [zero_lt_iff] using hp
      rcases hμ.exists_integrable with ⟨l, hl⟩
      let k := ⌈(l / p : ℝ)⌉₊
      have hlk : l ≤ k * (p : ℝ) := by simpa [div_le_iff₀ hp_pos] using Nat.le_ceil (l / p : ℝ)
      use k
      suffices HasFiniteIntegral (fun x ↦ ((1 + ‖x‖) ^ (-(k * p) : ℝ))) μ by
        rw [hasFiniteIntegral_iff_enorm] at this
        rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp ENNReal.coe_ne_top]
        simp only [ENNReal.coe_toReal]
        refine Eq.subst (motive := (∫⁻ x, · x ∂μ < ⊤)) (funext fun x ↦ ?_) this
        rw [← neg_mul, Real.rpow_mul (h_one_add x).le]
        exact Real.enorm_rpow_of_nonneg (by positivity) NNReal.zero_le_coe
      refine hl.hasFiniteIntegral.mono' (ae_of_all μ fun x ↦ ?_)
      rw [Real.norm_of_nonneg (Real.rpow_nonneg (h_one_add x).le _)]
      gcongr
      simp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
top : ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) ∞ μ < ∞
⊢ ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
have coe : ∀ (p : ℝ≥0), ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
Tactic: cases p with
  | top => exact ⟨0, eLpNormEssSup_lt_top_of_ae_bound (C := 1) (by simp)⟩
  | coe p =>
    cases eq_or_ne (p : ℝ≥0∞) 0 with
    | inl hp => exact ⟨0, by simp [hp]⟩
    | inr hp =>
      have h_one_add (x : E) : 0 < 1 + ‖x‖ := lt_add_of_pos_of_le zero_lt_one (norm_nonneg x)
      have hp_pos : 0 < (p : ℝ) := by simpa [zero_lt_iff] using hp
      rcases hμ.exists_integrable with ⟨l, hl⟩
      let k := ⌈(l / p : ℝ)⌉₊
      have hlk : l ≤ k * (p : ℝ) := by simpa [div_le_iff₀ hp_pos] using Nat.le_ceil (l / p : ℝ)
      use k
      suffices HasFiniteIntegral (fun x ↦ ((1 + ‖x‖) ^ (-(k * p) : ℝ))) μ by
        rw [hasFiniteIntegral_iff_enorm] at this
        rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp ENNReal.coe_ne_top]
        simp only [ENNReal.coe_toReal]
        refine Eq.subst (motive := (∫⁻ x, · x ∂μ < ⊤)) (funext fun x ↦ ?_) this
        rw [← neg_mul, Real.rpow_mul (h_one_add x).le]
        exact Real.enorm_rpow_of_nonneg (by positivity) NNReal.zero_le_coe
      refine hl.hasFiniteIntegral.mono' (ae_of_all μ fun x ↦ ?_)
      rw [Real.norm_of_nonneg (Real.rpow_nonneg (h_one_add x).le _)]
      gcongr
      simp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
g : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((toTemperedDistribution f : (a : 𝓢(E, ℂ)) → F) g : F)
    (∫ (x : E), HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x) ∂μ : F)
have simp : Eq.{u_4 + 1} (α := F) (∫ (x : E), (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ)
  (∫ (x : E), HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x) ∂μ)
Tactic: simp only [toTemperedDistribution, toPointwiseConvergenceCLM_apply, comp_apply _, toLpCLM_apply,
    lpPairing_eq_integral, lsmul_flip_apply, toSpanSingleton_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
g : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    (∫ (x : E), (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ)
    (∫ (x : E), HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x) ∂μ)
have h : Filter.EventuallyEq.{u_3, u_4} (β := F) (ae μ)
  (fun (a : E) ↦ (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) a • (↑(↑f : E →ₘ[μ] F) : E → F) a) fun (a : E) ↦
  HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) a : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) a)
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
g : 𝓢(E, ℂ)
⊢ Filter.EventuallyEq.{u_3, u_4} (β := F) (ae μ)
    (fun (a : E) ↦ (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) a • (↑(↑f : E →ₘ[μ] F) : E → F) a) fun (a : E) ↦
    HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) a : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) a)
have h : ∀ (x : E) (hg : (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) x = (g : (a : E) → ℂ) x),
  (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) x • (↑(↑f : E →ₘ[μ] F) : E → F) x =
    HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x)
Tactic: filter_upwards [g.coeFn_toLp (1 - p⁻¹)⁻¹ μ] with x hg
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
g : 𝓢(E, ℂ)
x : E
hg : (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) x = (g : (a : E) → ℂ) x
⊢ (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) x • (↑(↑f : E →ₘ[μ] F) : E → F) x =
    HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x)
have h : HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x) =
  HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x)
Tactic: rw [hg]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ Eq (α := 𝓢'(E, F)) (toTemperedDistribution (f.toLp p μ))
    ((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) f)
have h : ∀ (g : 𝓢(E, ℂ)),
  Eq.{u_4 + 1} (α := F) ((toTemperedDistribution (f.toLp p μ) : (a : 𝓢(E, ℂ)) → F) g : F)
    ((((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) g : F)
Tactic: ext g
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperedDistribution (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((toTemperedDistribution (f.toLp p μ) : (a : 𝓢(E, ℂ)) → F) g : F)
    ((((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) g : F)
have h : Eq.{u_4 + 1} (α := F)
  (∫ (x : E), HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) x) ∂μ)
  (∫ (x : E), HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F) ∂μ)
Tactic: simp only [Lp.toTemperedDistribution_apply, toTemperedDistributionCLM_apply_apply]