[Merged by Bors] - feat(Analysis/Analytic): some more API for analytic functions #7552
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
loefflerd
commented
Oct 6, 2023
Comment on lines
-60
to
-65
| @[simp] -- porting note: new; was not needed in Lean 3 | ||
| theorem zero_apply (n : ℕ) : (0 : FormalMultilinearSeries 𝕜 E F) n = 0 := rfl | ||
|
|
||
| @[simp] -- porting note: new; was not needed in Lean 3 | ||
| theorem neg_apply (f : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : (-f) n = - f n := rfl | ||
|
|
There was a problem hiding this comment.
I moved these simp lemmas inside the FormalMultilinearSeries namespace (where I think they really belong).
loefflerd
commented
Oct 6, 2023
Comment on lines
+351
to
+386
|
|
||
| section Linear | ||
|
|
||
| variable [NontriviallyNormedField 𝕜] | ||
| [NormedAddCommGroup E] [NormedSpace 𝕜 E] | ||
| [NormedAddCommGroup F] [NormedSpace 𝕜 F] | ||
|
|
||
| namespace ContinuousLinearMap | ||
|
|
||
| /-- Formal power series of a continuous linear map `f : E →L[𝕜] F` at `x : E`: | ||
| `f y = f x + f (y - x)`. -/ | ||
| def fpowerSeries (f : E →L[𝕜] F) (x : E) : FormalMultilinearSeries 𝕜 E F | ||
| | 0 => ContinuousMultilinearMap.curry0 𝕜 _ (f x) | ||
| | 1 => (continuousMultilinearCurryFin1 𝕜 E F).symm f | ||
| | _ => 0 | ||
| #align continuous_linear_map.fpower_series ContinuousLinearMap.fpowerSeries | ||
|
|
||
| theorem fpower_series_apply_zero (f : E →L[𝕜] F) (x : E) : | ||
| f.fpowerSeries x 0 = ContinuousMultilinearMap.curry0 𝕜 _ (f x) := | ||
| rfl | ||
|
|
||
| theorem fpower_series_apply_one (f : E →L[𝕜] F) (x : E) : | ||
| f.fpowerSeries x 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm f := | ||
| rfl | ||
|
|
||
| theorem fpowerSeries_apply_add_two (f : E →L[𝕜] F) (x : E) (n : ℕ) : f.fpowerSeries x (n + 2) = 0 := | ||
| rfl | ||
| #align continuous_linear_map.fpower_series_apply_add_two ContinuousLinearMap.fpowerSeries_apply_add_two | ||
|
|
||
| attribute | ||
| [eqns fpower_series_apply_zero fpower_series_apply_one fpowerSeries_apply_add_two] fpowerSeries | ||
| attribute [simp] fpowerSeries | ||
|
|
||
| end ContinuousLinearMap | ||
|
|
||
| end Linear |
There was a problem hiding this comment.
This material is moved (verbatim) from Analytic/Linear.lean (it seems to belong better here since it is purely algebraic, without mentioning radius of convergence, and the other file is very very long).
loefflerd
commented
Oct 6, 2023
Comment on lines
-30
to
-53
| /-- Formal power series of a continuous linear map `f : E →L[𝕜] F` at `x : E`: | ||
| `f y = f x + f (y - x)`. -/ | ||
| def fpowerSeries (f : E →L[𝕜] F) (x : E) : FormalMultilinearSeries 𝕜 E F | ||
| | 0 => ContinuousMultilinearMap.curry0 𝕜 _ (f x) | ||
| | 1 => (continuousMultilinearCurryFin1 𝕜 E F).symm f | ||
| | _ => 0 | ||
| #align continuous_linear_map.fpower_series ContinuousLinearMap.fpowerSeries | ||
|
|
||
| theorem fpower_series_apply_zero (f : E →L[𝕜] F) (x : E) : | ||
| f.fpowerSeries x 0 = ContinuousMultilinearMap.curry0 𝕜 _ (f x) := | ||
| rfl | ||
|
|
||
| theorem fpower_series_apply_one (f : E →L[𝕜] F) (x : E) : | ||
| f.fpowerSeries x 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm f := | ||
| rfl | ||
|
|
||
| theorem fpowerSeries_apply_add_two (f : E →L[𝕜] F) (x : E) (n : ℕ) : f.fpowerSeries x (n + 2) = 0 := | ||
| rfl | ||
| #align continuous_linear_map.fpower_series_apply_add_two ContinuousLinearMap.fpowerSeries_apply_add_two | ||
|
|
||
| attribute | ||
| [eqns fpower_series_apply_zero fpower_series_apply_one fpowerSeries_apply_add_two] fpowerSeries | ||
| attribute [simp] fpowerSeries | ||
|
|
There was a problem hiding this comment.
I moved this to FormalMultlinearSeries.lean (it is purely algebraic so it seems to belong better there)
loefflerd
commented
Oct 6, 2023
Comment on lines
+367
to
+394
| /-- The radius of the Cartesian product of two formal series is the minimum of their radii. --/ | ||
| lemma radius_prod_eq_min | ||
| (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 E G) : | ||
| (p.prod q).radius = min p.radius q.radius := by | ||
| apply le_antisymm | ||
| · refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_ | ||
| rw [le_min_iff] | ||
| have := (p.prod q).isLittleO_one_of_lt_radius hr | ||
| constructor | ||
| all_goals { -- kludge, there is no "work_on_goal" in Lean 4? | ||
| apply FormalMultilinearSeries.le_radius_of_isBigO | ||
| refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO | ||
| rw [norm_mul, norm_norm, norm_mul, norm_norm] | ||
| refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _) | ||
| rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.op_norm_prod] | ||
| try apply le_max_left | ||
| try apply le_max_right } | ||
| · refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_ | ||
| rw [lt_min_iff] at hr | ||
| have := ((p.isLittleO_one_of_lt_radius hr.1).add | ||
| (q.isLittleO_one_of_lt_radius hr.2)).isBigO | ||
| refine (p.prod q).le_radius_of_isBigO ((isBigO_of_le _ λ n ↦ ?_).trans this) | ||
| rw [norm_mul, norm_norm, ←add_mul, norm_mul] | ||
| refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _) | ||
| rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.op_norm_prod] | ||
| refine (max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)).trans ?_ | ||
| apply Real.le_norm_self | ||
|
|
There was a problem hiding this comment.
This proof and the next are a bit convoluted, but I couldn't find a nicer way of doing it.
loefflerd
added
the
awaiting-review
jcommelin
reviewed
Oct 18, 2023
Co-authored-by: Johan Commelin <johan@commelin.net>
|
Thanks for the review! |
|
The previous CI run failed because of the (unrelated, sporadic) lean4checker ReduceBool glitch. I've merged master to force a new CI cycle. |
|
Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Oct 18, 2023
This PR adds some basic results about analytic functions: products of analytic functions are analytic, and the inverse map on a normed field is analytic away from 0.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds some basic results about analytic functions: products of analytic functions are analytic, and the inverse map on a normed field is analytic away from 0.