LeanPool.SardMoreira.ContDiffMoreiraHolder

structure ContDiffMoreiraHolderAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (α : ↑unitInterval) (f : E → F) (a : E) : Prop

A map f is C^{k+(α)} at a point a, meaning it is C^k at a and its k-th derivative satisfies a pointwise Hölder estimate of exponent α at a.

• contDiffAt : ContDiffAt ℝ (↑k) f a

  A C^{k+(α)} map is in particular C^k at the point.

• isBigO : (fun (x : E) => iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a) =O[nhds a] fun (x : E) => ‖x - a‖ ^ ↑α

  A C^{k+(α)} map satisfies D^k f x - D^k f a = O(‖x - a‖^α) as x → a.

theorem contDiffMoreiraHolderAt_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (α : ↑unitInterval) (f : E → F) (a : E) : ContDiffMoreiraHolderAt k α f a ↔ ContDiffAt ℝ (↑k) f a ∧ (fun (x : E) => iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a) =O[nhds a] fun (x : E) => ‖x - a‖ ^ ↑α

theorem ContDiffAt.contDiffMoreiraHolderAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : WithTop ℕ∞} {k : ℕ} {f : E → F} {a : E} (h : ContDiffAt ℝ n f a) (hk : ↑k < n) (α : ↑unitInterval) : ContDiffMoreiraHolderAt k α f a

theorem ContDiffMoreiraHolderAt.continuousAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E} (h : ContDiffMoreiraHolderAt k α f a) : ContinuousAt f a

theorem ContDiffMoreiraHolderAt.differentiableAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E} (h : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) : DifferentiableAt ℝ f a

@[simp]

theorem ContDiffMoreiraHolderAt.zero_exponent_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {f : E → F} {a : E} : ContDiffMoreiraHolderAt k 0 f a ↔ ContDiffAt ℝ (↑k) f a

theorem ContDiffMoreiraHolderAt.zero_left_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {α : ↑unitInterval} {f : E → F} {a : E} : ContDiffMoreiraHolderAt 0 α f a ↔ ContDiffAt ℝ 0 f a ∧ (fun (x : E) => f x - f a) =O[nhds a] fun (x : E) => ‖x - a‖ ^ ↑α

theorem ContDiffMoreiraHolderAt.of_exponent_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {f : E → F} {a : E} {α β : ↑unitInterval} (hf : ContDiffMoreiraHolderAt k α f a) (hle : β ≤ α) : ContDiffMoreiraHolderAt k β f a

theorem ContDiffMoreiraHolderAt.of_lt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k l : ℕ} {f : E → F} {a : E} {α β : ↑unitInterval} (hf : ContDiffMoreiraHolderAt k α f a) (hlt : l < k) : ContDiffMoreiraHolderAt l β f a

theorem ContDiffMoreiraHolderAt.of_toLex_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k l : ℕ} {f : E → F} {a : E} {α β : ↑unitInterval} (hf : ContDiffMoreiraHolderAt k α f a) (hle : toLex (l, β) ≤ toLex (k, α)) : ContDiffMoreiraHolderAt l β f a

theorem ContDiffMoreiraHolderAt.of_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k l : ℕ} {f : E → F} {a : E} {α : ↑unitInterval} (hf : ContDiffMoreiraHolderAt k α f a) (hl : l ≤ k) : ContDiffMoreiraHolderAt l α f a

