awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedAddCommGroup V
inst_8 : NormedSpace ℝ V
inst_9 : NormedSpace 𝕜 V
inst_10 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_11 : BorelSpace D
inst_12 : SecondCountableTopology D
n : ℕ
h : Integrable (ε := ℝ) (fun (x : D) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ))) μ
m : ℕ × ℕ := (n, 0)
f : 𝓢(D, V)
h' :
  ∀ (x : D),
    Norm.norm.{u_9} (E := V) ((f : (a : D) → V) x : V) ≤
      HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) *
        HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
          (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
⊢ ∫ (x : D),
      HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) *
        HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
          (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ) ∂μ ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
have h₁ : (∫ (a : D), HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑n : ℝ)) ∂μ) *
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
      (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ) ≤
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ)
    (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
Tactic: rw [integral_mul_const, ← mul_assoc, mul_comm (2 ^ n)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedAddCommGroup V
inst_8 : NormedSpace ℝ V
inst_9 : NormedSpace 𝕜 V
inst_10 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_11 : BorelSpace D
inst_12 : SecondCountableTopology D
n : ℕ
h : Integrable (ε := ℝ) (fun (x : D) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ))) μ
m : ℕ × ℕ := (n, 0)
f : 𝓢(D, V)
h' :
  ∀ (x : D),
    Norm.norm.{u_9} (E := V) ((f : (a : D) → V) x : V) ≤
      HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) *
        HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
          (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
h₁ :
  (∫ (a : D), HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑n : ℝ)) ∂μ) *
      HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
        (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
⊢ ∫ (x : D),
      HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) *
        HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
          (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ) ∂μ ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
have h₂ : HMul.hMul (β := ℝ) ((∫ (a : D), HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑n : ℝ)) ∂μ) * HPow.hPow (α := ℝ) 2 n)
    (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ) ≤
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ)
    (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
Tactic: rw [integral_mul_const, ← mul_assoc, mul_comm (2 ^ n)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedAddCommGroup V
inst_8 : NormedSpace ℝ V
inst_9 : NormedSpace 𝕜 V
inst_10 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_11 : BorelSpace D
inst_12 : SecondCountableTopology D
n : ℕ
h : Integrable (ε := ℝ) (fun (x : D) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ))) μ
m : ℕ × ℕ := (n, 0)
f : 𝓢(D, V)
h' :
  ∀ (x : D),
    Norm.norm.{u_9} (E := V) ((f : (a : D) → V) x : V) ≤
      HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) *
        HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
          (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
h₁ :
  (∫ (a : D), HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑n : ℝ)) ∂μ) *
      HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
        (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
h₂ :
  HMul.hMul (β := ℝ) ((∫ (a : D), HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑n : ℝ)) ∂μ) * HPow.hPow (α := ℝ) 2 n)
      (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
⊢ ∫ (x : D),
      HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) *
        HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
          (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ) ∂μ ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
