Skip to content

Commit

Permalink
Fix
Browse files Browse the repository at this point in the history
  • Loading branch information
@urkud
urkud committed Jan 3, 2025
1 parent 13bf522 commit 7be0b06
Show file tree
Hide file tree
Showing 21 changed files with 85 additions and 93 deletions.
12 changes: 6 additions & 6 deletions Mathlib/Analysis/Analytic/IteratedFDeriv.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -207,7 +207,7 @@ theorem HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum
(h : HasFPowerSeriesOnBall f p x r) (h' : AnalyticOn 𝕜 f univ) {n : ℕ} (v : Fin n → E) :
iteratedFDeriv 𝕜 n f x v = ∑ σ : Perm (Fin n), p n (fun i ↦ v (σ i)) := by
simp only [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊢
exact h.iteratedFDerivWithin_eq_sum h' uniqueDiffOn_univ (mem_univ x) v
exact h.iteratedFDerivWithin_eq_sum h' .univ (mem_univ x) v

/-- If a function has a power series in a ball, then its `n`-th iterated derivative is given by
`(v₁, ..., vₙ) ↦ ∑ pₙ (v_{σ (1)}, ..., v_{σ (n)})` where the sum is over all
Expand All @@ -224,7 +224,7 @@ theorem HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_completeSpace
· exact h.mono inter_subset_left
· apply h.analyticOn.mono
rw [insert_eq_of_mem hx]
· exact hs.inter EMetric.isOpen_ball
· exact hs.inter_isOpen EMetric.isOpen_ball
· exact ⟨hx, EMetric.mem_ball_self h.r_pos⟩
· exact inter_subset_right

Expand All @@ -235,7 +235,7 @@ theorem HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum_of_completeSpace [CompleteSp
(h : HasFPowerSeriesOnBall f p x r) {n : ℕ} (v : Fin n → E) :
iteratedFDeriv 𝕜 n f x v = ∑ σ : Perm (Fin n), p n (fun i ↦ v (σ i)) := by
simp only [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊢
exact h.iteratedFDerivWithin_eq_sum_of_completeSpace uniqueDiffOn_univ (mem_univ _) v
exact h.iteratedFDerivWithin_eq_sum_of_completeSpace .univ (mem_univ _) v

/-- The `n`-th iterated derivative of an analytic function on a set is symmetric. -/
theorem AnalyticOn.iteratedFDerivWithin_comp_perm
Expand All @@ -257,18 +257,18 @@ theorem ContDiffWithinAt.iteratedFDerivWithin_comp_perm
have : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x :=
iteratedFDerivWithin_inter_open u_open xu
rw [← this]
exact AnalyticOn.iteratedFDerivWithin_comp_perm hu.analyticOn (hs.inter u_open) ⟨hx, xu⟩ _ _
exact hu.analyticOn.iteratedFDerivWithin_comp_perm (hs.inter_isOpen u_open) ⟨hx, xu⟩ _ _

/-- The `n`-th iterated derivative of an analytic function is symmetric. -/
theorem AnalyticOn.iteratedFDeriv_comp_perm
(h : AnalyticOn 𝕜 f univ) {n : ℕ} (v : Fin n → E) (σ : Perm (Fin n)) :
iteratedFDeriv 𝕜 n f x (v ∘ σ) = iteratedFDeriv 𝕜 n f x v := by
rw [← iteratedFDerivWithin_univ]
exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _
exact h.iteratedFDerivWithin_comp_perm .univ (mem_univ x) _ _

/-- The `n`-th iterated derivative of an analytic function is symmetric. -/
theorem ContDiffAt.iteratedFDeriv_comp_perm
(h : ContDiffAt 𝕜 ω f x) {n : ℕ} (v : Fin n → E) (σ : Perm (Fin n)) :
iteratedFDeriv 𝕜 n f x (v ∘ σ) = iteratedFDeriv 𝕜 n f x v := by
rw [← iteratedFDerivWithin_univ]
exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _
exact h.iteratedFDerivWithin_comp_perm .univ (mem_univ x) _ _
26 changes: 13 additions & 13 deletions Mathlib/Analysis/Calculus/ContDiff/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -222,7 +222,7 @@ theorem ContinuousLinearMap.iteratedFDeriv_comp_left {f : E → F} (g : F →L[
(hf : ContDiff 𝕜 n f) (x : E) {i : ℕ} (hi : i ≤ n) :
iteratedFDeriv 𝕜 i (g ∘ f) x = g.compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f x) := by
simp only [← iteratedFDerivWithin_univ]
exact g.iteratedFDerivWithin_comp_left hf.contDiffOn uniqueDiffOn_univ (mem_univ x) hi
exact g.iteratedFDerivWithin_comp_left hf.contDiffOn .univ (mem_univ x) hi

/-- The iterated derivative within a set of the composition with a linear equiv on the left is
obtained by applying the linear equiv to the iterated derivative. This is true without
Expand Down Expand Up @@ -266,7 +266,7 @@ theorem LinearIsometry.norm_iteratedFDeriv_comp_left {f : E → F} (g : F →ₗ
(hf : ContDiff 𝕜 n f) (x : E) {i : ℕ} (hi : i ≤ n) :
‖iteratedFDeriv 𝕜 i (g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖ := by
simp only [← iteratedFDerivWithin_univ]
exact g.norm_iteratedFDerivWithin_comp_left hf.contDiffOn uniqueDiffOn_univ (mem_univ x) hi
exact g.norm_iteratedFDerivWithin_comp_left hf.contDiffOn .univ (mem_univ x) hi

/-- Composition with a linear isometry equiv on the left preserves the norm of the iterated
derivative within a set. -/
Expand All @@ -285,7 +285,7 @@ derivative. -/
theorem LinearIsometryEquiv.norm_iteratedFDeriv_comp_left (g : F ≃ₗᵢ[𝕜] G) (f : E → F) (x : E)
(i : ℕ) : ‖iteratedFDeriv 𝕜 i (g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖ := by
rw [← iteratedFDerivWithin_univ, ← iteratedFDerivWithin_univ]
apply g.norm_iteratedFDerivWithin_comp_left f uniqueDiffOn_univ (mem_univ x) i
apply g.norm_iteratedFDerivWithin_comp_left f .univ (mem_univ x) i

/-- Composition by continuous linear equivs on the left respects higher differentiability at a
point in a domain. -/
Expand Down Expand Up @@ -412,7 +412,7 @@ theorem ContinuousLinearMap.iteratedFDeriv_comp_right (g : G →L[𝕜] E) {f :
iteratedFDeriv 𝕜 i (f ∘ g) x =
(iteratedFDeriv 𝕜 i f (g x)).compContinuousLinearMap fun _ => g := by
simp only [← iteratedFDerivWithin_univ]
exact g.iteratedFDerivWithin_comp_right hf.contDiffOn uniqueDiffOn_univ uniqueDiffOn_univ
exact g.iteratedFDerivWithin_comp_right hf.contDiffOn .univ .univ
(mem_univ _) hi

/-- Composition with a linear isometry on the right preserves the norm of the iterated derivative
Expand All @@ -430,7 +430,7 @@ within a set. -/
theorem LinearIsometryEquiv.norm_iteratedFDeriv_comp_right (g : G ≃ₗᵢ[𝕜] E) (f : E → F) (x : G)
(i : ℕ) : ‖iteratedFDeriv 𝕜 i (f ∘ g) x‖ = ‖iteratedFDeriv 𝕜 i f (g x)‖ := by
simp only [← iteratedFDerivWithin_univ]
apply g.norm_iteratedFDerivWithin_comp_right f uniqueDiffOn_univ (mem_univ (g x)) i
apply g.norm_iteratedFDerivWithin_comp_right f .univ (mem_univ (g x)) i

/-- Composition by continuous linear equivs on the right respects higher differentiability at a
point in a domain. -/
Expand Down Expand Up @@ -950,7 +950,7 @@ theorem iteratedFDeriv_clm_apply_const_apply
{i : ℕ} (hi : i ≤ n) {x : E} {u : F} {m : Fin i → E} :
(iteratedFDeriv 𝕜 i (fun y ↦ (c y) u) x) m = (iteratedFDeriv 𝕜 i c x) m u := by
simp only [← iteratedFDerivWithin_univ]
exact iteratedFDerivWithin_clm_apply_const_apply uniqueDiffOn_univ hc.contDiffOn hi (mem_univ _)
exact iteratedFDerivWithin_clm_apply_const_apply .univ hc.contDiffOn hi (mem_univ _)

end ClmApplyConst

Expand Down Expand Up @@ -1109,7 +1109,7 @@ protected theorem ContDiffAt.fderiv {f : E → F → G} {g : E → F}
(hf : ContDiffAt 𝕜 n (Function.uncurry f) (x₀, g x₀)) (hg : ContDiffAt 𝕜 m g x₀)
(hmn : m + 1 ≤ n) : ContDiffAt 𝕜 m (fun x => fderiv 𝕜 (f x) (g x)) x₀ := by
simp_rw [← fderivWithin_univ]
refine (ContDiffWithinAt.fderivWithin hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ
refine (ContDiffWithinAt.fderivWithin hf.contDiffWithinAt hg.contDiffWithinAt .univ
hmn (mem_univ x₀) ?_).contDiffAt univ_mem
rw [preimage_univ]

Expand All @@ -1121,7 +1121,7 @@ theorem ContDiffAt.fderiv_right (hf : ContDiffAt 𝕜 n f x₀) (hmn : m + 1 ≤
theorem ContDiffAt.iteratedFDeriv_right {i : ℕ} (hf : ContDiffAt 𝕜 n f x₀)
(hmn : m + i ≤ n) : ContDiffAt 𝕜 m (iteratedFDeriv 𝕜 i f) x₀ := by
rw [← iteratedFDerivWithin_univ, ← contDiffWithinAt_univ] at *
exact hf.iteratedFderivWithin_right uniqueDiffOn_univ hmn trivial
exact hf.iteratedFderivWithin_right .univ hmn trivial

/-- `x ↦ fderiv 𝕜 (f x) (g x)` is smooth. -/
protected theorem ContDiff.fderiv {f : E → F → G} {g : E → F}
Expand Down Expand Up @@ -1169,7 +1169,7 @@ theorem ContDiff.contDiff_fderiv_apply {f : E → F} (hf : ContDiff 𝕜 n f) (h
ContDiff 𝕜 m fun p : E × E => (fderiv 𝕜 f p.1 : E →L[𝕜] F) p.2 := by
rw [← contDiffOn_univ] at hf ⊢
rw [← fderivWithin_univ, ← univ_prod_univ]
exact contDiffOn_fderivWithin_apply hf uniqueDiffOn_univ hmn
exact contDiffOn_fderivWithin_apply hf .univ hmn

/-!
### Smoothness of functions `f : E → Π i, F' i`
Expand Down Expand Up @@ -1320,7 +1320,7 @@ theorem iteratedFDerivWithin_add_apply' {f g : E → F} (hf : ContDiffOn 𝕜 i
theorem iteratedFDeriv_add_apply {i : ℕ} {f g : E → F} (hf : ContDiff 𝕜 i f) (hg : ContDiff 𝕜 i g) :
iteratedFDeriv 𝕜 i (f + g) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x := by
simp_rw [← contDiffOn_univ, ← iteratedFDerivWithin_univ] at hf hg ⊢
exact iteratedFDerivWithin_add_apply hf hg uniqueDiffOn_univ (Set.mem_univ _)
exact iteratedFDerivWithin_add_apply hf hg .univ (Set.mem_univ _)

theorem iteratedFDeriv_add_apply' {i : ℕ} {f g : E → F} (hf : ContDiff 𝕜 i f)
(hg : ContDiff 𝕜 i g) :
Expand Down Expand Up @@ -1377,7 +1377,7 @@ theorem iteratedFDerivWithin_neg_apply {f : E → F} (hu : UniqueDiffOn 𝕜 s)
theorem iteratedFDeriv_neg_apply {i : ℕ} {f : E → F} :
iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x := by
simp_rw [← iteratedFDerivWithin_univ]
exact iteratedFDerivWithin_neg_apply uniqueDiffOn_univ (Set.mem_univ _)
exact iteratedFDerivWithin_neg_apply .univ (Set.mem_univ _)

end Neg

Expand Down Expand Up @@ -1443,7 +1443,7 @@ theorem iteratedFDeriv_sum {ι : Type*} {f : ι → E → F} {u : Finset ι} {i
(h : ∀ j ∈ u, ContDiff 𝕜 i (f j)) :
iteratedFDeriv 𝕜 i (∑ j ∈ u, f j ·) = ∑ j ∈ u, iteratedFDeriv 𝕜 i (f j) :=
funext fun x ↦ by simpa [iteratedFDerivWithin_univ] using
iteratedFDerivWithin_sum_apply uniqueDiffOn_univ (mem_univ x) fun j hj ↦ (h j hj).contDiffOn
iteratedFDerivWithin_sum_apply .univ (mem_univ x) fun j hj ↦ (h j hj).contDiffOn

/-! ### Product of two functions -/

Expand Down Expand Up @@ -1619,7 +1619,7 @@ theorem iteratedFDerivWithin_const_smul_apply (hf : ContDiffOn 𝕜 i f s) (hu :
theorem iteratedFDeriv_const_smul_apply {x : E} (hf : ContDiff 𝕜 i f) :
iteratedFDeriv 𝕜 i (a • f) x = a • iteratedFDeriv 𝕜 i f x := by
simp_rw [← contDiffOn_univ, ← iteratedFDerivWithin_univ] at *
exact iteratedFDerivWithin_const_smul_apply hf uniqueDiffOn_univ (Set.mem_univ _)
exact iteratedFDerivWithin_const_smul_apply hf .univ (Set.mem_univ _)

theorem iteratedFDeriv_const_smul_apply' {x : E} (hf : ContDiff 𝕜 i f) :
iteratedFDeriv 𝕜 i (fun x ↦ a • f x) x = a • iteratedFDeriv 𝕜 i f x :=
Expand Down
20 changes: 8 additions & 12 deletions Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -210,8 +210,7 @@ theorem ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear (B : E →L[𝕜]
‖iteratedFDeriv 𝕜 n (fun y => B (f y) (g y)) x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1),
(n.choose i : ℝ) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖ := by
simp_rw [← iteratedFDerivWithin_univ]
exact B.norm_iteratedFDerivWithin_le_of_bilinear hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ
(mem_univ x) hn
exact B.norm_iteratedFDerivWithin_le_of_bilinear hf.contDiffOn hg.contDiffOn .univ (mem_univ x) hn

/-- Bounding the norm of the iterated derivative of `B (f x) (g x)` within a set in terms of the
iterated derivatives of `f` and `g` when `B` is bilinear of norm at most `1`:
Expand All @@ -236,7 +235,7 @@ theorem ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one (B : E
(n.choose i : ℝ) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖ := by
simp_rw [← iteratedFDerivWithin_univ]
exact B.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one hf.contDiffOn hg.contDiffOn
uniqueDiffOn_univ (mem_univ x) hn hB
.univ (mem_univ x) hn hB

section

Expand Down Expand Up @@ -282,7 +281,7 @@ theorem norm_iteratedFDeriv_mul_le {f : E → A} {g : E → A} {N : WithTop ℕ
(n.choose i : ℝ) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖ := by
simp_rw [← iteratedFDerivWithin_univ]
exact norm_iteratedFDerivWithin_mul_le
hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ (mem_univ x) hn
hf.contDiffOn hg.contDiffOn .univ (mem_univ x) hn

-- TODO: Add `norm_iteratedFDeriv[Within]_list_prod_le` for non-commutative `NormedRing A`.

Expand Down Expand Up @@ -337,8 +336,7 @@ theorem norm_iteratedFDeriv_prod_le [DecidableEq ι] [NormOneClass A'] {u : Fins
∑ p ∈ u.sym n, (p : Multiset ι).multinomial *
∏ j ∈ u, ‖iteratedFDeriv 𝕜 ((p : Multiset ι).count j) (f j) x‖ := by
simpa [iteratedFDerivWithin_univ] using
norm_iteratedFDerivWithin_prod_le (fun i hi ↦ (hf i hi).contDiffOn) uniqueDiffOn_univ
(mem_univ x) hn
norm_iteratedFDerivWithin_prod_le (fun i hi ↦ (hf i hi).contDiffOn) .univ (mem_univ x) hn

end

Expand Down Expand Up @@ -518,8 +516,8 @@ theorem norm_iteratedFDeriv_comp_le {g : F → G} {f : E → F} {n : ℕ} {N : W
(hD : ∀ i, 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i) :
‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ n ! * C * D ^ n := by
simp_rw [← iteratedFDerivWithin_univ] at hC hD ⊢
exact norm_iteratedFDerivWithin_comp_le hg.contDiffOn hf.contDiffOn hn uniqueDiffOn_univ
uniqueDiffOn_univ (mapsTo_univ _ _) (mem_univ x) hC hD
exact norm_iteratedFDerivWithin_comp_le hg.contDiffOn hf.contDiffOn hn .univ .univ
(mapsTo_univ _ _) (mem_univ x) hC hD

section Apply

Expand All @@ -542,8 +540,7 @@ theorem norm_iteratedFDeriv_clm_apply {f : E → F →L[𝕜] G} {g : E → F} {
‖iteratedFDeriv 𝕜 n (fun y : E => (f y) (g y)) x‖ ≤ ∑ i ∈ Finset.range (n + 1),
↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖ := by
simp only [← iteratedFDerivWithin_univ]
exact norm_iteratedFDerivWithin_clm_apply hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ
(Set.mem_univ x) hn
exact norm_iteratedFDerivWithin_clm_apply hf.contDiffOn hg.contDiffOn .univ (Set.mem_univ x) hn

theorem norm_iteratedFDerivWithin_clm_apply_const {f : E → F →L[𝕜] G} {c : F} {s : Set E} {x : E}
{N : WithTop ℕ∞} {n : ℕ} (hf : ContDiffOn 𝕜 N f s) (hs : UniqueDiffOn 𝕜 s)
Expand All @@ -562,7 +559,6 @@ theorem norm_iteratedFDeriv_clm_apply_const {f : E → F →L[𝕜] G} {c : F} {
{N : WithTop ℕ∞} {n : ℕ} (hf : ContDiff 𝕜 N f) (hn : n ≤ N) :
‖iteratedFDeriv 𝕜 n (fun y : E => (f y) c) x‖ ≤ ‖c‖ * ‖iteratedFDeriv 𝕜 n f x‖ := by
simp only [← iteratedFDerivWithin_univ]
exact norm_iteratedFDerivWithin_clm_apply_const hf.contDiffOn uniqueDiffOn_univ
(Set.mem_univ x) hn
exact norm_iteratedFDerivWithin_clm_apply_const hf.contDiffOn .univ (Set.mem_univ x) hn

end Apply
Loading

0 comments on commit 7be0b06

Please sign in to comment.