Commit 2024-11-09 07:31 905613cc

View on Github →

feat: improve the Analysis.Analytic.OfScalars API and implement it for geometric and exponential functions (#18407) Following PR #17455, in which the ofScalars API was defined, this PR cleans up the file, fixes typos, adds additional infrastructure and implements the API in Analysis.Normed.Algebra.Exponential and Analysis.Analytic.Constructions.

Estimated changes

Modified Mathlib/Analysis/Analytic/Constructions.lean

added theorem formalMultilinearSeries_geometric_eq_ofScalars

Modified Mathlib/Analysis/Analytic/OfScalars.lean

modified def FormalMultilinearSeries.ofScalars

added def FormalMultilinearSeries.ofScalarsSubmodule

added theorem FormalMultilinearSeries.ofScalarsSum_of_subsingleton

added theorem FormalMultilinearSeries.ofScalarsSum_op

added theorem FormalMultilinearSeries.ofScalarsSum_unop

added theorem FormalMultilinearSeries.ofScalarsSum_zero

added theorem FormalMultilinearSeries.ofScalars_add

added theorem FormalMultilinearSeries.ofScalars_apply_zero

added theorem FormalMultilinearSeries.ofScalars_eq_zero_of_scalar_zero

deleted theorem FormalMultilinearSeries.ofScalars_op

modified theorem FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto

added theorem FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto_ENNReal

added theorem FormalMultilinearSeries.ofScalars_radius_eq_top_of_tendsto

added theorem FormalMultilinearSeries.ofScalars_radius_eq_zero_of_tendsto

added theorem FormalMultilinearSeries.ofScalars_radius_ge_inv_of_tendsto

added theorem FormalMultilinearSeries.ofScalars_series_eq_iff

added theorem FormalMultilinearSeries.ofScalars_series_eq_zero

added theorem FormalMultilinearSeries.ofScalars_series_eq_zero_of_scalar_zero

added theorem FormalMultilinearSeries.ofScalars_series_injective

added theorem FormalMultilinearSeries.ofScalars_series_of_subsingleton

added theorem FormalMultilinearSeries.ofScalars_smul

deleted theorem FormalMultilinearSeries.ofScalars_unop

Modified Mathlib/Analysis/Normed/Algebra/Exponential.lean

added theorem NormedSpace.expSeries_eq_ofScalars

added theorem NormedSpace.exp_eq_ofScalarsSum