theorem ContDiffMoreiraHolderAt.of_contDiffOn_holderWith {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {k : ℕ} {α : ↑unitInterval} {a : E} {C : NNReal} (hf : ContDiffOn ℝ (↑k) f s) (hs : s ∈ nhds a) (hd : HolderOnWith C ⟨↑α, ⋯⟩ (iteratedFDeriv ℝ k f) s) : ContDiffMoreiraHolderAt k α f a

theorem ContDiffMoreiraHolderAt.fst {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {a : E × F} : ContDiffMoreiraHolderAt k α Prod.fst a

theorem ContDiffMoreiraHolderAt.snd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {a : E × F} : ContDiffMoreiraHolderAt k α Prod.snd a

theorem ContDiffMoreiraHolderAt.prodMk {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} {f : E → F} {g : E → G} {a : E} (hf : ContDiffMoreiraHolderAt k α f a) (hg : ContDiffMoreiraHolderAt k α g a) : ContDiffMoreiraHolderAt k α (fun (x : E) => (f x, g x)) a

theorem ContDiffMoreiraHolderAt.comp' {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {g : F → G} {f : E → F} {a : E} {k : ℕ} {α : ↑unitInterval} (hg : ContDiffMoreiraHolderAt k α g (f a)) (hf : ContDiffMoreiraHolderAt k α f a) (hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a) : ContDiffMoreiraHolderAt k α (g ∘ f) a

theorem ContDiffMoreiraHolderAt.comp {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {g : F → G} {f : E → F} {a : E} {k : ℕ} {α : ↑unitInterval} (hg : ContDiffMoreiraHolderAt k α g (f a)) (hf : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) : ContDiffMoreiraHolderAt k α (g ∘ f) a

theorem ContinuousLinearMap.contDiffMoreiraHolderAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E →L[ℝ] F) {a : E} {k : ℕ} {α : ↑unitInterval} : ContDiffMoreiraHolderAt k α (⇑f) a

theorem ContinuousLinearEquiv.contDiffMoreiraHolderAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E ≃L[ℝ] F) {a : E} {k : ℕ} {α : ↑unitInterval} : ContDiffMoreiraHolderAt k α (⇑f) a

theorem ContDiffMoreiraHolderAt.continuousLinearMap_comp {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {a : E} {k : ℕ} {α : ↑unitInterval} (hf : ContDiffMoreiraHolderAt k α f a) (g : F →L[ℝ] G) : ContDiffMoreiraHolderAt k α (⇑g ∘ f) a

@[simp]

theorem ContinuousLinearEquiv.contDiffMoreiraHolderAt_left_comp {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {a : E} {k : ℕ} {α : ↑unitInterval} (g : F ≃L[ℝ] G) : ContDiffMoreiraHolderAt k α (⇑g ∘ f) a ↔ ContDiffMoreiraHolderAt k α f a

@[simp]

theorem LinearIsometryEquiv.contDiffMoreiraHolderAt_left_comp {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {a : E} {k : ℕ} {α : ↑unitInterval} (g : F ≃ₗᵢ[ℝ] G) : ContDiffMoreiraHolderAt k α (⇑g ∘ f) a ↔ ContDiffMoreiraHolderAt k α f a

theorem ContDiffMoreiraHolderAt.id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} {α : ↑unitInterval} {a : E} : ContDiffMoreiraHolderAt k α id a

theorem ContDiffMoreiraHolderAt.const {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {a : E} {b : F} : ContDiffMoreiraHolderAt k α (Function.const E b) a

theorem ContDiffMoreiraHolderAt.fderiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {a : E} {k l : ℕ} {α : ↑unitInterval} (hf : ContDiffMoreiraHolderAt k α f a) (hl : l + 1 ≤ k) : ContDiffMoreiraHolderAt l α (fderiv ℝ f) a

theorem ContDiffMoreiraHolderAt.iteratedFDeriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {a : E} {k l m : ℕ} {α : ↑unitInterval} (hf : ContDiffMoreiraHolderAt k α f a) (hl : l + m ≤ k) : ContDiffMoreiraHolderAt l α (iteratedFDeriv ℝ m f) a

theorem ContDiffMoreiraHolderAt.congr_eventuallyEq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : E → F} {a : E} {k : ℕ} {α : ↑unitInterval} (hf : ContDiffMoreiraHolderAt k α f a) (hfg : f =ᶠ[nhds a] g) : ContDiffMoreiraHolderAt k α g a

theorem OpenPartialHomeomorph.contDiffMoreiraHolderAt_symm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace E] {k : ℕ} {α : ↑unitInterval} (f : OpenPartialHomeomorph E F) {a : F} (ha : a ∈ f.target) (hf' : (fderiv ℝ (↑f) (↑f.symm a)).IsInvertible) (hf : ContDiffMoreiraHolderAt k α (↑f) (↑f.symm a)) : ContDiffMoreiraHolderAt k α (↑f.symm) a