funProp minimal setup for ContDiff(At/On) #
theorem
contDiff_id'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{n : WithTop ℕ∞}
:
ContDiff K n fun (x : E) => x
theorem
contDiffAt_id'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{x : E}
{n : WithTop ℕ∞}
:
ContDiffAt K n (fun (x : E) => x) x
theorem
contDiffOn_id'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{s : Set E}
{n : WithTop ℕ∞}
:
ContDiffOn K n (fun (x : E) => x) s
theorem
ContDiff.comp'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace K F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace K G]
{f : E → F}
{n : WithTop ℕ∞}
{g : F → G}
(hg : ContDiff K n g)
(hf : ContDiff K n f)
:
ContDiff K n fun (x : E) => g (f x)
theorem
ContDiffAt.comp'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace K F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace K G]
{x : E}
{n : WithTop ℕ∞}
{f : E → F}
{g : F → G}
(hg : ContDiffAt K n g (f x))
(hf : ContDiffAt K n f x)
:
ContDiffAt K n (fun (x : E) => g (f x)) x
theorem
contDiff_pi'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{n : WithTop ℕ∞}
{ι : Type u_5}
[Fintype ι]
{F' : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (F' i)]
[(i : ι) → NormedSpace K (F' i)]
{Φ : E → (i : ι) → F' i}
(hΦ : ∀ (i : ι), ContDiff K n fun (x : E) => Φ x i)
:
ContDiff K n Φ
theorem
contDiffOn_pi'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{s : Set E}
{n : WithTop ℕ∞}
{ι : Type u_5}
[Fintype ι]
{F' : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (F' i)]
[(i : ι) → NormedSpace K (F' i)]
{Φ : E → (i : ι) → F' i}
(hΦ : ∀ (i : ι), ContDiffOn K n (fun (x : E) => Φ x i) s)
:
ContDiffOn K n Φ s
theorem
contDiffAt_pi'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{x : E}
{n : WithTop ℕ∞}
{ι : Type u_5}
[Fintype ι]
{F' : ι → Type u_6}
[(i : ι) → NormedAddCommGroup (F' i)]
[(i : ι) → NormedSpace K (F' i)]
{Φ : E → (i : ι) → F' i}
(hΦ : ∀ (i : ι), ContDiffAt K n (fun (x : E) => Φ x i) x)
:
ContDiffAt K n Φ x
theorem
ContDiffOn.div'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{s : Set E}
{f g : E → K}
{n : WithTop ℕ∞}
(hf : ContDiffOn K n f s)
(hg : ContDiffOn K n g s)
(h₀ : ∀ x ∈ s, g x ≠ 0)
:
ContDiffOn K n (fun (x : E) => f x / g x) s
theorem
ContDiff.differentiable_iteratedDeriv'
{K : Type u_1}
[NontriviallyNormedField K]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace K F]
{m : ℕ}
{f : K → F}
(hf : ContDiff K (↑m + 1) f)
:
Differentiable K (iteratedDeriv m f)
Original version ContDiff.differentiable_iteratedDeriv introduces a new variable (n:ℕ∞)
and funProp can't work with such theorem. The theorem should be state where n is explicitly
the smallest possible value i.e. n=m+1.
In conjunction with ContDiff.of_le we can recover the full power of the original theorem.