awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * ‖f x‖) μ

Tactic:
AEStronglyMeasurable.mul (aestronglyMeasurable_id.norm.pow _) h''f.norm

Premises used: aestronglyMeasurable_id, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.AEStronglyMeasurable.pow, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * ‖f x‖) μ

Tactic:
exact AEStronglyMeasurable.mul (aestronglyMeasurable_id.norm.pow _) h''f.norm

Premises used: aestronglyMeasurable_id, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.AEStronglyMeasurable.pow, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
h :
  ∀ (v : E),
    ‖‖v‖ ^ k * ‖f v‖‖ ≤
      HPow.hPow (α := ℝ) 2 μ.integrablePower * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + ‖v‖) (-(↑μ.integrablePower : ℝ))
⊢ ∀ᵐ (a : E) ∂μ,
    ‖‖a‖ ^ k * ‖f a‖‖ ≤
      HPow.hPow (α := ℝ) 2 μ.integrablePower * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ))

Tactic:
filter_upwards with v
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
v : E
h :
  ‖v‖ ^ k * ‖f v‖ ≤
    HPow.hPow (α := ℝ) 2 μ.integrablePower * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + ‖v‖) (-(↑μ.integrablePower : ℝ))
⊢ ‖‖v‖ ^ k * ‖f v‖‖ ≤
    HPow.hPow (α := ℝ) 2 μ.integrablePower * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + ‖v‖) (-(↑μ.integrablePower : ℝ))

Tactic:
simp only [norm_mul, norm_pow, norm_norm]

Premises used: norm_pow, norm_mul, norm_norm
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
v : E
⊢ ‖v‖ ^ k * ‖f v‖ ≤
    HPow.hPow (α := ℝ) 2 μ.integrablePower * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + ‖v‖) (-(↑μ.integrablePower : ℝ))

Tactic:
apply pow_mul_le_of_le_of_pow_mul_le (norm_nonneg _) (norm_nonneg _) (hf v) (h'f v)

Premises used: pow_mul_le_of_le_of_pow_mul_le, norm_nonneg
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂
rw :
  LE.le (α := ℝ) (∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ)
    (∫ (a : E),
      HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂) ∂μ)
⊢ ∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ ≤
    (HPow.hPow (α := ℝ) 2 μ.integrablePower * ∫ (x : E), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑μ.integrablePower : ℝ)) ∂μ) *
      (C₁ + C₂)

Tactic:
rw [← integral_const_mul, ← integral_mul_const]

Premises used: MeasureTheory.integral_const_mul, MeasureTheory.integral_mul_const
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂))
    μ
h :
  (ae μ).EventuallyLE (β := ℝ) (fun (a : E) ↦ ‖a‖ ^ k * ‖f a‖) 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₂) ∂μ)

Tactic:
apply integral_mono_of_nonneg

Premises used: MeasureTheory.integral_mono_of_nonneg
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂
v : E
⊢ 0 v ≤ ‖v‖ ^ k * ‖f v‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hf₂ hf₃ : ∀ (v : E), 0 v ≤ ‖v‖ ^ k * ‖f v‖
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : E) ↦ ‖a‖ ^ k * ‖f a‖

Tactic:
filter_upwards with v using by positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂
⊢ Integrable (ε := ℝ)
    (fun (a : E) ↦
      HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂))
    μ

Tactic:
((integrable_pow_neg_integrablePower μ).const_mul _).mul_const _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mul_const, MeasureTheory.Measure.integrable_pow_neg_integrablePower
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂
⊢ Integrable (ε := ℝ)
    (fun (a : E) ↦
      HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂))
    μ

Tactic:
exact ((integrable_pow_neg_integrablePower μ).const_mul _).mul_const _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mul_const, MeasureTheory.Measure.integrable_pow_neg_integrablePower
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂
h :
  ∀ (v : E),
    ‖v‖ ^ k * ‖f v‖ ≤
      HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖v‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂)
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (a : E) ↦ ‖a‖ ^ k * ‖f a‖) fun (a : E) ↦
    HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂)

Tactic:
filter_upwards with v
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂
v : E
⊢ HPow.hPow (α := ℝ) 2 μ.integrablePower * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + ‖v‖) (-(↑μ.integrablePower : ℝ)) =
    HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖v‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂)

Tactic:
ring
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂
v : E
⊢ ‖v‖ ^ k * ‖f v‖ ≤
    HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖v‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂)

Tactic:
exact (pow_mul_le_of_le_of_pow_mul_le (norm_nonneg _) (norm_nonneg _) (hf v) (h'f v)).trans
    (le_of_eq (by ring))

Premises used: pow_mul_le_of_le_of_pow_mul_le, LE.le.trans, le_of_eq, norm_nonneg
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ ∀ᵐ (x : E) ∂μ, ‖HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑0 : ℝ))‖ ≤ 1

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) ∞ μ < ∞

