awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
k n : ℕ
rcases :
  ∀ (C : ℝ)
    (hC :
      ∀ (x : E),
        ‖x‖ ^ k *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDeriv ℝ n f.toFun x) ≤
          C),
    ∃ (C : ℝ),
      0 < C ∧
        ∀ (x : E),
          ‖x‖ ^ k *
              norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
                (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
            C
⊢ ∃ (C : ℝ),
    0 < C ∧
      ∀ (x : E),
        ‖x‖ ^ k *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
          C

Tactic:
rcases f.decay' k n with ⟨C, hC⟩

Premises used: SchwartzMap.decay'
-- 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)
k n : ℕ
C : ℝ
hC :
  ∀ (x : E),
    ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f.toFun x) ≤
      C
⊢ 0 < max C 1

Tactic:
positivity
-- 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)
k n : ℕ
C : ℝ
hC :
  ∀ (x : E),
    ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f.toFun x) ≤
      C
⊢ ∃ (C : ℝ),
    0 < C ∧
      ∀ (x : E),
        ‖x‖ ^ k *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
          C

Tactic:
exact ⟨max C 1, by positivity, fun x => (hC x).trans (le_max_left _ _)⟩
-- 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)
n : ℕ∞
⊢ ContDiff.{0, u_5, u_6} ℝ (E := E) (F := F) (↑n : ℕ∞ω) (⇑f : (a : E) → F)

Tactic:
f.smooth'.of_le (mod_cast le_top)

Premises used: WithTop.coe_le_coe._simp_1, cast, ContDiff.of_le, le_top, SchwartzMap.smooth', Eq.symm
-- 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)
n : ℕ∞
x : E
⊢ ContDiffAt.{0, u_5, u_6} ℝ (F := F) (↑n : ℕ∞ω) (⇑f : (a : E) → F) x

Tactic:
(f.smooth n).contDiffAt

Premises used: SchwartzMap.smooth, ContDiff.contDiffAt
-- 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)
⊢ Continuous.{u_5, u_6} (X := E) (Y := F) (⇑f : (a : E) → F)

Tactic:
(f.smooth 0).continuous

Premises used: ContDiff.continuous, OfNat.ofNat, SchwartzMap.smooth
-- 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)
⊢ Differentiable.{0, u_5, u_6} ℝ (E := E) (F := F) (⇑f : (a : E) → F)

Tactic:
(f.smooth 1).differentiable one_ne_zero

Premises used: ContDiff.differentiable, one_ne_zero, OfNat.ofNat, SchwartzMap.smooth
-- 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
⊢ DifferentiableAt.{0, u_5, u_6} ℝ (F := F) (⇑f : (a : E) → F) x

Tactic:
f.differentiable.differentiableAt

Premises used: Differentiable.differentiableAt, SchwartzMap.differentiable
-- 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 g : 𝓢(E, F)
h : ∀ (x : E), Eq.{u_6 + 1} (α := F) ((f : (a : E) → F) x : F) ((g : (a : E) → F) x : F)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- 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)
k : ℕ
obtain :
  ∀ (d : ℝ),
    0 < d →
      ∀
        (hd' :
          ∀ (x : E),
            ‖x‖ ^ k *
                norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F)
                  (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x) ≤
              d),
        IsBigO.{u_5, u_6, 0} (E := F) (F := ℝ) (cocompact E) (⇑f : (a : E) → F) fun (x : E) ↦
          HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))
⊢ IsBigO.{u_5, u_6, 0} (E := F) (F := ℝ) (cocompact E) (⇑f : (a : E) → F) fun (x : E) ↦
    HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))

Tactic:
obtain ⟨d, _, hd'⟩ := f.decay k 0

Premises used: SchwartzMap.decay, OfNat.ofNat
-- 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)
k : ℕ
d : ℝ
left : 0 < d
hd' :
  ∀ (x : E),
    ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F)
          (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x) ≤
      d
⊢ ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d

Tactic:
simp only [norm_iteratedFDeriv_zero] at hd'

Premises used: norm_iteratedFDeriv_zero
-- 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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
simp_rw :
  ∃ (c : ℝ),
    ∀ᶠ (x : E) in cocompact E, norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖
⊢ IsBigO.{u_5, u_6, 0} (E := F) (F := ℝ) (cocompact E) (⇑f : (a : E) → F) fun (x : E) ↦
    HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))

Tactic:
simp_rw [Asymptotics.IsBigO, Asymptotics.IsBigOWith]

Premises used: Asymptotics.IsBigOWith, Asymptotics.IsBigO
-- 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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : E) in cocompact E, norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖

Tactic:
⟨d, Filter.Eventually.filter_mono Filter.cocompact_le_cofinite ?_⟩

Premises used: Filter.Eventually.filter_mono, Filter.cocompact_le_cofinite, Exists.intro
-- 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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
refine :
  ∀ᶠ (x : E) in cofinite, norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : E) in cocompact E, norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖

