internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.Distribution.one_apply
Proof state before:
E : Type u_1
F : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℝ F
mE : MeasureSpace E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : BorelSpace E
inst✝⁹ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
𝕜' : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedSpace ℝ 𝕜'
inst✝² : NormedSpace 𝕜' F
inst✝¹ : SMulCommClass ℝ 𝕜' F
inst✝ : IsScalarTower ℝ 𝕜' F
φ : 𝓢(E, F)
⊢ One.one φ = ∫ (x : E), φ x
Tactic:
simp [One.one]
Proof state after:
E : Type u_1
F : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℝ F
mE : MeasureSpace E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : BorelSpace E
inst✝⁹ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
𝕜' : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedSpace ℝ 𝕜'
inst✝² : NormedSpace 𝕜' F
inst✝¹ : SMulCommClass ℝ 𝕜' F
inst✝ : IsScalarTower ℝ 𝕜' F
φ : 𝓢(E, F)
⊢ integralCLM φ = ∫ (x : E), φ x
Theorem: SchwartzMap.Distribution.one_apply
Proof state before:
E : Type u_1
F : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℝ F
mE : MeasureSpace E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : BorelSpace E
inst✝⁹ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
𝕜' : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedSpace ℝ 𝕜'
inst✝² : NormedSpace 𝕜' F
inst✝¹ : SMulCommClass ℝ 𝕜' F
inst✝ : IsScalarTower ℝ 𝕜' F
φ : 𝓢(E, F)
⊢ integralCLM φ = ∫ (x : E), φ x
Tactic:
rw [integralCLM_apply]
Proof state after:
no goals
Theorem: SchwartzMap.Distribution.const_apply
Proof state before:
E : Type u_1
F : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℝ F
mE : MeasureSpace E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : BorelSpace E
inst✝⁹ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
𝕜' : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedSpace ℝ 𝕜'
inst✝² : NormedSpace 𝕜' F
inst✝¹ : SMulCommClass ℝ 𝕜' F
inst✝ : IsScalarTower ℝ 𝕜' F
c : 𝕜'
φ : 𝓢(E, F)
⊢ (const E F c) φ = c • ∫ (x : E), φ x
Tactic:
simp [const, one_apply]
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_zero
Proof state before:
n : ℕ
⊢ iteratedDeriv n 0 = 0
Tactic:
induction n with
| zero => simp
| succ n h =>
  simp [iteratedDeriv_succ, h]
  ext x
  apply deriv_const
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_zero
Proof state before:
case zero

⊢ iteratedDeriv Nat.zero 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_zero
Proof state before:
case succ
n : ℕ
h : iteratedDeriv n 0 = 0
⊢ iteratedDeriv (Nat.succ n) 0 = 0
Tactic:
simp [iteratedDeriv_succ, h]
Proof state after:
case succ
n : ℕ
h : iteratedDeriv n 0 = 0
⊢ deriv 0 = 0
Theorem: Bump₁.iteratedDeriv_zero
Proof state before:
case succ
n : ℕ
h : iteratedDeriv n 0 = 0
⊢ deriv 0 = 0
Tactic:
ext x
Proof state after:
case succ.h
n : ℕ
h : iteratedDeriv n 0 = 0
x : ℝ
⊢ deriv 0 x = 0 x
Theorem: Bump₁.iteratedDeriv_zero
Proof state before:
case succ.h
n : ℕ
h : iteratedDeriv n 0 = 0
x : ℝ
⊢ deriv 0 x = 0 x
Tactic:
apply deriv_const
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_add
Proof state before:
n : ℕ
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
⊢ iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
Tactic:
induction n with
| zero => simp
| succ n h =>
  simp [iteratedDeriv_succ, h]
  ext x
  apply deriv_add
  . apply Differentiable.differentiableAt
    exact ContDiff.differentiable_iteratedDeriv _ hf (WithTop.coe_lt_top _)
  . apply Differentiable.differentiableAt
    exact ContDiff.differentiable_iteratedDeriv _ hg (WithTop.coe_lt_top _)
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_add
Proof state before:
case zero
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
⊢ iteratedDeriv Nat.zero (f + g) = iteratedDeriv Nat.zero f + iteratedDeriv Nat.zero g
Tactic:
simp
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_add
Proof state before:
case succ
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
⊢ iteratedDeriv (Nat.succ n) (f + g) = iteratedDeriv (Nat.succ n) f + iteratedDeriv (Nat.succ n) g
Tactic:
simp [iteratedDeriv_succ, h]
Proof state after:
case succ
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
⊢ deriv (iteratedDeriv n f + iteratedDeriv n g) = deriv (iteratedDeriv n f) + deriv (iteratedDeriv n g)
Theorem: Bump₁.iteratedDeriv_add
Proof state before:
case succ
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
⊢ deriv (iteratedDeriv n f + iteratedDeriv n g) = deriv (iteratedDeriv n f) + deriv (iteratedDeriv n g)
Tactic:
ext x
Proof state after:
case succ.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ deriv (iteratedDeriv n f + iteratedDeriv n g) x = (deriv (iteratedDeriv n f) + deriv (iteratedDeriv n g)) x
Theorem: Bump₁.iteratedDeriv_add
Proof state before:
case succ.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ deriv (iteratedDeriv n f + iteratedDeriv n g) x = (deriv (iteratedDeriv n f) + deriv (iteratedDeriv n g)) x
Tactic:
apply deriv_add
Proof state after:
case succ.h.hf
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n f y) x

