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 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
_ :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
          x) =
    ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
          (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
_₁ :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
          (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    ‖x‖ ^ k *
      (‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
          x) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have _₂ : ‖x‖ ^ k *
    (‖L‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) =
  ‖L‖ *
    (‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
Tactic: calc
    _ = ‖x‖ ^ k * ‖(L.restrictScalars ℝ).compContinuousMultilinearMap
        (iteratedFDeriv ℝ n f x)‖ := by
      congr
      exact (L.restrictScalars ℝ).iteratedFDeriv_comp_left f.smooth'.contDiffAt (mod_cast le_top)
    _ ≤ ‖x‖ ^ k * (‖L‖ * ‖iteratedFDeriv ℝ n f x‖) := by
      gcongr
      apply (L.restrictScalars ℝ).norm_compContinuousMultilinearMap_le
    _ = ‖L‖ * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖) := by ring
    _ ≤ ‖L‖ * (SchwartzMap.seminorm 𝕜 k n) f := by
      grw [le_seminorm 𝕜 k n f x]
-- 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 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
_ :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
          x) =
    ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
          (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
_₁ :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
          (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    ‖x‖ ^ k *
      (‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
_₂ :
  ‖x‖ ^ k *
      (‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) =
    ‖L‖ *
      (‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
          x) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have _₃ : ‖L‖ *
    (‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
  HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: calc
    _ = ‖x‖ ^ k * ‖(L.restrictScalars ℝ).compContinuousMultilinearMap
        (iteratedFDeriv ℝ n f x)‖ := by
      congr
      exact (L.restrictScalars ℝ).iteratedFDeriv_comp_left f.smooth'.contDiffAt (mod_cast le_top)
    _ ≤ ‖x‖ ^ k * (‖L‖ * ‖iteratedFDeriv ℝ n f x‖) := by
      gcongr
      apply (L.restrictScalars ℝ).norm_compContinuousMultilinearMap_le
    _ = ‖L‖ * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖) := by ring
    _ ≤ ‖L‖ * (SchwartzMap.seminorm 𝕜 k n) f := by
      grw [le_seminorm 𝕜 k n f 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (compSubConstCLM 𝕜 0) (ContinuousLinearMap.id 𝕜 𝓢(E, F))
have h : ∀ (f : 𝓢(E, F)) (x : E),
  Eq.{u_6 + 1} (α := F) ((((compSubConstCLM 𝕜 0 : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
    ((((ContinuousLinearMap.id 𝕜 𝓢(E, F) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
Tactic: ext f 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
f : 𝓢(E, F)
a b : E
⊢ Eq (α := 𝓢(E, F))
    ((compSubConstCLM 𝕜 b : (a : 𝓢(E, F)) → 𝓢(E, F)) ((compSubConstCLM 𝕜 a : (a : 𝓢(E, F)) → 𝓢(E, F)) f) : 𝓢(E, F))
    ((compSubConstCLM 𝕜 (a + b) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))
have h : ∀ (x : E),
  Eq.{u_6 + 1} (α := F)
    ((((compSubConstCLM 𝕜 b : (a : 𝓢(E, F)) → 𝓢(E, F)) ((compSubConstCLM 𝕜 a : (a : 𝓢(E, F)) → 𝓢(E, F)) f) : 𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    ((((compSubConstCLM 𝕜 (a + b) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
Tactic: ext 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
f : 𝓢(E, F)
a b x : E
⊢ Eq.{u_6 + 1} (α := F)
    ((((compSubConstCLM 𝕜 b : (a : 𝓢(E, F)) → 𝓢(E, F)) ((compSubConstCLM 𝕜 a : (a : 𝓢(E, F)) → 𝓢(E, F)) f) : 𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    ((((compSubConstCLM 𝕜 (a + b) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
have h : Eq.{u_6 + 1} (α := F) ((f : (a : E) → F) (x - b - a) : F) ((f : (a : E) → F) (x - (a + b)) : F)
Tactic: simp only [compSubConstCLM_apply]
-- 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
f : 𝓢(E, F)
a b x : E
⊢ Eq.{u_6 + 1} (α := F) ((f : (a : E) → F) (x - b - a) : F) ((f : (a : E) → F) (x - (a + b)) : F)
have h : x - b - a = x - (a + b)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
D : Type u_4
V : Type u_9
inst : NormedAddCommGroup D
inst_1 : NormedSpace ℝ D
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_5 : BorelSpace D
inst_6 : SecondCountableTopology D
f : 𝓢(D, V)
k : ℕ
⊢ Integrable (ε := ℝ) (fun (x : D) ↦ ‖x‖ ^ k * Norm.norm.{u_9} (E := V) ((f : (a : D) → V) x : V)) μ
have h : ∀ (x : D),
  Norm.norm.{u_9} (E := V) ((f : (a : D) → V) x : V) =
    Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_9} ℝ (fun (i : Fin 0) ↦ D) V)
      (iteratedFDeriv ℝ 0 (⇑f : (a : D) → V) x)
Tactic: convert! integrable_pow_mul_iteratedFDeriv μ f k 0 with x
-- 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
⊢ 𝓢(D, V) →L[𝕜] V
have refine : ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
  0 ≤ C ∧
    ∀ (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 (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)
Tactic: refine mkCLMtoNormedSpace (∫ x, · x ∂μ)
    (fun f g ↦ integral_add f.integrable g.integrable) (integral_smul · ·) ?_
-- 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
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (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 (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)
have rcases : ∀ (n : ℕ) (h : Integrable (ε := ℝ) (fun (x : D) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ))) μ),
  ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (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 (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)
Tactic: rcases hμ.exists_integrable with ⟨n, h⟩
-- 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)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (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 (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)
have h₁ : 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: use Finset.Iic m, 2 ^ n * ∫ x : D, (1 + ‖x‖) ^ (- (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)
⊢ 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 : ℝ)
have 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 : ℝ)
Tactic: refine ⟨by positivity, fun f ↦ (norm_integral_le_integral_norm f).trans ?_⟩
-- 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)
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 : ℝ)
have 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 : ℝ)
Tactic: rw [rpow_neg (by positivity), ← div_eq_inv_mul, le_div_iff₀' (by positivity), rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
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)
⊢ ∫ (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 : ℝ)
have 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 : ℝ)
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
-- 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 : ℝ)
⊢ ∫ (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 : ℝ)
have 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 : ℝ)
Tactic: apply (integral_mono (by simpa using f.integrable_pow_mul μ 0) _ h').trans
-- 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₁ :
  ∫ (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 : ℝ)
⊢ ∫ (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 : ℝ)
have 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 : ℝ))
  μ
Tactic: apply (integral_mono (by simpa using f.integrable_pow_mul μ 0) _ h').trans
-- 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 (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)
have 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 : ℝ)
Tactic: unfold schwartzSeminormFamily