Hadamard

📁 Source: Mathlib/Analysis/Complex/Hadamard.lean

Statistics

Metric	Count
Definitions F, interpStrip, interpStrip', invInterpStrip, sSupNormIm, scale, verticalClosedStrip, verticalStrip	8
Theorems F_BddAbove, F_edge_le_one, diffContOnCl_interpStrip, diffContOnCl_invInterpStrip, eventuallyle, interpStrip_eq_of_mem_verticalStrip, interpStrip_eq_of_pos, interpStrip_eq_of_zero, interpStrip_scale, mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip, norm_invInterpStrip, norm_le_interpStrip_of_mem_verticalClosedStrip, norm_le_interpStrip_of_mem_verticalClosedStrip_eps, norm_le_interpStrip_of_mem_verticalClosedStrip₀₁, norm_le_interpStrip_of_mem_verticalStrip_zero, norm_le_interp_of_mem_verticalClosedStrip', norm_le_interp_of_mem_verticalClosedStrip₀₁', norm_le_sSupNormIm, norm_lt_sSupNormIm_eps, norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip, sSupNormIm_eps_pos, sSupNormIm_nonneg, sSupNormIm_scale_left, sSupNormIm_scale_right, scale_bddAbove, scale_bound_left, scale_bound_right, scale_diffContOnCl, scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip, scale_id_mem_verticalStrip_of_mem_verticalStrip	30
Total	38

Complex.HadamardThreeLines

Definitions

