Commit 2023-06-19 04:18 c10de4a0

View on Github →

feat: port Analysis.SchwartzSpace (#4762)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SchwartzSpace.lean

added theorem Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux

added def Function.HasTemperateGrowth

added theorem SchwartzMap.add_apply

added def SchwartzMap.bilinLeftCLM

added theorem SchwartzMap.bounds_bddBelow

added theorem SchwartzMap.bounds_nonempty

added theorem SchwartzMap.coeFn_zero

added def SchwartzMap.coeHom

added theorem SchwartzMap.coeHom_injective

added theorem SchwartzMap.coe_coeHom

added theorem SchwartzMap.coe_zero

added def SchwartzMap.compCLM

added theorem SchwartzMap.decay

added theorem SchwartzMap.decay_add_le_aux

added theorem SchwartzMap.decay_neg_aux

added theorem SchwartzMap.decay_smul_aux

added def SchwartzMap.delta

added theorem SchwartzMap.delta_apply

added def SchwartzMap.derivCLM

added theorem SchwartzMap.derivCLM_apply

added theorem SchwartzMap.ext

added def SchwartzMap.fderivCLM

added theorem SchwartzMap.fderivCLM_apply

added theorem SchwartzMap.isBigO_cocompact_rpow

added theorem SchwartzMap.isBigO_cocompact_zpow

added theorem SchwartzMap.isBigO_cocompact_zpow_neg_nat

added def SchwartzMap.iteratedPDeriv

added theorem SchwartzMap.iteratedPDeriv_one

added theorem SchwartzMap.iteratedPDeriv_succ_left

added theorem SchwartzMap.iteratedPDeriv_succ_right

added theorem SchwartzMap.iteratedPDeriv_zero

added theorem SchwartzMap.le_seminorm'

added theorem SchwartzMap.le_seminorm

added theorem SchwartzMap.le_seminormAux

added def SchwartzMap.mkCLM

added def SchwartzMap.mkLM

added theorem SchwartzMap.norm_iteratedFDeriv_le_seminorm

added theorem SchwartzMap.norm_le_seminorm

added theorem SchwartzMap.norm_pow_mul_le_seminorm

added theorem SchwartzMap.one_add_le_sup_seminorm_apply

added def SchwartzMap.pderivCLM

added theorem SchwartzMap.pderivCLM_apply

added theorem SchwartzMap.schwartzSeminormFamily_apply

added theorem SchwartzMap.schwartzSeminormFamily_apply_zero

added theorem SchwartzMap.seminormAux_add_le

added theorem SchwartzMap.seminormAux_le_bound

added theorem SchwartzMap.seminormAux_nonneg

added theorem SchwartzMap.seminormAux_smul_le

added theorem SchwartzMap.seminormAux_zero

added theorem SchwartzMap.seminorm_le_bound'

added theorem SchwartzMap.seminorm_le_bound

added theorem SchwartzMap.smooth

added theorem SchwartzMap.smul_apply

added theorem SchwartzMap.sub_apply

added def SchwartzMap.toBoundedContinuousFunction

added def SchwartzMap.toBoundedContinuousFunctionCLM

added theorem SchwartzMap.toBoundedContinuousFunctionCLM_apply

added def SchwartzMap.toBoundedContinuousFunctionLM

added theorem SchwartzMap.toBoundedContinuousFunctionLM_apply

added theorem SchwartzMap.toBoundedContinuousFunction_apply

added def SchwartzMap.toContinuousMap

added theorem SchwartzMap.zero_apply

added structure SchwartzMap

added def schwartzSeminormFamily

added theorem schwartz_withSeminorms