-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem eLpNorm_le_seminorm (p : ℝ≥0∞) (μ : Measure E

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ * eLpNorm (fun x => (1 + ‖x‖) ^ k • f x) ⊤ μ ≤
    eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f))

Tactic:
gcongr

Result:
case bc
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (fun x => (1 + ‖x‖) ^ k • f x) ⊤ μ ≤
    2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm ((fun x => (1 + ‖x‖) ^ (-↑k)) • fun x => (1 + ‖x‖) ^ k • f x) p μ ≤
    eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ * eLpNorm (fun x => (1 + ‖x‖) ^ k • f x) ⊤ μ

Tactic:
refine eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top p _ ?_

Result:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ AEStronglyMeasurable (fun x => (1 + ‖x‖) ^ (-↑k)) μ

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
⊢ ∃ k C,
    ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Tactic:
rcases hμ.exists_eLpNorm_lt_top p with ⟨k, hk⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
⊢ ∃ k C,
    ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) =
    ↑((eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ).toNNReal * 2 ^ k) *
      ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Tactic:
rw [ENNReal.coe_mul, ENNReal.coe_toNNReal hk.ne]

Result:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) =
    eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ * ↑(2 ^ k) *
      ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Proof state:
case bc
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
x : E
⊢ ‖(1 + ‖x‖) ^ k • f x‖ ≤ ↑(↑2 ^ k * (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f).toNNReal)

Tactic:
simpa [norm_smul, abs_of_nonneg (h_one_add x).le] using
  one_add_le_sup_seminorm_apply (m := (k, 0)) (le_refl k) (le_refl 0) f x

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ Continuous fun x => (1 + ‖x‖) ^ (-↑k)

Tactic:
exact .rpow_const (.add continuous_const continuous_norm) fun x ↦ .inl (h_one_add x).ne'

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
hk : eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
x : E
⊢ f x = ((fun x => (1 + ‖x‖) ^ (-↑k)) • fun x => (1 + ‖x‖) ^ k • f x) x

Tactic:
simp [Real.rpow_neg (h_one_add x).le, (h_one_add x).ne']

Result:
no goals