Tactic:
exact ⟨0, eLpNormEssSup_lt_top_of_ae_bound (C := 1) (by simp)⟩
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) = 0
⊢ eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑0 : ℝ))) (↑p : ℝ≥0∞) μ < ∞

Tactic:
simp [hp]
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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∞) μ < ∞

Tactic:
exact ⟨0, by simp [hp]⟩
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
⊢ ∀ (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)
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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‖
⊢ 0 < (↑p : ℝ)

Tactic:
simpa [zero_lt_iff] using hp

Premises used: zero_lt_iff
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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‖
⊢ 0 < (↑p : ℝ)

Tactic:
have hp_pos : 0 < (p : ℝ) := by simpa [zero_lt_iff] using hp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ)
coe :
  ∀ (l : ℕ) (hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ),
    ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
⊢ ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞

Tactic:
rcases hμ.exists_integrable with ⟨l, hl⟩

Premises used: MeasureTheory.Measure.HasTemperateGrowth.exists_integrable
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ)⌉₊
⊢ (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)

Tactic:
simpa [div_le_iff₀ hp_pos] using Nat.le_ceil (l / p : ℝ)

Premises used: div_le_iff₀, HDiv.hDiv, Nat.cast, Nat.le_ceil, NNReal.toReal
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ)⌉₊
⊢ (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)

Tactic:
have hlk : l ≤ k * (p : ℝ) := by simpa [div_le_iff₀ hp_pos] using Nat.le_ceil (l / p : ℝ)
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ)
h : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
⊢ ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞

Tactic:
use k
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ)))) μ
⊢ ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ₑ ∂μ < ∞

Tactic:
rw [hasFiniteIntegral_iff_enorm] at this

Premises used: MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ)))‖ₑ ∂μ < ∞
rw : ∫⁻ (a : E), ‖HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂μ < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp ENNReal.coe_ne_top]

Premises used: MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top, ENNReal.coe_ne_top
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ)))‖ₑ ∂μ < ∞
simp : ∫⁻ (a : E), ‖HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ) ∂μ < ∞
⊢ ∫⁻ (a : E), ‖HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂μ < ∞

Tactic:
simp only [ENNReal.coe_toReal]

Premises used: ENNReal.coe_toReal
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ) ∂μ < ∞

Tactic:
Eq.subst (motive := (∫⁻ x, · x ∂μ < ⊤)) (funext fun x ↦ ?_) this

Premises used: Eq.subst, funext
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ)))‖ₑ ∂μ < ∞
refine : ∀ (x : E), ‖(1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ₑ = ‖HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ)
⊢ ∫⁻ (a : E), ‖HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ) ∂μ < ∞

Tactic:
refine Eq.subst (motive := (∫⁻ x, · x ∂μ < ⊤)) (funext fun x ↦ ?_) this

Premises used: Eq.subst, funext
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
rw : ‖HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)) ^ (↑p : ℝ)‖ₑ = ‖HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ)
⊢ ‖(1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ₑ = ‖HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ)

Tactic:
rw [← neg_mul, Real.rpow_mul (h_one_add x).le]

Premises used: LT.lt.le, neg_mul, Real.rpow_mul
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ 0 ≤ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ ‖HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)) ^ (↑p : ℝ)‖ₑ = ‖HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))‖ₑ ^ (↑p : ℝ)

Tactic:
exact Real.enorm_rpow_of_nonneg (by positivity) NNReal.zero_le_coe

Premises used: Real.enorm_rpow_of_nonneg, NNReal.zero_le_coe
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ)
h : HasFiniteIntegral (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))) μ
⊢ eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞

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
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ)))) μ

Tactic:
hl.hasFiniteIntegral.mono' (ae_of_all μ fun x ↦ ?_)

Premises used: MeasureTheory.HasFiniteIntegral.mono', MeasureTheory.ae_of_all, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ)
h : ∀ (x : E), ‖(1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ ≤ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))) μ

Tactic:
refine hl.hasFiniteIntegral.mono' (ae_of_all μ fun x ↦ ?_)

Premises used: MeasureTheory.HasFiniteIntegral.mono', MeasureTheory.ae_of_all, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
h : (1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ))) ≤ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))
⊢ ‖(1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ)))‖ ≤ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))

Tactic:
rw [Real.norm_of_nonneg (Real.rpow_nonneg (h_one_add x).le _)]

Premises used: LT.lt.le, Real.rpow_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
h : 1 ≤ 1 + ‖x‖
⊢ (1 + ‖x‖) ^ (-((↑k : ℝ) * (↑p : ℝ))) ≤ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))

Tactic:
gcongr