Tactic:
refine ⟨d, Filter.Eventually.filter_mono Filter.cocompact_le_cofinite ?_⟩
-- 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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
⊢ ∀ᶠ (x : E) in cofinite, norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖

Tactic:
(Filter.eventually_cofinite_ne 0).mono fun x hx ↦ ?_

Premises used: Filter.eventually_cofinite_ne, Filter.Eventually.mono, OfNat.ofNat
-- 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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
refine :
  ∀ (x : E) (hx : x ≠ 0), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖
⊢ ∀ᶠ (x : E) in cofinite, norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖

Tactic:
refine (Filter.eventually_cofinite_ne 0).mono fun x hx ↦ ?_

Premises used: Filter.eventually_cofinite_ne, Filter.Eventually.mono, OfNat.ofNat
-- 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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
x : E
hx : x ≠ 0
⊢ 0 ≤ HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))

Tactic:
positivity
-- 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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
x : E
hx : x ≠ 0
⊢ 0 < HPow.hPow (β := ℤ) ‖x‖ (↑k : ℤ)

Tactic:
positivity
-- 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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
x : E
hx : x ≠ 0
rw : HPow.hPow (β := ℤ) ‖x‖ (↑k : ℤ) * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
⊢ norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖

Tactic:
rw [Real.norm_of_nonneg (by positivity), zpow_neg, ← div_eq_mul_inv, le_div_iff₀' (by positivity)]

Premises used: le_div_iff₀', div_eq_mul_inv, zpow_neg, Real.norm_of_nonneg
-- 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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
x : E
hx : x ≠ 0
⊢ HPow.hPow (β := ℤ) ‖x‖ (↑k : ℤ) * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d

Tactic:
hd' x

Premises used: zpowRec
-- 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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
x : E
hx : x ≠ 0
⊢ HPow.hPow (β := ℤ) ‖x‖ (↑k : ℤ) * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d

Tactic:
exact hd' x
-- 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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
⊢ -(↑k : ℝ) ≤ s

Tactic:
have hk : -(k : ℝ) ≤ s := neg_le.mp (Nat.le_ceil (-s))
-- 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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
⊢ IsBigO.{u_5, u_6, 0} (E := F) (F := ℝ) (cocompact E) (⇑f : (a : E) → F) fun (x : E) ↦ ‖x‖ ^ s

Tactic:
(isBigO_cocompact_zpow_neg_nat f k).trans ?_

Premises used: Asymptotics.IsBigO.trans, SchwartzMap.isBigO_cocompact_zpow_neg_nat
-- 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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
refine : IsBigO (E := ℝ) (F := ℝ) (cocompact E) (fun (x : E) ↦ HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))) fun (x : E) ↦ ‖x‖ ^ s
⊢ IsBigO.{u_5, u_6, 0} (E := F) (F := ℝ) (cocompact E) (⇑f : (a : E) → F) fun (x : E) ↦ ‖x‖ ^ s

Tactic:
refine (isBigO_cocompact_zpow_neg_nat f k).trans ?_

Premises used: Asymptotics.IsBigO.trans, SchwartzMap.isBigO_cocompact_zpow_neg_nat
-- 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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
suffices : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℤ) x (-(↑k : ℤ))) fun (x : ℝ) ↦ x ^ s
⊢ IsBigO (E := ℝ) (F := ℝ) (cocompact E) (fun (x : E) ↦ HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))) fun (x : E) ↦ ‖x‖ ^ s

Tactic:
suffices (fun x : ℝ ↦ x ^ (-k : ℤ)) =O[atTop] fun x : ℝ ↦ x ^ s
    from this.comp_tendsto tendsto_norm_cocompact_atTop
-- 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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
simp_rw : ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, ‖HPow.hPow (β := ℤ) x (-(↑k : ℤ))‖ ≤ c * ‖x ^ s‖
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℤ) x (-(↑k : ℤ))) fun (x : ℝ) ↦ x ^ s

Tactic:
simp_rw [Asymptotics.IsBigO, Asymptotics.IsBigOWith]

Premises used: Asymptotics.IsBigOWith, Asymptotics.IsBigO
-- 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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, ‖HPow.hPow (β := ℤ) x (-(↑k : ℤ))‖ ≤ c * ‖x ^ s‖

Tactic:
⟨1, (Filter.eventually_ge_atTop 1).mono fun x hx ↦ ?_⟩

Premises used: Filter.Eventually.mono, Exists.intro, Filter.eventually_ge_atTop, OfNat.ofNat
-- 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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
refine : ∀ (x : ℝ) (hx : 1 ≤ x), ‖HPow.hPow (β := ℤ) x (-(↑k : ℤ))‖ ≤ 1 * ‖x ^ s‖
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, ‖HPow.hPow (β := ℤ) x (-(↑k : ℤ))‖ ≤ c * ‖x ^ s‖

Tactic:
refine ⟨1, (Filter.eventually_ge_atTop 1).mono fun x hx ↦ ?_⟩
-- 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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ HPow.hPow (β := ℤ) x (-(↑k : ℤ))

