Documentation

Mathlib.Tactic.FunProp.ContDiff

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 : ℕ∞} :
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 : ℕ∞} :
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 : ℕ∞} :
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 : EF} {n : ℕ∞} {g : FG} (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 : ℕ∞} {f : EF} {g : FG} (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 : ℕ∞} {ι : 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 : ℕ∞} {ι : 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 : ℕ∞} {ι : 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} [CompleteSpace K] {f : EK} {g : EK} {n : ℕ∞} (hf : ContDiffOn K n f s) (hg : ContDiffOn K n g s) (h₀ : xs, 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 : KF} (hf : ContDiff K (m + 1) 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.