Name	Category	Theorems
F 📖	CompOp	3 math math: F_BddAbove, F_edge_le_one, norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip
interpStrip 📖	CompOp	7 math math: interpStrip_scale, interpStrip_eq_of_pos, interpStrip_eq_of_zero, diffContOnCl_interpStrip, norm_le_interpStrip_of_mem_verticalStrip_zero, interpStrip_eq_of_mem_verticalStrip, norm_le_interpStrip_of_mem_verticalClosedStrip₀₁
interpStrip' 📖	CompOp	2 math math: interpStrip_scale, norm_le_interpStrip_of_mem_verticalClosedStrip
invInterpStrip 📖	CompOp	2 math math: norm_invInterpStrip, diffContOnCl_invInterpStrip
sSupNormIm 📖	CompOp	10 math math: norm_le_interpStrip_of_mem_verticalClosedStrip_eps, norm_le_sSupNormIm, norm_invInterpStrip, sSupNormIm_eps_pos, sSupNormIm_scale_left, interpStrip_eq_of_mem_verticalStrip, norm_lt_sSupNormIm_eps, eventuallyle, sSupNormIm_nonneg, sSupNormIm_scale_right
scale 📖	CompOp	7 math math: interpStrip_scale, scale_bound_left, sSupNormIm_scale_left, scale_bddAbove, scale_diffContOnCl, sSupNormIm_scale_right, scale_bound_right
verticalClosedStrip 📖	CompOp	—
verticalStrip 📖	CompOp	2 math math: diffContOnCl_interpStrip, diffContOnCl_invInterpStrip

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
F_BddAbove 📖	mathematical	Real Real.instLT Real.instZero BddAbove Real.instLE Set.image Complex Norm.norm NormedAddCommGroup.toNorm verticalClosedStrip Real.instOne	F	—	Set.image_congr bddAbove_def norm_smul NormedSpace.toNormSMulClass norm_mul NormedDivisionRing.toNormMulClass mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono le_trans Complex.norm_cpow_eq_rpow_re_of_pos sSupNormIm_eps_pos Real.rpow_le_one_of_one_le_of_nonpos sub_nonpos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_max_left Real.rpow_le_rpow_of_exponent_ge le_of_lt not_le IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le le_max_right Right.neg_nonpos_iff neg_le_neg_iff norm_nonneg lt_max_of_lt_left Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing
F_edge_le_one 📖	mathematical	Real Real.instLT Real.instZero BddAbove Real.instLE Set.image Complex Norm.norm NormedAddCommGroup.toNorm verticalClosedStrip Real.instOne Set Set.instMembership Set.preimage Complex.re Set.instInsert Set.instSingletonSet	F	—	norm_smul NormedSpace.toNormSMulClass norm_invInterpStrip zero_sub Real.rpow_neg_one neg_zero Real.rpow_zero mul_one inv_mul_le_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing sSupNormIm_eps_pos le_of_lt norm_lt_sSupNormIm_eps Real.instZeroLEOneClass Set.mem_singleton_iff sub_self one_mul
diffContOnCl_interpStrip 📖	mathematical	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace interpStrip verticalStrip Real Real.instZero Real.instOne	—	interpStrip_eq_of_zero diffContOnCl_const Differentiable.diffContOnCl interpStrip_eq_of_pos lt_of_le_of_ne sSupNormIm_nonneg DifferentiableAt.mul DifferentiableAt.const_cpow DifferentiableAt.const_sub differentiableAt_id
diffContOnCl_invInterpStrip 📖	mathematical	Real Real.instLT Real.instZero	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace invInterpStrip verticalStrip Real.instOne	—	Differentiable.diffContOnCl Differentiable.mul Differentiable.const_cpow Differentiable.sub_const differentiable_id Complex.ofReal_add Complex.ofReal_ne_zero ne_of_gt sSupNormIm_eps_pos Differentiable.neg
eventuallyle 📖	mathematical	BddAbove Real Real.instLE Set.image Complex Norm.norm NormedAddCommGroup.toNorm verticalClosedStrip Real.instZero Real.instOne DiffContOnCl DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace verticalStrip Set Set.instMembership	Filter.EventuallyLE nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioi Real.instPreorder Complex.instNorm Complex.instMul Complex.instPow Complex.instAdd Complex.ofReal sSupNormIm Complex.instSub Complex.instOne	—	Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' norm_le_interpStrip_of_mem_verticalClosedStrip_eps Set.mem_of_mem_of_subset Set.preimage_mono Set.Ioo_subset_Icc_self
interpStrip_eq_of_mem_verticalStrip 📖	mathematical	Complex Set Set.instMembership verticalStrip Real Real.instZero Real.instOne	interpStrip Complex.instMul Complex.instPow Complex.ofReal sSupNormIm Complex.instSub Complex.instOne	—	interpStrip_eq_of_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass sub_eq_zero ne_of_lt lt_of_le_of_ne sSupNormIm_nonneg interpStrip_eq_of_pos
interpStrip_eq_of_pos 📖	mathematical	Real Real.instLT Real.instZero sSupNormIm Real.instOne	interpStrip Complex Complex.instMul Complex.instPow Complex.ofReal Complex.instSub Complex.instOne	—	ne_of_gt
interpStrip_eq_of_zero 📖	mathematical	sSupNormIm Real Real.instZero Real.instOne	interpStrip Complex Complex.instZero	—	—
interpStrip_scale 📖	mathematical	Real Real.instLT	interpStrip scale Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instSub Complex.ofReal interpStrip'	—	sSupNormIm_scale_left sSupNormIm_scale_right
mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip 📖	mathematical	Real Real.instLT Complex Set Set.instMembership verticalClosedStrip	Real.instZero Real.instOne Complex.instSub DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.ofReal	—	Complex.div_re sub_self MulZeroClass.mul_zero zero_div add_zero covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid AddGroup.toOrderedSub Nat.cast_one Complex.normSq_ofReal mul_div_assoc div_mul_eq_div_div_swap div_self Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing sub_eq_zero_of_eq div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing le_of_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd sub_le_sub_iff_right add_sub_assoc div_sub_div_same div_le_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
norm_invInterpStrip 📖	mathematical	Real Real.instLT Real.instZero	Norm.norm Complex Complex.instNorm invInterpStrip Real.instMul Real.instPow Real.instAdd sSupNormIm Real.instSub Complex.re Real.instOne Real.instNeg	—	norm_mul NormedDivisionRing.toNormMulClass Complex.ofReal_add Complex.norm_cpow_eq_rpow_re_of_pos sSupNormIm_eps_pos
norm_le_interpStrip_of_mem_verticalClosedStrip 📖	mathematical	Real Real.instLT Complex Set Set.instMembership verticalClosedStrip DiffContOnCl DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace verticalStrip BddAbove Real.instLE Set.image Norm.norm NormedAddCommGroup.toNorm	Complex.instNorm interpStrip'	—	norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip scale_diffContOnCl scale_bddAbove interpStrip_scale div_sub_div_same
norm_le_interpStrip_of_mem_verticalClosedStrip_eps 📖	mathematical	Real Real.instLT Real.instZero BddAbove Real.instLE Set.image Complex Norm.norm NormedAddCommGroup.toNorm verticalClosedStrip Real.instOne DiffContOnCl DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace verticalStrip Set Set.instMembership	Complex.instNorm Complex.instMul Complex.instPow Complex.instAdd Complex.ofReal sSupNormIm Complex.instSub Complex.instOne	—	norm_mul NormedDivisionRing.toNormMulClass Complex.norm_cpow_eq_rpow_re_of_pos sSupNormIm_eps_pos mul_inv_le_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.rpow_pos_of_pos one_mul mul_inv_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.rpow_neg_one Real.rpow_mul le_of_lt mul_neg mul_one neg_sub mul_assoc norm_smul NormedSpace.toNormSMulClass norm_invInterpStrip mul_comm norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip
norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ 📖	mathematical	Complex Set Set.instMembership verticalClosedStrip Real Real.instZero Real.instOne DiffContOnCl DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace verticalStrip BddAbove Real.instLE Set.image Norm.norm NormedAddCommGroup.toNorm	Complex.instNorm interpStrip	—	le_on_closure HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid norm_le_interpStrip_of_mem_verticalStrip_zero Continuous.comp_continuousOn' continuous_norm DiffContOnCl.continuousOn diffContOnCl_interpStrip Complex.closure_preimage_re closure_Ioo instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing zero_ne_one NeZero.charZero_one RCLike.charZero_rclike verticalClosedStrip.eq_1
norm_le_interpStrip_of_mem_verticalStrip_zero 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace verticalStrip Real Real.instZero Real.instOne BddAbove Real.instLE Set.image Norm.norm NormedAddCommGroup.toNorm verticalClosedStrip Set Set.instMembership	Complex.instNorm interpStrip	—	tendsto_le_of_eventuallyLE HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid nhdsGT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace interpStrip_eq_of_mem_verticalStrip zero_add ContinuousWithinAt.tendsto norm_mul NormedDivisionRing.toNormMulClass Complex.norm_cpow_eq_rpow_re_of_nonneg le_of_lt sSupNormIm_eps_pos ne_of_lt tendsto_nhdsWithin_congr sSupNormIm_nonneg Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.rpow_const Filter.Tendsto.add_const IsTopologicalSemiring.toContinuousAdd tendsto_nhdsWithin_of_tendsto_nhds Continuous.tendsto continuous_id' covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono eventuallyle
norm_le_interp_of_mem_verticalClosedStrip' 📖	mathematical	Real Real.instLT Complex Set Set.instMembership verticalClosedStrip DiffContOnCl DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace verticalStrip BddAbove Real.instLE Set.image Norm.norm NormedAddCommGroup.toNorm	Real.instMul Real.instPow Real.instSub Real.instOne DivInvMonoid.toDiv Real.instDivInvMonoid Complex.re	—	norm_le_interp_of_mem_verticalClosedStrip₀₁' mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip scale_diffContOnCl scale_bddAbove scale_bound_left scale_bound_right
norm_le_interp_of_mem_verticalClosedStrip₀₁' 📖	mathematical	Complex Set Set.instMembership verticalClosedStrip Real Real.instZero Real.instOne DiffContOnCl DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace verticalStrip BddAbove Real.instLE Set.image Norm.norm NormedAddCommGroup.toNorm	Real.instMul Real.instPow Real.instSub Complex.re	—	interpStrip_eq_of_zero norm_zero mul_nonneg_iff AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toPosMulStrictMono IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.rpow_nonneg sSupNormIm_nonneg interpStrip_eq_of_pos lt_of_le_of_ne norm_mul NormedDivisionRing.toNormMulClass Complex.norm_cpow_eq_rpow_re_of_pos Ne.le_iff_lt LE.le.trans norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ mul_le_mul_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono Real.rpow_le_rpow sSupNormIm.eq_1 csSup_le Set.image_congr sub_nonneg covariant_swap_add_of_covariant_add norm_nonneg
norm_le_sSupNormIm 📖	mathematical	Complex Set Set.instMembership verticalClosedStrip Real Real.instZero Real.instOne BddAbove Real.instLE Set.image Norm.norm NormedAddCommGroup.toNorm	sSupNormIm Complex.re	—	le_csSup BddAbove.mono Set.image_mono Set.preimage_mono Set.singleton_subset_iff Set.mem_image_of_mem
norm_lt_sSupNormIm_eps 📖	mathematical	Real Real.instLT Real.instZero Complex Set Set.instMembership verticalClosedStrip Real.instOne BddAbove Real.instLE Set.image Norm.norm NormedAddCommGroup.toNorm	Real.instAdd sSupNormIm Complex.re	—	lt_add_of_pos_of_le IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_le_sSupNormIm
norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip 📖	mathematical	Real Real.instLT Real.instZero DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace verticalStrip Real.instOne BddAbove Real.instLE Set.image Norm.norm NormedAddCommGroup.toNorm verticalClosedStrip Set Set.instMembership	F	—	PhragmenLindelof.vertical_strip DiffContOnCl.smul IsScalarTower.left diffContOnCl_invInterpStrip sub_zero div_one Real.pi_pos F_BddAbove Asymptotics.isBigO_iff Filter.eventually_inf_principal Filter.Eventually.of_forall MulZeroClass.zero_mul Real.exp_zero mul_one Real.abs_exp one_mul LE.le.trans Set.image_congr Set.preimage_mono Set.Ioo_subset_Icc_self le_of_lt lt_add_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.add_one_le_exp F_edge_le_one
sSupNormIm_eps_pos 📖	mathematical	Real Real.instLT Real.instZero	Real.instAdd sSupNormIm	—	lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le sSupNormIm_nonneg
sSupNormIm_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero sSupNormIm	—	Real.sSup_nonneg
sSupNormIm_scale_left 📖	mathematical	Real Real.instLT	sSupNormIm scale Real.instZero	—	Set.image_comp Set.ext Set.image_congr MulZeroClass.zero_mul sub_self MulZeroClass.mul_zero add_zero Nat.cast_zero Complex.div_re Complex.normSq_ofReal Complex.ofReal_re zero_div sub_zero Complex.ofReal_sub div_mul_comm div_self Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing sub_eq_zero_of_eq one_mul add_sub_cancel
sSupNormIm_scale_right 📖	mathematical	Real Real.instLT	sSupNormIm scale Real.instOne	—	Set.image_comp Set.ext Set.image_congr one_mul sub_self MulZeroClass.mul_zero sub_zero add_sub_cancel Nat.cast_one Complex.div_re Complex.normSq_ofReal Complex.ofReal_re Complex.ofReal_sub zero_div add_zero div_mul_eq_div_div_swap mul_div_assoc div_self Nat.cast_zero Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing sub_eq_zero_of_eq mul_one div_mul_comm
scale_bddAbove 📖	mathematical	Real Real.instLT BddAbove Real.instLE Set.image Complex Norm.norm NormedAddCommGroup.toNorm verticalClosedStrip	scale Real.instZero Real.instOne	—	bddAbove_def Set.image_congr scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip
scale_bound_left 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Complex Set Set.instMembership Set.preimage Complex.re Set.instSingletonSet Real.instZero	scale	—	MulZeroClass.zero_mul sub_self MulZeroClass.mul_zero add_zero
scale_bound_right 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Complex Set Set.instMembership Set.preimage Complex.re Set.instSingletonSet Real.instOne	scale	—	one_mul sub_self MulZeroClass.mul_zero sub_zero add_sub_cancel
scale_diffContOnCl 📖	mathematical	Real Real.instLT DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace verticalStrip	scale Real.instZero Real.instOne	—	DiffContOnCl.comp DiffContOnCl.const_add DiffContOnCl.smul_const IsScalarTower.right Differentiable.diffContOnCl differentiable_id Set.MapsTo.eq_1 scale_id_mem_verticalStrip_of_mem_verticalStrip
scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip 📖	mathematical	Real Real.instLT Complex Set Set.instMembership verticalClosedStrip Real.instZero Real.instOne	Complex.instAdd Complex.ofReal Complex.instMul Complex.instSub	—	sub_self MulZeroClass.mul_zero sub_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add add_comm sub_le_sub_iff_right add_sub_assoc add_zero one_mul sub_nonneg LT.lt.le mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing
scale_id_mem_verticalStrip_of_mem_verticalStrip 📖	mathematical	Real Real.instLT Complex Set Set.instMembership verticalStrip Real.instZero Real.instOne	Complex.instAdd Complex.ofReal Complex.instMul Complex.instSub	—	sub_self MulZeroClass.mul_zero sub_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add add_comm sub_lt_sub_iff_right add_sub_assoc add_zero one_mul mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono

---

← Back to Index