Commit 2023-03-09 06:58 2f773887

View on Github →

feat: port Analysis.Normed.Group.Basic (#2736)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Group/Basic.lean

added theorem AntilipschitzWith.le_mul_norm_div

added theorem AntilipschitzWith.mul_div_lipschitzWith

added theorem AntilipschitzWith.mul_lipschitzWith

added theorem Continuous.bounded_above_of_compact_support

added theorem Continuous.nnnorm'

added theorem Continuous.norm'

added theorem ContinuousAt.nnnorm'

added theorem ContinuousAt.norm'

added theorem ContinuousOn.nnnorm'

added theorem ContinuousOn.norm'

added theorem ContinuousWithinAt.nnnorm'

added theorem ContinuousWithinAt.norm'

added theorem Filter.Tendsto.nnnorm'

added theorem Filter.Tendsto.norm'

added theorem Filter.Tendsto.op_one_isBoundedUnder_le'

added theorem Filter.Tendsto.op_one_isBoundedUnder_le

added theorem Filter.tendsto_inv_cobounded

added def GroupNorm.toNormedCommGroup

added def GroupNorm.toNormedGroup

added def GroupSeminorm.toSeminormedCommGroup

added def GroupSeminorm.toSeminormedGroup

added theorem HasCompactMulSupport.exists_pos_le_norm

added theorem Int.abs_le_floor_nnreal_iff

added theorem Int.norm_cast_rat

added theorem Int.norm_cast_real

added theorem Int.norm_coe_nat

added theorem Int.norm_eq_abs

added theorem IsCompact.exists_bound_of_continuous_on'

added theorem Isometry.norm_map_of_map_one

added theorem LipschitzOnWith.norm_div_le_of_le

added theorem LipschitzWith.div

added theorem LipschitzWith.inv

added theorem LipschitzWith.mul'

added theorem LipschitzWith.norm_div_le_of_le

added theorem Metric.Bounded.exists_pos_norm_le'

added theorem MonoidHomClass.antilipschitz_of_bound

added theorem MonoidHomClass.bound_of_antilipschitz

added theorem MonoidHomClass.continuous_of_bound

added theorem MonoidHomClass.isometry_iff_norm

added theorem MonoidHomClass.lipschitz_of_bound

added theorem MonoidHomClass.lipschitz_of_bound_nnnorm

added theorem MonoidHomClass.uniformContinuous_of_bound

added theorem MulOpposite.nnnorm_op

added theorem MulOpposite.nnnorm_unop

added theorem MulOpposite.norm_op

added theorem MulOpposite.norm_unop

added theorem NNReal.coe_natAbs

added theorem NormedCommGroup.cauchySeq_iff

added def NormedCommGroup.induced

added theorem NormedCommGroup.nhds_basis_norm_lt

added theorem NormedCommGroup.nhds_one_basis_norm_lt

added def NormedCommGroup.ofMulDist'

added def NormedCommGroup.ofMulDist

added def NormedCommGroup.ofSeparation

added theorem NormedCommGroup.tendsto_nhds_nhds

added theorem NormedCommGroup.tendsto_nhds_one

added theorem NormedCommGroup.uniformity_basis_dist

added def NormedGroup.induced

added def NormedGroup.ofMulDist'

added def NormedGroup.ofMulDist

added def NormedGroup.ofSeparation

added theorem PUnit.norm_eq_zero

added theorem Pi.nnnorm_def'

added theorem Pi.norm_def'

added theorem Pi.sum_nnnorm_apply_le_nnnorm'

added theorem Pi.sum_norm_apply_le_norm'

added theorem Prod.nnorm_def

added theorem Prod.norm_def

added theorem Rat.norm_cast_real

added theorem Real.ennnorm_eq_ofReal

added theorem Real.ennnorm_eq_ofReal_abs

added theorem Real.le_norm_self

added theorem Real.nnnorm_abs

added theorem Real.nnnorm_coe_nat

added theorem Real.nnnorm_of_nonneg

added theorem Real.nnnorm_two

added theorem Real.norm_coe_nat

added theorem Real.norm_eq_abs

added theorem Real.norm_of_nonneg

added theorem Real.norm_of_nonpos

added theorem Real.norm_two

added theorem Real.ofReal_le_ennnorm

added theorem Real.toNNReal_eq_nnnorm_of_nonneg

added def SeminormedCommGroup.induced

added theorem SeminormedCommGroup.mem_closure_iff

added def SeminormedCommGroup.ofMulDist'

added def SeminormedCommGroup.ofMulDist

added def SeminormedGroup.induced

added def SeminormedGroup.ofMulDist'

added def SeminormedGroup.ofMulDist

added theorem SeminormedGroup.tendstoUniformlyOn_one

added theorem SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one

added theorem SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one

added theorem Subgroup.coe_norm

added theorem Subgroup.norm_coe

added theorem Submodule.coe_norm

added theorem Submodule.norm_coe

added theorem ULift.nnnorm_def

added theorem ULift.nnnorm_down

added theorem ULift.nnnorm_up

added theorem ULift.norm_def

added theorem ULift.norm_down

added theorem ULift.norm_up

added theorem abs_dist_sub_le_dist_mul_mul

added theorem abs_norm_sub_norm_le'

added theorem ball_eq'

added theorem ball_one_eq

added theorem bounded_iff_forall_norm_le'

added theorem cauchySeq_prod_of_eventually_eq

added theorem closure_one_eq

added theorem coe_comp_nnnorm'

added theorem coe_nnnorm'

added theorem coe_normGroupNorm

added theorem coe_normGroupSeminorm

added theorem comap_norm_nhds_one

added theorem continuous_nnnorm'

added theorem continuous_norm'

added theorem controlled_prod_of_mem_closure

added theorem controlled_prod_of_mem_closure_range

added theorem dist_div_div_le

added theorem dist_div_div_le_of_le

added theorem dist_div_eq_dist_mul_left

added theorem dist_div_eq_dist_mul_right

added theorem dist_eq_norm_div'

added theorem dist_eq_norm_div

added theorem dist_inv

added theorem dist_le_norm_mul_norm

added theorem dist_mul_mul_le

added theorem dist_mul_mul_le_of_le

added theorem dist_mul_self_left

added theorem dist_mul_self_right

added theorem dist_norm_norm_le'

added theorem dist_one_left

added theorem dist_one_right

added theorem dist_prod_prod_le

added theorem dist_prod_prod_le_of_le

added theorem dist_self_div_left

added theorem dist_self_div_right

added theorem dist_self_mul_left

added theorem dist_self_mul_right

added theorem edist_eq_coe_nnnorm'

added theorem edist_eq_coe_nnnorm_div

added theorem edist_mul_mul_le

added theorem eq_of_norm_div_le_zero

added theorem eventually_ne_of_tendsto_norm_atTop'

added theorem hasCompactSupport_norm_iff

added theorem lipschitzOnWith_iff_norm_div_le

added theorem lipschitzWith_iff_norm_div_le

added theorem lipschitzWith_one_nnnorm'

added theorem lipschitzWith_one_norm'

added theorem mem_ball_iff_norm'''

added theorem mem_ball_iff_norm''

added theorem mem_ball_one_iff

added theorem mem_closedBall_iff_norm'''

added theorem mem_closedBall_iff_norm''

added theorem mem_closedBall_one_iff

added theorem mem_closure_one_iff_norm

added theorem mem_emetric_ball_one_iff

added theorem mem_sphere_iff_norm'

added theorem mem_sphere_one_iff_norm

added theorem mul_mem_ball_iff_norm

added theorem mul_mem_ball_mul_iff

added theorem mul_mem_closedBall_iff_norm

added theorem mul_mem_closedBall_mul_iff

added theorem ne_one_of_mem_sphere

added theorem ne_one_of_mem_unit_sphere

added theorem ne_one_of_nnnorm_ne_zero

added theorem ne_one_of_norm_ne_zero

added theorem nndist_eq_nnnorm_div

added theorem nndist_mul_mul_le

added theorem nndist_nnnorm_nnnorm_le'

added theorem nnnorm_div_le

added theorem nnnorm_eq_zero'

added theorem nnnorm_inv'

added theorem nnnorm_le_mul_nnnorm_add

added theorem nnnorm_le_nnnorm_add_nnnorm_div'

added theorem nnnorm_le_nnnorm_add_nnnorm_div

added theorem nnnorm_le_pi_nnnorm'

added theorem nnnorm_mul_le'

added theorem nnnorm_multiset_prod_le

added theorem nnnorm_ne_zero_iff'

added theorem nnnorm_ofAdd

added theorem nnnorm_ofDual

added theorem nnnorm_ofMul

added theorem nnnorm_one'

added theorem nnnorm_pow_le_mul_norm

added theorem nnnorm_prod_le

added theorem nnnorm_prod_le_of_le

added theorem nnnorm_toAdd

added theorem nnnorm_toDual

added theorem nnnorm_toMul

added theorem nnnorm_zpow_le_mul_norm

added def normGroupNorm

added def normGroupSeminorm

added theorem norm_div_eq_zero_iff

added theorem norm_div_le

added theorem norm_div_le_of_le

added theorem norm_div_pos_iff

added theorem norm_div_rev

added theorem norm_div_sub_norm_div_le_norm_div

added theorem norm_eq_of_mem_sphere'

added theorem norm_eq_zero'''

added theorem norm_eq_zero''

added theorem norm_fst_le

added theorem norm_inv'

added theorem norm_le_mul_norm_add

added theorem norm_le_norm_add_const_of_dist_le'

added theorem norm_le_norm_add_norm_div'

added theorem norm_le_norm_add_norm_div

added theorem norm_le_of_mem_closedBall'

added theorem norm_le_pi_norm'

added theorem norm_le_zero_iff'''

added theorem norm_le_zero_iff''

added theorem norm_lt_of_mem_ball'

added theorem norm_mul_le'

added theorem norm_mul_le_of_le

added theorem norm_multiset_prod_le

added theorem norm_multiset_sum_le

added theorem norm_mul₃_le

added theorem norm_ne_zero_iff'

added theorem norm_nonneg'

added theorem norm_ofAdd

added theorem norm_ofDual

added theorem norm_ofMul

added theorem norm_of_subsingleton'

added theorem norm_one'

added theorem norm_pos_iff'''

added theorem norm_pos_iff''

added theorem norm_pow_le_mul_norm

added theorem norm_prod_le

added theorem norm_prod_le_iff

added theorem norm_prod_le_of_le

added theorem norm_snd_le

added theorem norm_sub_norm_le'

added theorem norm_sum_le

added theorem norm_toAdd

added theorem norm_toDual

added theorem norm_toMul

added theorem norm_toNNReal'

added theorem norm_zpow_le_mul_norm

added theorem ofReal_norm_eq_coe_nnnorm'

added theorem pi_nnnorm_const'

added theorem pi_nnnorm_const_le'

added theorem pi_nnnorm_le_iff'

added theorem pi_nnnorm_lt_iff'

added theorem pi_norm_const'

added theorem pi_norm_const_le'

added theorem pi_norm_le_iff_of_nonempty'

added theorem pi_norm_le_iff_of_nonneg'

added theorem pi_norm_lt_iff'

added theorem pow_mem_ball

added theorem pow_mem_closedBall

added theorem preimage_mul_ball

added theorem preimage_mul_closedBall

added theorem preimage_mul_sphere

added theorem smul_ball''

added theorem smul_closedBall''

added theorem squeeze_one_norm'

added theorem squeeze_one_norm

added theorem tendsto_iff_norm_tendsto_one

added theorem tendsto_norm'

added theorem tendsto_norm_cocompact_atTop'

added theorem tendsto_norm_div_self

added theorem tendsto_norm_div_self_punctured_nhds

added theorem tendsto_norm_nhdsWithin_one

added theorem tendsto_norm_one

added theorem tendsto_one_iff_norm_tendsto_one

added theorem uniformContinuous_nnnorm'

added theorem uniformContinuous_norm'

added theorem zero_lt_one_add_norm_sq'