case succ.h.hg
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n g y) x
Theorem: Bump₁.iteratedDeriv_add
Proof state before:
case succ.h.hf
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n f y) x

case succ.h.hg
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n g y) x
Tactic:
. apply Differentiable.differentiableAt
  exact ContDiff.differentiable_iteratedDeriv _ hf (WithTop.coe_lt_top _)
Proof state after:
case succ.h.hg
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n g y) x
Theorem: Bump₁.iteratedDeriv_add
Proof state before:
case succ.h.hg
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n g y) x
Tactic:
. apply Differentiable.differentiableAt
  exact ContDiff.differentiable_iteratedDeriv _ hg (WithTop.coe_lt_top _)
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_add
Proof state before:
case succ.h.hf
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n f y) x
Tactic:
apply Differentiable.differentiableAt
Proof state after:
case succ.h.hf.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ Differentiable ℝ fun y => iteratedDeriv n f y
Theorem: Bump₁.iteratedDeriv_add
Proof state before:
case succ.h.hf.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ Differentiable ℝ fun y => iteratedDeriv n f y
Tactic:
exact ContDiff.differentiable_iteratedDeriv _ hf (WithTop.coe_lt_top _)
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_add
Proof state before:
case succ.h.hg
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n g y) x
Tactic:
apply Differentiable.differentiableAt
Proof state after:
case succ.h.hg.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ Differentiable ℝ fun y => iteratedDeriv n g y
Theorem: Bump₁.iteratedDeriv_add
Proof state before:
case succ.h.hg.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ Differentiable ℝ fun y => iteratedDeriv n g y
Tactic:
exact ContDiff.differentiable_iteratedDeriv _ hg (WithTop.coe_lt_top _)
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_neg
Proof state before:
n : ℕ
f : ℝ → ℝ
⊢ iteratedDeriv n (-f) = -iteratedDeriv n f
Tactic:
induction n with
| zero => simp
| succ n h =>
  conv => rhs; rw [iteratedDeriv_succ]
  rw [iteratedDeriv_succ]
  rw [h]
  ext x
  conv => lhs; arg 1; intro x
  simp [deriv.neg']
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_neg
Proof state before:
case zero
f : ℝ → ℝ
⊢ iteratedDeriv Nat.zero (-f) = -iteratedDeriv Nat.zero f
Tactic:
simp
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_neg
Proof state before:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (-f) = -iteratedDeriv (Nat.succ n) f
Tactic:
conv => rhs; rw [iteratedDeriv_succ]
Proof state after:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (-f) = -deriv (iteratedDeriv n f)
Theorem: Bump₁.iteratedDeriv_neg
Proof state before:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (-f) = -deriv (iteratedDeriv n f)
Tactic:
rw [iteratedDeriv_succ]
Proof state after:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ deriv (iteratedDeriv n (-f)) = -deriv (iteratedDeriv n f)
Theorem: Bump₁.iteratedDeriv_neg
Proof state before:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ deriv (iteratedDeriv n (-f)) = -deriv (iteratedDeriv n f)
Tactic:
rw [h]
Proof state after:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ deriv (-iteratedDeriv n f) = -deriv (iteratedDeriv n f)
Theorem: Bump₁.iteratedDeriv_neg
Proof state before:
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ deriv (-iteratedDeriv n f) = -deriv (iteratedDeriv n f)
Tactic:
ext x
Proof state after:
case succ.h
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
x : ℝ
⊢ deriv (-iteratedDeriv n f) x = (-deriv (iteratedDeriv n f)) x
Theorem: Bump₁.iteratedDeriv_neg
Proof state before:
case succ.h
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
x : ℝ
⊢ deriv (-iteratedDeriv n f) x = (-deriv (iteratedDeriv n f)) x
Tactic:
conv => lhs; arg 1; intro x
Proof state after:
case succ.h
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
x : ℝ
⊢ deriv (fun x => (-iteratedDeriv n f) x) x = (-deriv (iteratedDeriv n f)) x
Theorem: Bump₁.iteratedDeriv_neg
Proof state before:
case succ.h
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
x : ℝ
⊢ deriv (fun x => (-iteratedDeriv n f) x) x = (-deriv (iteratedDeriv n f)) x
Tactic:
simp [deriv.neg']
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_const_smul
Proof state before:
n : ℕ
r : ℝ
f : ℝ → ℝ
⊢ iteratedDeriv n (r • f) = r • iteratedDeriv n f
Tactic:
induction n with
| zero => simp
| succ n h =>
  conv => rhs; rw [iteratedDeriv_succ]
  rw [iteratedDeriv_succ]
  rw [h]
  ext x
  conv => lhs; arg 1; intro x
  simp [deriv_const_mul]
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_const_smul
Proof state before:
case zero
r : ℝ
f : ℝ → ℝ
⊢ iteratedDeriv Nat.zero (r • f) = r • iteratedDeriv Nat.zero f
Tactic:
simp
Proof state after:
no goals
Theorem: Bump₁.iteratedDeriv_const_smul
Proof state before:
case succ
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (r • f) = r • iteratedDeriv (Nat.succ n) f
Tactic:
conv => rhs; rw [iteratedDeriv_succ]
Proof state after:
case succ
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (r • f) = r • deriv (iteratedDeriv n f)
Theorem: Bump₁.iteratedDeriv_const_smul
Proof state before:
case succ
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (r • f) = r • deriv (iteratedDeriv n f)
Tactic:
rw [iteratedDeriv_succ]
Proof state after:
case succ
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
⊢ deriv (iteratedDeriv n (r • f)) = r • deriv (iteratedDeriv n f)
Theorem: Bump₁.iteratedDeriv_const_smul
Proof state before:
case succ
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
⊢ deriv (iteratedDeriv n (r • f)) = r • deriv (iteratedDeriv n f)
Tactic:
rw [h]
Proof state after:
case succ
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
⊢ deriv (r • iteratedDeriv n f) = r • deriv (iteratedDeriv n f)
Theorem: Bump₁.iteratedDeriv_const_smul
Proof state before:
case succ
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
⊢ deriv (r • iteratedDeriv n f) = r • deriv (iteratedDeriv n f)
Tactic:
ext x
Proof state after:
case succ.h
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
x : ℝ
⊢ deriv (r • iteratedDeriv n f) x = (r • deriv (iteratedDeriv n f)) x
Theorem: Bump₁.iteratedDeriv_const_smul
Proof state before:
case succ.h
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
x : ℝ
⊢ deriv (r • iteratedDeriv n f) x = (r • deriv (iteratedDeriv n f)) x
Tactic:
conv => lhs; arg 1; intro x
Proof state after:
case succ.h
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
x : ℝ
⊢ deriv (fun x => (r • iteratedDeriv n f) x) x = (r • deriv (iteratedDeriv n f)) x
Theorem: Bump₁.iteratedDeriv_const_smul
Proof state before:
case succ.h
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
x : ℝ
⊢ deriv (fun x => (r • iteratedDeriv n f) x) x = (r • deriv (iteratedDeriv n f)) x
Tactic:
simp [deriv_const_mul]
Proof state after:
no goals
Theorem: Bump₁.absNthDeriv_nonneg
Proof state before:
n : ℕ
f : Bump ℝ
x : ℝ
⊢ 0 ≤ absNthDeriv n f x
Tactic:
simp [absNthDeriv]
Proof state after:
no goals
Theorem: Bump₁.absNthDeriv_continuous
Proof state before:
n : ℕ
f : Bump ℝ
⊢ Continuous (absNthDeriv n f)
Tactic:
simp [absNthDeriv_def]
Proof state after:
n : ℕ
f : Bump ℝ
⊢ Continuous fun x => ‖iteratedDeriv n (↑f) x‖₊
Theorem: Bump₁.absNthDeriv_continuous
Proof state before:
n : ℕ
f : Bump ℝ
⊢ Continuous fun x => ‖iteratedDeriv n (↑f) x‖₊
Tactic:
apply Continuous.nnnorm
Proof state after:
case a
n : ℕ
f : Bump ℝ
⊢ Continuous fun x => iteratedDeriv n (↑f) x
Theorem: Bump₁.absNthDeriv_continuous
Proof state before:
case a
n : ℕ
f : Bump ℝ
⊢ Continuous fun x => iteratedDeriv n (↑f) x
Tactic:
exact ContDiff.continuous_iteratedDeriv _ f.contDiff (by norm_num)
Proof state after:
no goals
Theorem: Bump₁.absNthDeriv_continuous
Proof state before:
n : ℕ
f : Bump ℝ
⊢ ↑n ≤ ⊤
Tactic:
norm_num
Proof state after:
no goals
Theorem: Bump₁.absNthDeriv_bddAbove_image
Proof state before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ BddAbove (absNthDeriv n f '' K)
Tactic:
apply IsCompact.bddAbove_image hK
Proof state after:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ContinuousOn (absNthDeriv n f) K
Theorem: Bump₁.absNthDeriv_bddAbove_image
Proof state before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ContinuousOn (absNthDeriv n f) K
Tactic:
exact Continuous.continuousOn absNthDeriv_continuous
Proof state after:
no goals
Theorem: Bump₁.iSup₂_coe_eq_coe_sSup
Proof state before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ⨆ x ∈ K, ↑(absNthDeriv n f x) = ↑(sSup (absNthDeriv n f '' K))
Tactic:
rw [ENNReal.coe_sSup (absNthDeriv_bddAbove_image hK)]
Proof state after:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ⨆ x ∈ K, ↑(absNthDeriv n f x) = ⨆ a ∈ absNthDeriv n f '' K, ↑a
Theorem: Bump₁.iSup₂_coe_eq_coe_sSup
Proof state before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ⨆ x ∈ K, ↑(absNthDeriv n f x) = ⨆ a ∈ absNthDeriv n f '' K, ↑a
Tactic:
repeat rw [← sSup_image]
Proof state after:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ sSup ((fun x => ↑(absNthDeriv n f x)) '' K) = sSup ((fun a => ↑a) '' (absNthDeriv n f '' K))
Theorem: Bump₁.iSup₂_coe_eq_coe_sSup
Proof state before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ sSup ((fun x => ↑(absNthDeriv n f x)) '' K) = sSup ((fun a => ↑a) '' (absNthDeriv n f '' K))
Tactic:
congr
Proof state after:
case e_a
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ (fun x => ↑(absNthDeriv n f x)) '' K = (fun a => ↑a) '' (absNthDeriv n f '' K)
Theorem: Bump₁.iSup₂_coe_eq_coe_sSup
Proof state before:
case e_a
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ (fun x => ↑(absNthDeriv n f x)) '' K = (fun a => ↑a) '' (absNthDeriv n f '' K)
Tactic:
ext x
Proof state after:
case e_a.h
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
x : ENNReal
⊢ x ∈ (fun x => ↑(absNthDeriv n f x)) '' K ↔ x ∈ (fun a => ↑a) '' (absNthDeriv n f '' K)
Theorem: Bump₁.iSup₂_coe_eq_coe_sSup
Proof state before:
case e_a.h
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
x : ENNReal
⊢ x ∈ (fun x => ↑(absNthDeriv n f x)) '' K ↔ x ∈ (fun a => ↑a) '' (absNthDeriv n f '' K)
Tactic:
simp
Proof state after:
no goals
Theorem: Bump₁.iSup₂_coe_eq_coe_sSup
Proof state before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ sSup ((fun x => ↑(absNthDeriv n f x)) '' K) = ⨆ a ∈ absNthDeriv n f '' K, ↑a
Tactic:
rw [← sSup_image]
Proof state after:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ sSup ((fun x => ↑(absNthDeriv n f x)) '' K) = sSup ((fun a => ↑a) '' (absNthDeriv n f '' K))
Theorem: Bump₁.iSup_absNthDeriv_ne_top
Proof state before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ⨆ x ∈ K, ↑(absNthDeriv n f x) ≠ ⊤
Tactic:
rw [iSup₂_coe_eq_coe_sSup hK]
Proof state after:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ↑(sSup (absNthDeriv n f '' K)) ≠ ⊤
Theorem: Bump₁.iSup_absNthDeriv_ne_top
Proof state before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ↑(sSup (absNthDeriv n f '' K)) ≠ ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: Equiv.piSplitAt_symm_apply_eq_update_zero
Proof state before:
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
i : ι
x : D i × ((j : { j // j ≠ i }) → D ↑j)
⊢ (piSplitAt i D).symm x = Function.update ((piSplitAt i D).symm (0, x.2)) i x.1
Tactic:
ext j
Proof state after:
case h
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
i : ι
x : D i × ((j : { j // j ≠ i }) → D ↑j)
j : ι
⊢ (piSplitAt i D).symm x j = Function.update ((piSplitAt i D).symm (0, x.2)) i x.1 j
Theorem: Equiv.piSplitAt_symm_apply_eq_update_zero
Proof state before:
case h
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
i : ι
x : D i × ((j : { j // j ≠ i }) → D ↑j)
j : ι
⊢ (piSplitAt i D).symm x j = Function.update ((piSplitAt i D).symm (0, x.2)) i x.1 j
Tactic:
simp [Equiv.piSplitAt_symm_apply]
Proof state after:
case h
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
i : ι
x : D i × ((j : { j // j ≠ i }) → D ↑j)
j : ι
⊢ (if h : j = i then (_ : i = j) ▸ x.1 else x.snd { val := j, property := (_ : ¬j = i) }) =
    Function.update ((piSplitAt i D).symm (0, x.2)) i x.1 j
Theorem: Equiv.piSplitAt_symm_apply_eq_update_zero
Proof state before:
case h
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
i : ι
x : D i × ((j : { j // j ≠ i }) → D ↑j)
j : ι
⊢ (if h : j = i then (_ : i = j) ▸ x.1 else x.snd { val := j, property := (_ : ¬j = i) }) =
    Function.update ((piSplitAt i D).symm (0, x.2)) i x.1 j
Tactic:
rw [Function.update]
Proof state after:
case h
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
i : ι
x : D i × ((j : { j // j ≠ i }) → D ↑j)
j : ι
⊢ (if h : j = i then (_ : i = j) ▸ x.1 else x.snd { val := j, property := (_ : ¬j = i) }) =
    if h : j = i then (_ : i = j) ▸ x.1 else (piSplitAt i D).symm (0, x.2) j
Theorem: Equiv.piSplitAt_symm_apply_eq_update_zero
Proof state before:
case h
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
i : ι
x : D i × ((j : { j // j ≠ i }) → D ↑j)
j : ι
⊢ (if h : j = i then (_ : i = j) ▸ x.1 else x.snd { val := j, property := (_ : ¬j = i) }) =
    if h : j = i then (_ : i = j) ▸ x.1 else (piSplitAt i D).symm (0, x.2) j
Tactic:
by_cases h : j = i <;> simp [h]
Proof state after:
no goals