Commit 2023-06-13 22:07 9b2617a8

View on Github →

feat: port Analysis.Analytic.Composition (#4572)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Analytic/Composition.lean

added theorem AnalyticAt.comp

added theorem Composition.blocksFun_sigmaCompositionAux

added def Composition.gather

added theorem Composition.length_gather

added theorem Composition.length_sigmaCompositionAux

added def Composition.sigmaCompositionAux

added def Composition.sigmaEquivSigmaPi

added theorem Composition.sigma_composition_eq_iff

added theorem Composition.sigma_pi_composition_eq_iff

added theorem Composition.sizeUpTo_sizeUpTo_add

added def ContinuousMultilinearMap.compAlongComposition

added theorem ContinuousMultilinearMap.compAlongComposition_apply

added def FormalMultilinearSeries.applyComposition

added theorem FormalMultilinearSeries.applyComposition_ones

added theorem FormalMultilinearSeries.applyComposition_single

added theorem FormalMultilinearSeries.applyComposition_update

added def FormalMultilinearSeries.compAlongComposition

added theorem FormalMultilinearSeries.compAlongComposition_apply

added theorem FormalMultilinearSeries.compAlongComposition_bound

added theorem FormalMultilinearSeries.compAlongComposition_nnnorm

added theorem FormalMultilinearSeries.compAlongComposition_norm

added def FormalMultilinearSeries.compChangeOfVariables

added theorem FormalMultilinearSeries.compChangeOfVariables_blocksFun

added theorem FormalMultilinearSeries.compChangeOfVariables_length

added theorem FormalMultilinearSeries.compChangeOfVariables_sum

added theorem FormalMultilinearSeries.compContinuousLinearMap_applyComposition

added def FormalMultilinearSeries.compPartialSumSource

added def FormalMultilinearSeries.compPartialSumTarget

added def FormalMultilinearSeries.compPartialSumTargetSet

added theorem FormalMultilinearSeries.compPartialSumTargetSet_image_compPartialSumSource

added theorem FormalMultilinearSeries.compPartialSumTarget_tendsto_atTop

added theorem FormalMultilinearSeries.comp_assoc

added theorem FormalMultilinearSeries.comp_coeff_one

added theorem FormalMultilinearSeries.comp_coeff_zero''

added theorem FormalMultilinearSeries.comp_coeff_zero'

added theorem FormalMultilinearSeries.comp_coeff_zero

added theorem FormalMultilinearSeries.comp_id

added theorem FormalMultilinearSeries.comp_partialSum

added theorem FormalMultilinearSeries.comp_removeZero

added theorem FormalMultilinearSeries.comp_summable_nnreal

added def FormalMultilinearSeries.id

added theorem FormalMultilinearSeries.id_apply_ne_one

added theorem FormalMultilinearSeries.id_apply_one'

added theorem FormalMultilinearSeries.id_apply_one

added theorem FormalMultilinearSeries.id_comp

added theorem FormalMultilinearSeries.le_comp_radius_of_summable

added theorem FormalMultilinearSeries.mem_compPartialSumSource_iff

added theorem FormalMultilinearSeries.mem_compPartialSumTarget_iff

added theorem FormalMultilinearSeries.removeZero_applyComposition

added theorem FormalMultilinearSeries.removeZero_comp_of_pos

added theorem HasFPowerSeriesAt.comp

Modified Mathlib/Combinatorics/Composition.lean

added theorem List.get_splitWrtComposition