have h₃ : HMul.hMul (β := ℝ) ((∫ (a : D), HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑n : ℝ)) ∂μ) * HPow.hPow (α := ℝ) 2 n)
    (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ) ≤
  HMul.hMul (β := ℝ) ((∫ (a : D), HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑n : ℝ)) ∂μ) * HPow.hPow (α := ℝ) 2 n)
    (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
Tactic: rw [integral_mul_const, ← mul_assoc, mul_comm (2 ^ n)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f g : 𝓢(E, F)
⊢ (f + g).toBoundedContinuousFunction = f.toBoundedContinuousFunction + g.toBoundedContinuousFunction
have h : ∀ (x : E),
  Eq.{u_6 + 1} (α := F) (((f + g).toBoundedContinuousFunction : (a : E) → F) x : F)
    ((f.toBoundedContinuousFunction + g.toBoundedContinuousFunction : (a : E) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
a : 𝕜
f : 𝓢(E, F)
⊢ (a • f).toBoundedContinuousFunction =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) f.toBoundedContinuousFunction
have h : ∀ (x : E),
  Eq.{u_6 + 1} (α := F) (((a • f).toBoundedContinuousFunction : (a : E) → F) x : F)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) f.toBoundedContinuousFunction : (a : E) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : ProperSpace E
f : 𝓢(E, F)
⊢ ‖f.toZeroAtInfty‖ = ‖f.toBoundedContinuousFunction‖
have rw : ‖f.toZeroAtInfty.toBCF‖ = ‖f.toBoundedContinuousFunction‖
Tactic: rw [← ZeroAtInftyContinuousMap.norm_toBCF_eq_norm, toZeroAtInfty_toBCF]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : ProperSpace E
f : 𝓢(E, F)
rw : ‖f.toZeroAtInfty.toBCF‖ = ‖f.toBoundedContinuousFunction‖
⊢ ‖f.toZeroAtInfty‖ = ‖f.toBoundedContinuousFunction‖
have rw₁ : ‖f.toBoundedContinuousFunction‖ = ‖f.toBoundedContinuousFunction‖
Tactic: rw [← ZeroAtInftyContinuousMap.norm_toBCF_eq_norm, toZeroAtInfty_toBCF]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : ProperSpace E
inst_5 : RCLike 𝕜
inst_6 : NormedSpace 𝕜 F
inst_7 : SMulCommClass ℝ 𝕜 F
f g : 𝓢(E, F)
⊢ (f + g).toZeroAtInfty = f.toZeroAtInfty + g.toZeroAtInfty
have h : ∀ (x : E),
  Eq.{u_6 + 1} (α := F) (((f + g).toZeroAtInfty : (a : E) → F) x : F)
    ((f.toZeroAtInfty + g.toZeroAtInfty : (a : E) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : ProperSpace E
inst_5 : RCLike 𝕜
inst_6 : NormedSpace 𝕜 F
inst_7 : SMulCommClass ℝ 𝕜 F
a : 𝕜
f : 𝓢(E, F)
⊢ (a • f).toZeroAtInfty = HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) f.toZeroAtInfty
have h : ∀ (x : E),
  Eq.{u_6 + 1} (α := F) (((a • f).toZeroAtInfty : (a : E) → F) x : F)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) f.toZeroAtInfty : (a : E) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ ∃ (k : ℕ) (C : ℝ≥0),
    ∀ (f : 𝓢(E, F)),
      eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
        (↑C : ℝ≥0∞) *
          ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
have rcases : ∀ (k : ℕ) (hk : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞),
  ∃ (k : ℕ) (C : ℝ≥0),
    ∀ (f : 𝓢(E, F)),
      eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
        (↑C : ℝ≥0∞) *
          ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
Tactic: rcases hμ.exists_eLpNorm_lt_top p with ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
⊢ ∃ (k : ℕ) (C : ℝ≥0),
    ∀ (f : 𝓢(E, F)),
      eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
        (↑C : ℝ≥0∞) *
          ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
have refine : ∀ (f : 𝓢(E, F)),
  eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
    (↑((eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ).toNNReal *
            HPow.hPow (α := ℝ≥0) 2 k) :
        ℝ≥0∞) *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
Tactic: refine ⟨k, (eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ).toNNReal * 2 ^ k, fun f ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
f : 𝓢(E, F)
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
    (↑((eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ).toNNReal *
            HPow.hPow (α := ℝ≥0) 2 k) :
        ℝ≥0∞) *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
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.SchwartzSpace.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ =
    eLpNorm
      (HSMul.hSMul (α := (x : E) → ℝ) (β := (x : E) → F) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)))
        fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F))
      p μ
have refine : ∀ (x : E),
  (f : (a : E) → F) x =
    HSMul.hSMul (α := (x : E) → ℝ) (β := (x : E) → F) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)))
      (fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F)) x
Tactic: refine congrArg (eLpNorm · p μ) (funext fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm
      (HSMul.hSMul (α := (x : E) → ℝ) (β := (x : E) → F) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)))
        fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F))
      p μ ≤
    eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
      eLpNorm.{u_5, u_6} (ε := F) (fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F)) ∞ μ
have refine : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) μ
Tactic: refine eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top p _ ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) μ
have refine : Continuous (Y := ℝ) fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))
Tactic: refine Continuous.aestronglyMeasurable ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
      eLpNorm.{u_5, u_6} (ε := F) (fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F)) ∞ μ ≤
    eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
      (HPow.hPow (α := ℝ≥0∞) 2 k *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f))
have bc : eLpNorm.{u_5, u_6} (ε := F) (fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F)) ∞ μ ≤
  HPow.hPow (α := ℝ≥0∞) 2 k *
    ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm.{u_5, u_6} (ε := F) (fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F)) ∞ μ ≤
    HPow.hPow (α := ℝ≥0∞) 2 k *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
have bc : ∀ (x : E),
  ‖HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F)‖₊ ≤
    HPow.hPow (α := ℝ≥0) (↑2 : ℝ≥0) k *
      Real.toNNReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
Tactic: refine eLpNormEssSup_le_of_ae_nnnorm_bound (ae_of_all μ fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
x : E
⊢ ‖HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F)‖₊ ≤
    HPow.hPow (α := ℝ≥0) (↑2 : ℝ≥0) k *
      Real.toNNReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
have bc : ‖HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F)‖ ≤
  (↑(HPow.hPow (α := ℝ≥0) (↑2 : ℝ≥0) k *
        Real.toNNReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)) :
    ℝ)
Tactic: rw [← norm_toNNReal, Real.toNNReal_le_iff_le_coe]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
      (HPow.hPow (α := ℝ≥0∞) 2 k *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)) =
    (↑((eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ).toNNReal *
            HPow.hPow (α := ℝ≥0) 2 k) :
        ℝ≥0∞) *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
have rw : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
    (HPow.hPow (α := ℝ≥0∞) 2 k *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)) =
  eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ * (↑(HPow.hPow (α := ℝ≥0) 2 k) : ℝ≥0∞) *
    ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
Tactic: rw [ENNReal.coe_mul, ENNReal.coe_toNNReal hk.ne]