Tactic:
positivity
-- 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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x ^ s

Tactic:
positivity
-- 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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
x : ℝ
hx : 1 ≤ x
rw : HPow.hPow (β := ℝ) x (-(↑k : ℝ)) ≤ x ^ s
⊢ ‖HPow.hPow (β := ℤ) x (-(↑k : ℤ))‖ ≤ 1 * ‖x ^ s‖

Tactic:
rw [one_mul, Real.norm_of_nonneg (by positivity), Real.norm_of_nonneg (by positivity),
    ← Real.rpow_intCast, Int.cast_neg, Int.cast_natCast]

Premises used: Int.cast_neg, Int.cast_natCast, Real.rpow_intCast, one_mul, Real.norm_of_nonneg
-- 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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
x : ℝ
hx : 1 ≤ x
⊢ HPow.hPow (β := ℝ) x (-(↑k : ℝ)) ≤ x ^ s

Tactic:
Real.rpow_le_rpow_of_exponent_le hx hk

Premises used: Real.rpow_le_rpow_of_exponent_le
-- 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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
x : ℝ
hx : 1 ≤ x
⊢ HPow.hPow (β := ℝ) x (-(↑k : ℝ)) ≤ x ^ s

Tactic:
exact Real.rpow_le_rpow_of_exponent_le hx hk

Premises used: Real.rpow_le_rpow_of_exponent_le
-- 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)
inst_4 : ProperSpace E
k : ℤ
⊢ IsBigO.{u_5, u_6, 0} (E := F) (F := ℝ) (cocompact E) (⇑f : (a : E) → F) fun (x : E) ↦ ‖x‖ ^ k

Tactic:
simpa only [Real.rpow_intCast] using isBigO_cocompact_rpow f k

Premises used: Int.cast, Real.rpow_intCast, SchwartzMap.isBigO_cocompact_rpow
-- 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)
apply : Tendsto (β := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) ‖x‖ (-1)) (cocompact E) (𝓝 0)
⊢ Tendsto.{u_5, u_6} (β := F) (⇑f : (a : E) → F) (cocompact E) (𝓝 0)

Tactic:
apply (isBigO_cocompact_rpow f (-1)).trans_tendsto

Premises used: Asymptotics.IsBigO.trans_tendsto, OfNat.ofNat, Neg.neg, SchwartzMap.isBigO_cocompact_rpow
-- 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)
simp_rw : Tendsto (β := ℝ) (fun (x : E) ↦ ‖x‖⁻¹) (cocompact E) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) ‖x‖ (-1)) (cocompact E) (𝓝 0)

Tactic:
simp_rw [Real.rpow_neg_one]

Premises used: Real.rpow_neg_one
-- 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)
⊢ Tendsto (β := ℝ) (fun (x : E) ↦ ‖x‖⁻¹) (cocompact E) (𝓝 0)

Tactic:
tendsto_norm_cocompact_atTop.inv_tendsto_atTop

Premises used: Filter.Tendsto.inv_tendsto_atTop, tendsto_norm_cocompact_atTop
-- 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)
⊢ Tendsto (β := ℝ) (fun (x : E) ↦ ‖x‖⁻¹) (cocompact E) (𝓝 0)

Tactic:
exact tendsto_norm_cocompact_atTop.inv_tendsto_atTop

Premises used: Filter.Tendsto.inv_tendsto_atTop, tendsto_norm_cocompact_atTop
-- 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
k n : ℕ
f : 𝓢(E, F)
⊢ ∃ (c : ℝ),
    Membership.mem (γ := Set ℝ)
      {c : ℝ |
        0 ≤ c ∧
          ∀ (x : E),
            ‖x‖ ^ k *
                norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
                  (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
              c}
      c

Tactic:
let ⟨M, hMp, hMb⟩ := f.decay k n
  ⟨M, le_of_lt hMp, hMb⟩

Premises used: setOf, le_of_lt, Membership.mem, Exists, LE.le, And, _private.0.SchwartzMap.bounds_nonempty.match_1, And.intro, Exists.intro, SchwartzMap.decay, OfNat.ofNat
-- 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
k n : ℕ
f : 𝓢(E, F)
⊢ BddBelow (α := ℝ)
    {c : ℝ |
      0 ≤ c ∧
        ∀ (x : E),
          ‖x‖ ^ k *
              norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
                (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
            c}

Tactic:
⟨0, fun _ ⟨hn, _⟩ => hn⟩

Premises used: _private.0.SchwartzMap.bounds_bddBelow.match_1, LE.le, Set.Nonempty, BddBelow, Exists.intro, OfNat.ofNat
-- 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
k n : ℕ
f g : 𝓢(E, F)
x : E
rw :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
    ‖x‖ ^ k *
      (norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x))
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
    ‖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_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)

Tactic:
rw [← mul_add]

Premises used: mul_add
-- 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
k n : ℕ
f g : 𝓢(E, F)
x : E
hbc :
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
    ‖x‖ ^ k *
      (norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x))

Tactic:
gcongr _ * ?_