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 : 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)
h₁ :
  ∀ (f : 𝓢(D, V)),
    ∫ (a : D), Norm.norm.{u_9} (E := V) ((f : (a : D) → V) a : V) ∂μ ≤
      HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ)
        (((Finset.Iic m).sup (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)
⊢ 0 ≤ HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ ∧
    ∀ (f : 𝓢(D, V)),
      Norm.norm.{u_9} (E := V) ((fun (x : 𝓢(D, V)) ↦ (∫ (x_1 : D), (x : (a : D) → V) x_1 ∂μ : V)) f) ≤
        HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ)
          (((Finset.Iic m).sup (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)

Tactic:
refine ⟨by positivity, fun f ↦ (norm_integral_le_integral_norm f).trans ?_⟩
-- 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 : 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)
x : D
⊢ 0 ≤ 1 + ‖x‖

Tactic:
positivity
-- 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 : 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)
x : D
⊢ 0 < HPow.hPow (β := ℝ) (1 + ‖x‖) (↑n : ℝ)

Tactic:
positivity
-- 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 : 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)
x : D
rw :
  (1 + ‖x‖) ^ n * Norm.norm.{u_9} (E := V) ((f : (a : D) → V) x : V) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
      (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)
⊢ 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 : ℝ)

Tactic:
rw [rpow_neg (by positivity), ← div_eq_inv_mul, le_div_iff₀' (by positivity), rpow_natCast]

Premises used: le_div_iff₀', div_eq_inv_mul, Real.rpow_neg, Real.rpow_natCast
-- 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 : 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)
x : D
⊢ (1 + ‖x‖) ^ n * Norm.norm.{u_9} (E := V) ((f : (a : D) → V) x : V) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
      (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ)

Tactic:
simpa using one_add_le_sup_seminorm_apply (m := m) (k := n) (n := 0) le_rfl le_rfl f x

Premises used: le_rfl, SchwartzMap.one_add_le_sup_seminorm_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 : 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)
⊢ ∀ (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 : ℝ)

Tactic:
have h' : ∀ x, ‖f x‖ ≤ (1 + ‖x‖) ^ (-(n : ℝ)) *
      (2 ^ n * ((Finset.Iic m).sup (fun m' => SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)) := by
    intro x
    rw [rpow_neg (by positivity), ← div_eq_inv_mul, le_div_iff₀' (by positivity), rpow_natCast]
    simpa using one_add_le_sup_seminorm_apply (m := m) (k := n) (n := 0) le_rfl le_rfl f x
-- 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 : 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 : ℝ)
⊢ Integrable (ε := ℝ) (fun (i : D) ↦ Norm.norm.{u_9} (E := V) ((f : (a : D) → V) i : V)) μ

Tactic:
simpa using f.integrable_pow_mul μ 0

Premises used: SchwartzMap.integrable_pow_mul, OfNat.ofNat
-- 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 : 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₁ :
  ∫ (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 (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)
apply :
  Integrable (ε := ℝ)
    (fun (i : D) ↦
      HPow.hPow (β := ℝ) (1 + ‖i‖) (-(↑n : ℝ)) *
        HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
          (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ))
    μ
⊢ ∫ (a : D), Norm.norm.{u_9} (E := V) ((f : (a : D) → V) a : V) ∂μ ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ)
      (((Finset.Iic m).sup (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)

Tactic:
apply (integral_mono (by simpa using f.integrable_pow_mul μ 0) _ h').trans

Premises used: MeasureTheory.integral_mono, LE.le.trans
-- 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 : 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₁ :
  ∫ (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 : ℝ)
⊢ ∫ (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 (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)

Tactic:
unfold schwartzSeminormFamily

Premises used: schwartzSeminormFamily
-- 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 : 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 : ℝ)
h₃ 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 : ℝ)
⊢ ∫ (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 : ℝ)

Tactic:
rw [integral_mul_const, ← mul_assoc, mul_comm (2 ^ n)]

Premises used: mul_assoc, HPow.hPow, mul_comm, OfNat.ofNat, MeasureTheory.integral_mul_const
-- 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 : 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 : ℝ)
⊢ Integrable (ε := ℝ)
    (fun (i : D) ↦
      HPow.hPow (β := ℝ) (1 + ‖i‖) (-(↑n : ℝ)) *
        HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n)
          (((Finset.Iic m).sup fun (m' : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2 : (a : 𝓢(D, V)) → ℝ) f : ℝ))
    μ

Tactic:
apply h.mul_const

Premises used: MeasureTheory.Integrable.mul_const
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
D : Type u_4
V : Type u_9
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace ℝ D
inst_3 : NormedAddCommGroup V
inst_4 : NormedSpace ℝ V
inst_5 : NormedSpace 𝕜 V
inst_6 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_7 : BorelSpace D
inst_8 : SecondCountableTopology D
f : 𝓢(D, V)
⊢ Eq.{u_9 + 1} (α := V) ((integralCLM 𝕜 μ : (a : 𝓢(D, V)) → V) f : V) (∫ (x : D), (f : (a : D) → V) x ∂μ : V)

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F) ((f.toBoundedContinuousFunction : (a : E) → F) x : F) ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : 𝓢(E, F)
⊢ LE.le (α := ℝ) (0 : ℝ) ((SchwartzMap.seminorm ℝ 0 0 : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
positivity
-- 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f g : 𝓢(E, F)
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)
⊢ (f + g).toBoundedContinuousFunction = f.toBoundedContinuousFunction + g.toBoundedContinuousFunction

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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f g : 𝓢(E, F)
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:
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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f g : 𝓢(E, F)
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:
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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
a : 𝕜
f : 𝓢(E, F)
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)
⊢ (a • f).toBoundedContinuousFunction =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜) f.toBoundedContinuousFunction

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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
a : 𝕜
f : 𝓢(E, F)
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:
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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
a : 𝕜
f : 𝓢(E, F)
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:
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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
⊢ ∀ (f : 𝓢(E, F)),
    ‖f.toBoundedContinuousFunction‖ ≤
      HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((Finset.sup {0} (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
simpa [BoundedContinuousFunction.norm_le (apply_nonneg _ _)] using norm_le_seminorm 𝕜

Premises used: SchwartzMap.norm_le_seminorm, BoundedContinuousFunction.norm_le, 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F)
    ((((toBoundedContinuousFunctionCLM 𝕜 E F : (a : 𝓢(E, F)) → E →ᵇ F) f : E →ᵇ F) : (a : E) → F) x : F)
    ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)
x : E
⊢ Eq.{u_6 + 1} (α := F) ((f.toZeroAtInfty : (a : E) → F) x : F) ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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.toBCF = f.toBoundedContinuousFunction

Tactic:
rfl

Premises used: ZeroAtInftyContinuousMap.toBCF, BoundedContinuousFunction.ofNormedAddCommGroup, toContinuousMap, SchwartzMap.toBoundedContinuousFunction, rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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‖
rw₁ rw₂ : ‖f.toBoundedContinuousFunction‖ = ‖f.toBoundedContinuousFunction‖
⊢ ‖f.toZeroAtInfty‖ = ‖f.toBoundedContinuousFunction‖

Tactic:
rw [← ZeroAtInftyContinuousMap.norm_toBCF_eq_norm, toZeroAtInfty_toBCF]

Premises used: ZeroAtInftyContinuousMap.norm_toBCF_eq_norm, SchwartzMap.toZeroAtInfty_toBCF