awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)
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)
⊢ (f + g).toZeroAtInfty = f.toZeroAtInfty + g.toZeroAtInfty

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)
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:
add_apply

Premises used: SchwartzMap.add_apply
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)
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:
exact add_apply

Premises used: SchwartzMap.add_apply
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)
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)
⊢ (a • f).toZeroAtInfty = HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) f.toZeroAtInfty

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)
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:
smul_apply

Premises used: SchwartzMap.smul_apply
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)
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:
exact smul_apply

Premises used: SchwartzMap.smul_apply
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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 : 𝓢(E, F)),
    ‖f.toZeroAtInfty‖ ≤
      HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((Finset.sup {0} (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
simpa [← ZeroAtInftyContinuousMap.norm_toBCF_eq_norm,
      BoundedContinuousFunction.norm_le (apply_nonneg _ _)] using norm_le_seminorm 𝕜

Premises used: SchwartzMap.norm_le_seminorm, BoundedContinuousFunction.norm_le, ZeroAtInftyContinuousMap.norm_toBCF_eq_norm, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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 : ProperSpace E
inst_5 : RCLike 𝕜
inst_6 : NormedSpace 𝕜 F
inst_7 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F) ((((toZeroAtInftyCLM 𝕜 E F : (a : 𝓢(E, F)) → E →C₀ F) f : E →C₀ F) : (a : E) → F) x : F)
    ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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
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)
⊢ ∃ (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⟩

Premises used: MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)

Tactic:
⟨k, (eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ).toNNReal * 2 ^ k, fun f ↦ ?_⟩

Premises used: Norm.norm, HMul.hMul, ENNReal.toNNReal, Nat.cast, HPow.hPow, HAdd.hAdd, Exists.intro, OfNat.ofNat, Neg.neg, MeasureTheory.eLpNorm
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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 μ < ∞
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)
⊢ ∃ (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:
refine ⟨k, (eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ).toNNReal * 2 ^ k, fun f ↦ ?_⟩
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)
⊢ ∀ (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.SchwartzSpace.Basic
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 μ

Tactic:
congrArg (eLpNorm · p μ) (funext fun x ↦ ?_)

Premises used: congrArg, funext, MeasureTheory.eLpNorm
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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‖
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
⊢ 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 μ

Tactic:
refine congrArg (eLpNorm · p μ) (funext fun x ↦ ?_)

Premises used: congrArg, funext, MeasureTheory.eLpNorm
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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
⊢ (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:
simp [(h_one_add x).ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)) ∞ μ

Tactic:
eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top p _ ?_

Premises used: MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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‖
refine : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) μ
⊢ 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)) ∞ μ

Tactic:
refine eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top p _ ?_

Premises used: MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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 : ℝ))) μ

Tactic:
Continuous.aestronglyMeasurable ?_

Premises used: Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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‖
refine : Continuous (Y := ℝ) fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) μ

Tactic:
refine Continuous.aestronglyMeasurable ?_

Premises used: Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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‖
⊢ Continuous (Y := ℝ) fun (x : E) ↦ 1 + ‖x‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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‖
⊢ Continuous (Y := ℝ) fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))

Tactic:
exact .rpow_const (by fun_prop) fun x ↦ .inl (h_one_add x).ne'
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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‖
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)
⊢ 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))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)

Tactic:
eLpNormEssSup_le_of_ae_nnnorm_bound (ae_of_all μ fun x ↦ ?_)

Premises used: Filter.limsSup, ENNReal.ofNNReal, WithTop.some, Filter.limsup, MeasureTheory.ae_of_all, MeasureTheory.eLpNormEssSup, essSup, MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound, MeasureTheory.eLpNorm, ite
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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‖
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)
⊢ 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:
refine eLpNormEssSup_le_of_ae_nnnorm_bound (ae_of_all μ fun x ↦ ?_)

Premises used: MeasureTheory.ae_of_all, MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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
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)) :
      ℝ)
⊢ ‖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]

Premises used: Real.toNNReal_le_iff_le_coe, norm_toNNReal
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)) :
      ℝ)

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

Premises used: le_refl, norm_smul, LT.lt.le, abs_of_nonneg, OfNat.ofNat, SchwartzMap.one_add_le_sup_seminorm_apply
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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‖
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)
⊢ 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)

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

Premises used: ENNReal.coe_toNNReal, ENNReal.coe_mul, LT.lt.ne