| Name | Category | Theorems |
|---|
hasOpNorm š | CompOp | 243 mathmath: Matrix.l2_opNorm_toEuclideanCLM, MeasureTheory.L1.SimpleFunc.norm_Integral_le_one, LinearMap.mkContinuousā_norm_le', HasCompactSupport.convolution_integrand_bound_left, opNorm_prod, norm_inr_le_one, opNorm_le_of_unit_norm, opNorm_bound_of_ball_bound, sSup_unit_ball_eq_norm, norm_jacobiThetaā_term_fderiv_ge, norm_inl_le_one, opNorm_le_bound', isBigOWith_sub, norm_iteratedFDerivWithin_one, MeasureTheory.L1.norm_setToL1_le, RCLike.conjCLE_norm, opNorm_ext, norm_compLp_le, ContinuousLinearEquiv.subsingleton_or_norm_symm_pos, norm_compContinuousMultilinearMap_le, opNorm_comp_linearIsometryEquiv, Complex.ofRealCLM_norm, opNorm_lsmul_apply_le, Module.Basis.exists_opNorm_le, isBigOWith_id, MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM, HasFDerivAt.le_of_lipschitzOn, opNorm_mul_flip_apply, norm_extendToš, Real.integrable_prod_sub, MeasureTheory.convolution_integrand_bound_right_of_le_of_subset, ContinuousMap.toLp_norm_le, ContinuousMultilinearMap.norm_smulRightL_le, RCLike.reCLM_norm, opNorm_mul, norm_fst_le, DoubleCentralizer.norm_fst_eq_snd, le_opNorm, DoubleCentralizer.norm_def', adjointAux_norm, ContinuousAffineMap.norm_def, norm_iteratedFDerivWithin_comp_left, DoubleCentralizer.norm_def, FDerivMeasurableAux.norm_sub_le_of_mem_A, ContinuousLinearEquiv.one_le_norm_mul_norm_symm, eventually_norm_mfderivWithin_symm_extChartAt_lt, LinearIsometry.norm_toContinuousLinearMap, norm_toSpanSingleton, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, opNorm_le_of_shell', NormedSpace.inclusionInDoubleDual_norm_eq, opNorm_mul_apply, norm_smulRightL, ContinuousMultilinearMap.curryLeft_norm, ContinuousAlternatingMap.norm_curryLeft, NormedSpace.inclusionInDoubleDual_norm_le, LinearMap.norm_mkContinuousā_aux, ContinuousAffineMap.norm_eq, ContinuousAlternatingMap.norm_alternatizeUncurryFinCLM_le, ratio_le_opNorm, norm_fderiv_le_of_lipschitz, Complex.imCLM_norm, ContinuousAffineMap.norm_contLinear_le, ContinuousAlternatingMap.norm_ofSubsingleton, norm_smulRight_apply, UniformSpace.Completion.norm_toComplL, PiTensorProduct.liftEquiv_symm_apply, Submodule.norm_subtypeL, norm_iteratedFDeriv_le_of_bilinear, opNorm_le_of_ball, norm_precompR_le, opNorm_le_bound, MultilinearMap.mkContinuousLinear_norm_le, MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm, FormalMultilinearSeries.norm_compContinuousLinearMap_le, DoubleCentralizer.norm_snd, opNorm_comp_le, Submodule.starProjection_norm_le, MeasureTheory.norm_weightedSMul_le, norm_fderiv_norm_rpow_le, Unitization.norm_eq_sup, ContinuousMap.toLp_norm_eq_toLp_norm_coe, Submodule.norm_starProjection, exists_dual_vector, banach_steinhaus, rayleighQuotient_le_norm, norm_def, le_opNorm_of_le, NormedSpace.equicontinuous_TFAE, opNorm_add_le, sSup_sphere_eq_norm, norm_inr, opNorm_extend_le, opNorm_mulLeftRight_apply_le, norm_map_tail_le, exists_dual_vector'', norm_fderiv_iteratedFDeriv, MeasureTheory.Lp.norm_constL_le, LinearIsometry.norm_toContinuousLinearMap_comp, isBigOWith_comp, eventually_norm_symmL_trivializationAt_self_comp_lt, MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le', ContinuousLinearEquiv.norm_symm_pos, MultilinearMap.mkContinuousLinear_norm_le', norm_fderivWithin_iteratedFDerivWithin, norm_extendToš'_bound, norm_derivWithin_eq_norm_fderivWithin, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, le_opNormā, norm_iteratedFDeriv_comp_left, norm_uncurryMid, opNorm_mul_le, uncurryLeft_norm, opNorm_subsingleton, ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le, MeasureTheory.dist_convolution_le', LinearMap.opNorm_extendOfNorm_le, InnerProductSpace.innerSL_norm, Unitization.norm_def, eventually_norm_symmL_trivializationAt_comp_self_lt, norm_single, norm_extendToš', coord_norm', norm_fderiv_norm, LinearMap.mkContinuousā_norm_le, StrongDual.norm_toLpā_le, RCLike.ofRealCLM_norm, opNorm_zero, LinearMap.mkContinuous_norm_le', exists_dual_vector', HasFDerivAt.le_of_lip', eventually_norm_symmL_trivializationAt_lt, opNorm_le_iff, opNorm_zero_iff, norm_iteratedFDerivWithin_le_of_bilinear, norm_compContinuousAlternatingMap_le, norm_id_le, HasFDerivAt.le_of_lipschitz, LinearMap.mkContinuous_norm_le, opNorm_mulLeftRight_apply_apply_le, opNorm_lsmul_le, WeakDual.CharacterSpace.norm_le_norm_one, Matrix.linfty_opNorm_toMatrix, innerSL_apply_norm, norm_compL_le, norm_fst, PiTensorProduct.mapL_opNorm, MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le, PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm, norm_restrictScalars, opNorm_mul_apply_le, opNorm_smul_le, MeasureTheory.L1.norm_setToL1_le', norm_iteratedFDeriv_one, norm_bilinearRestrictScalars, norm_inl, norm_deriv_eq_norm_fderiv, DoubleCentralizer.norm_fst, BoundedContinuousFunction.toLp_norm_le, ContDiffMapSupportedIn.seminorm_postcompLM_le, Matrix.linfty_opNorm_eq_opNorm, norm_fderiv_le_of_lipschitzOn, opNorm_le_iff_lipschitz, opNorm_le_of_nhds_zero, opNorm_flip, AlgHom.toContinuousLinearMap_norm, opNorm_le_of_shell, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, AlternatingMap.mkContinuousLinear_norm_le, norm_single_le_one, norm_compSL_le, MeasureTheory.norm_condExpInd_le, opNorm_nonneg, normOneClass, opNorm_neg, ContinuousAlternatingMap.norm_alternatizeUncurryFin_le, Complex.norm_fderiv_le_one_of_mapsTo_ball, Complex.conjCLE_norm, unit_le_opNorm, exists_extension_norm_eq, norm_id, MeasureTheory.L1.norm_Integral_le_one, norm_smulRightL_le, VectorFourier.norm_fourierSMulRight_le, Unitization.norm_splitMul_snd_sq, ContinuousMultilinearMap.norm_ofSubsingleton, VectorFourier.norm_fourierPowSMulRight_le, ProbabilityTheory.norm_uncenteredCovarianceBilin_le, VectorFourier.norm_fourierSMulRight, ContinuousLinearEquiv.coord_norm', LinearIsometry.norm_toContinuousLinearMap_le, FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2, Complex.reCLM_norm, norm_snd_le, opNorm_mulLeftRight_le, norm_compLpL_le, sSup_unitClosedBall_eq_norm, ContinuousLinearEquiv.coord_norm, opNorm_eq_of_bounds, norm_adjoint_comp_self, Submodule.norm_orthogonalProjection, opNorm_lsmul, norm_id_of_nontrivial_seminorm, NormedSpace.double_dual_bound, Matrix.cstar_norm_def, Module.Basis.opNorm_le, norm_snd, norm_fderiv_le_of_lip', norm_holderL_le, ContinuousAlternatingMap.norm_compContinuousLinearMap_le, eventually_norm_trivializationAt_lt, Matrix.l2_opNorm_def, ContinuousMultilinearMap.norm_compContinuousLinearMapL_le, Complex.norm_fderiv_le_div_of_mapsTo_ball, norm_innerSL_le, isLeast_opNorm, Real.exists_extension_norm_eq, AlternatingMap.mkContinuousLinear_norm_le_max, dist_le_opNorm, norm_fderiv_norm_id_rpow, norm_holder_apply_apply_le, homothety_norm, Submodule.norm_subtypeL_le, ContinuousMultilinearMap.norm_compContinuousLinearMap_le, eventually_norm_mfderiv_extChartAt_lt, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, norm_precompL_le, norm_map_removeNth_le, Submodule.orthogonalProjection_norm_le, MeasureTheory.norm_condExpL2_le_one, HasCompactSupport.convolution_integrand_bound_right, HasCompactSupport.convolution_integrand_bound_right_of_subset, norm_smulRightL_apply, opNorm_le_boundā, ContinuousMultilinearMap.norm_curryMid, opNorm_le_of_lipschitz, toSesqForm_apply_norm_le, CStarMatrix.norm_def, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le, InnerProductSpace.norm_rankOne, norm_jacobiThetaā_term_fderiv_le, ContinuousLinearEquiv.norm_pos, norm_iteratedFDerivWithin_le_of_bilinear_aux
|
opNorm š | CompOp | ā |
restrictScalarsIsometry š | CompOp | 2 mathmath: coe_restrictScalarsIsometry, restrictScalarsIsometry_toLinearMap
|
seminorm š | CompOp | ā |
toNormedAlgebra š | CompOp | ā |
toNormedSpace š | CompOp | 209 mathmath: ContMDiffAt.coordChangeL, MDifferentiable.coordChangeL, LinearMap.mkContinuousā_norm_le', SchwartzMap.lineDerivOpCLM_eq, Bundle.ContMDiffRiemannianMetric.contMDiff, HasCompactSupport.convolution_integrand_bound_left, Real.fderiv_fourierIntegral, ContDiff.fderiv_succ, ContinuousMultilinearMap.analyticAt_uncurry_compContinuousLinearMap, hasFTaylorSeriesUpToOn_top_iff_right, hasFDerivAt_integral_of_dominated_loc_of_lip_interval, integral_apply, SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left, Real.fourier_continuousLinearMap_apply, ContDiffAt.fderiv_right_succ, iteratedFDerivWithin_succ_eq_comp_right, ContMDiffWithinAt.mfderivWithin_const, FormalMultilinearSeries.derivSeries_coeff_one, mdifferentiableOn_symm_coordChangeL, fderiv_clm_comp, ContinuousMultilinearMap.norm_compContinuousLinearMapLRight_le, Bundle.ContinuousLinearMap.vectorBundle, SchwartzMap.fderivCLM_apply, Real.integrable_prod_sub, ContDiffAt.fderiv_succ, MeasureTheory.convolution_integrand_bound_right_of_le_of_subset, ContinuousMultilinearMap.norm_smulRightL_le, VectorBundleCore.contMDiffOn_coordChange, HasFPowerSeriesWithinOnBall.fderivWithin, opNorm_mul, Real.fderiv_fourier, MeasureTheory.L1.setToL1_smul_left, intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip, VectorFourier.fourierIntegral_continuousLinearMap_apply, contDiff_succ_iff_fderiv, ContinuousMultilinearMap.curryRight_norm, ContDiffWithinAt.hasFDerivWithinAt_nhds, VectorFourier.hasFDerivAt_fourierIntegral, MeasureTheory.convolution_precompR_apply, Bundle.ContinuousRiemannianMetric.continuous, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, NormedSpace.inclusionInDoubleDual_norm_eq, iteratedFDerivWithin_succ_apply_right, contDiffAt_map_inverse, Real.fourierIntegral_continuousLinearMap_apply, AnalyticOn.fderivWithin, norm_smulRightL, ContDiffAt.fderiv_right, ContMDiffVectorBundle.continuousLinearMap, ContDiffOn.fderiv_of_isOpen, inCoordinates_apply_eqā, AnalyticOnNhd.fderiv_of_isOpen, contDiffOn_infty_iff_fderivWithin, Real.hasFDerivAt_fourier, HasFPowerSeriesOnBall.fderiv, ContMDiffOn.coordChangeL, mdifferentiableAt_hom_bundle, NormedSpace.inclusionInDoubleDual_norm_le, ContinuousAlternatingMap.norm_alternatizeUncurryFinCLM_le, MeasureTheory.hasFDerivAt_convolution_right_with_param, ContMDiffAt.mfderiv_const, HasCompactSupport.hasFDerivAt_convolution_right, MDifferentiableOn.coordChangeL, continuousMultilinearCurryRightEquiv_symm_apply, IsContMDiffRiemannianBundle.exists_contMDiff, ContDiffWithinAt.fderivWithin'', contMDiffAt_coordChangeL, hasFDerivAt_integral_of_dominated_loc_of_lip', MDifferentiableWithinAt.coordChangeL, coe_flipāįµ¢', contDiffOn_succ_iff_fderiv_of_isOpen, hasFTaylorSeriesUpToOn_succ_iff_right, ContinuousMultilinearMap.norm_map_init_le, SchwartzMap.smulRightCLM_apply_apply, MeasureTheory.setToFun_smul_left, norm_iteratedFDeriv_le_of_bilinear, norm_precompR_le, nnnorm_holder_apply_apply_le, IsContinuousRiemannianBundle.exists_continuous, contMDiffOn_continuousLinearMapCoordChange, Real.fourier_fderiv, hasFTaylorSeriesUpTo_succ_nat_iff_right, VectorFourier.fderiv_fourierIntegral, hasFTaylorSeriesUpToOn_succ_nat_iff_right, Bundle.ContinuousLinearMap.vectorPrebundle.isContMDiff, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contDiffOn_succ_iff_hasFDerivWithinAt, FormalMultilinearSeries.radius_unshift, PiTensorProduct.dualSeminorms_bounded, opNorm_mulLeftRight_apply_le, SchwartzMap.fourier_evalCLM_eq, contDiffOn_infty_iff_fderiv_of_isOpen, SchwartzMap.evalCLM_apply_apply, contMDiffOn_symm_coordChangeL, contMDiffAt_hom_bundle, PiTensorProduct.injectiveSeminorm_apply, HasFTaylorSeriesUpToOn.shift_of_succ, contDiffOn_fderiv_coord_change, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left, le_opNormā, opNorm_mul_le, ContDiffWithinAt.fderivWithin', contDiffAt_succ_iff_hasFDerivAt, MeasureTheory.dist_convolution_le', InnerProductSpace.innerSL_norm, ContMDiffWithinAt.mfderivWithin, iteratedFDeriv_succ_apply_right, mdifferentiableOn_continuousLinearMapCoordChange, contDiff_clm_apply_iff, LinearMap.mkContinuousā_norm_le, contDiffOn_clm_apply, HasFDerivWithinAt.clm_comp, IsInvertible.contDiffAt_map_inverse, HasFPowerSeriesWithinOnBall.fderivWithin_of_mem, intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le, Real.fourierIntegral_fderiv, SchwartzMap.tsupport_fderivCLM_subset, intervalIntegral_apply, AnalyticOnNhd.fderiv, opNNNorm_mul, norm_iteratedFDerivWithin_le_of_bilinear, iteratedFDeriv_succ_eq_comp_right, ContDiffOn.fderivWithin, Real.hasFDerivAt_fourierIntegral, FormalMultilinearSeries.radius_shift, mdifferentiableOn_coordChangeL, opNorm_lsmul_le, norm_compL_le, ContMDiffVectorBundle.contMDiffOn_coordChangeL, fderivWithin_clm_comp, VectorBundleCore.IsContMDiff.contMDiffOn_coordChange, MDifferentiableAt.coordChangeL, norm_bilinearRestrictScalars, SchwartzMap.fderivCLM_fourier_eq, ContDiffAt.fderiv, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, contDiffOn_succ_iff_fderivWithin, continuousMultilinearCurryRightEquiv_symm_apply', ContDiffWithinAt.fderivWithin, ContinuousMultilinearMap.cpolynomialOn_uncurry_compContinuousLinearMap, ContinuousMultilinearMap.analyticWithinAt_uncurry_compContinuousLinearMap, ContDiffPointwiseHolderAt.fderiv, Real.fourierIntegral_continuousLinearMap_apply', hasFDerivAt_integral_of_dominated_of_fderiv_le, CPolynomialOn.fderiv, opNorm_flip, ContMDiffWithinAt.coordChangeL, FormalMultilinearSeries.radius_le_radius_derivSeries, norm_compSL_le, coe_flipāįµ¢, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, ContMDiffAt.mfderiv, VectorPrebundle.contMDiffOn_contMDiffCoordChange, mdifferentiableAt_coordChangeL, hasFDerivAt_integral_of_dominated_of_fderiv_le'', norm_smulRightL_le, VectorFourier.norm_fourierSMulRight_le, HasFiniteFPowerSeriesOnBall.fderiv', continuousMultilinearCurryRightEquiv_apply', flipāįµ¢'_symm, VectorFourier.norm_fourierPowSMulRight_le, SchwartzMap.fourier_fderivCLM_eq, ContinuousMultilinearMap.analyticOnNhd_uncurry_compContinuousLinearMap, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, contMDiffOn_coordChangeL, opNorm_mulLeftRight_le, norm_iteratedFDerivWithin_fderivWithin, ContinuousMultilinearMap.cpolynomialAt_uncurry_compContinuousLinearMap, AnalyticAt.fderiv, opNorm_lsmul, NormedSpace.double_dual_bound, ContDiff.fderiv_right, norm_holderL_le, contDiff_infty_iff_fderiv, HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_analyticOn, exists_continuousLinearEquiv_fderiv_symm_eq, SchwartzMap.integral_clm_comp_laplacian_right_eq_left, norm_innerSL_le, continuousMultilinearCurryRightEquiv_apply, ContDiff.fderiv, flipāįµ¢_symm, exists_continuousLinearEquiv_fderivWithin_symm_eq, norm_holder_apply_apply_le, HasStrictFDerivAt.clm_comp, ContinuousMultilinearMap.analyticOn_uncurry_compContinuousLinearMap, VectorFourier.fourierIntegral_fderiv, smulRightL_apply_apply, mdifferentiableWithinAt_hom_bundle, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, norm_precompL_le, PiTensorProduct.mapLMultilinear_opNorm, HasCompactSupport.convolution_integrand_bound_right, HasFDerivAt.clm_comp, HasCompactSupport.convolution_integrand_bound_right_of_subset, contMDiffWithinAt_hom_bundle, mem_contMDiffFiberwiseLinear_iff, opNorm_le_boundā, norm_iteratedFDeriv_fderiv, PiTensorProduct.injectiveSeminorm_def, contDiff_succ_iff_hasFDerivAt, HasCompactSupport.hasFDerivAt_convolution_left, ContMDiff.coordChangeL, ContDiffWithinAt.fderivWithin_right, contDiffWithinAt_succ_iff_hasFDerivWithinAt, hasFDerivAt_integral_of_dominated_loc_of_lip, HasFiniteFPowerSeriesOnBall.fderiv, ContinuousMultilinearMap.uncurryRight_norm, norm_iteratedFDerivWithin_le_of_bilinear_aux
|
toPseudoMetricSpace š | CompOp | 15 mathmath: NormedSpace.isBounded_polar_of_mem_nhds_zero, dist_iteratedFDerivWithin_one, isCompact_image_coe_closedBall, RegularNormedAlgebra.isometry_mul', isClosed_image_coe_closedBall, WeakDual.isCompact_closedBall, NormedSpace.polar_ball_subset_closedBall_div, lipschitz_apply, WeakDual.isSeqCompact_closedBall, WeakDual.isClosed_closedBall, isometry_mul, NormedSpace.polar_ball, NormedSpace.sInter_polar_eq_closedBall, NormedSpace.closedBall_inv_subset_polar_closedBall, NormedSpace.polar_closedBall
|
toSeminormedAddCommGroup š | CompOp | 357 mathmath: ContinuousLinearEquiv.antilipschitz, LinearMap.IsSymmetric.clm_adjoint_eq, fderiv_iteratedFDeriv, LinearMap.mkContinuousā_norm_le', isPositive_iff_eq_sum_rankOne, Bundle.ContMDiffRiemannianMetric.contMDiff, InnerProductSpace.isPositive_rankOne_self, mulLeftRight_isBoundedBilinear, MDifferentiableOn.clm_postcomp, HasCompactSupport.convolution_integrand_bound_left, compSL_apply, InnerProductSpace.toLinearIsometry_toDual, hasFDerivAt_iff_hasGradientAt, LinearIsometry.nnnorm_toContinuousLinearMap, InnerProductSpace.rankOne_one_left_eq_innerSL, MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv, ContinuousMultilinearMap.analyticAt_uncurry_compContinuousLinearMap, MDifferentiableAt.cle_arrowCongr, sSup_unitClosedBall_eq_nnnorm, hasFTaylorSeriesUpToOn_top_iff_right, InnerProductSpace.isIdempotentElem_rankOne_self, Matrix.cstar_nnnorm_def, ApproximatesLinearOn.lipschitz, banach_steinhaus_iSup_nnnorm, ContinuousMultilinearMap.changeOrigin_toFormalMultilinearSeries, iteratedFDerivWithin_succ_eq_comp_right, eventually_enorm_mfderivWithin_symm_extChartAt_lt, HasFTaylorSeriesUpTo.hasFDerivAt, norm_iteratedFDerivWithin_clm_apply, ContMDiffOn.clm_postcomp, DoubleCentralizer.nnnorm_def', LinearMap.adjoint_eq_toCLM_adjoint, nnnorm_def, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, fderiv_clm_comp, InnerProductSpace.toDual_symm_apply, ContinuousMultilinearMap.norm_compContinuousLinearMapLRight_le, MeasureTheory.charFun_toDual_symm_eq_charFunDual, opNNNorm_le_iff, HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt, adjoint_id, iteratedFDerivWithin_succ_eq_comp_left, isStarNormal_iff_norm_eq_adjoint, InnerProductSpace.inner_left_rankOne_apply, norm_iteratedFDeriv_clm_apply, ContMDiffAt.clm_postcomp, ContMDiffWithinAt.clm_postcomp, Real.integrable_prod_sub, eq_adjoint_iff, InnerProductSpace.rankOne_apply, MeasureTheory.convolution_integrand_bound_right_of_le_of_subset, ContinuousMultilinearMap.norm_smulRightL_le, precompL_apply, DoubleCentralizer.nnnorm_snd, IsSelfAdjoint.adjoint_eq, MDifferentiable.clm_postcomp, enorm_fderiv_norm_rpow_le, isPositive_self_comp_adjoint, LinearMap.adjoint_toContinuousLinearMap, toSesqForm_apply_coe, LinearIsometryEquiv.adjoint_eq_symm, sSup_sphere_eq_nnnorm, hasFDerivWithinAt_of_bilinear, opNorm_mul, MDifferentiable.cle_arrowCongr, MeasureTheory.dominatedFinMeasAdditive_condExpInd, Complex.reCLM_nnnorm, Unitization.nnnorm_def, ApproximatesLinearOn.norm_fderiv_sub_le, hasStrictFDerivAt_of_bilinear, norm_iteratedFDerivWithin_clm_apply_const, isBoundedBilinearMap_comp, ContinuousAlternatingMap.ofSubsingletonLIE_symm_apply, InnerProductSpace.toDualMap_apply_apply, opNNNorm_prod, ContinuousMultilinearMap.curryRight_norm, MDifferentiableAt.clm_postcomp, Matrix.linfty_opNNNorm_eq_opNNNorm, InnerProductSpace.nnnorm_rankOne, InnerProductSpace.isSymmetricProjection_rankOne_self, HasFTaylorSeriesUpToOn.eventually_hasFDerivAt, hasGradientWithinAt_iff_hasFDerivWithinAt, DoubleCentralizer.nnnorm_def, apply_norm_sq_eq_inner_adjoint_left, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, HasFPowerSeriesOnBall.fderiv_eq, NormedSpace.inclusionInDoubleDual_norm_eq, fderiv_of_bilinear, nnnorm_toSpanSingleton, HasFTaylorSeriesUpToOn.hasFDerivWithinAt, Submodule.adjoint_subtypeL, norm_smulRightL, InnerProductSpace.trace_rankOne, MDifferentiableWithinAt.cle_arrowCongr, MDifferentiableWithinAt.clm_precomp, isBoundedBilinearMap_compMultilinear, compL_apply, HasFPowerSeriesWithinAt.fderivWithin_eq, Matrix.linfty_opNNNorm_toMatrix, IsPositive.conj_adjoint, ContMDiffOn.clm_precomp, InnerProductSpace.adjoint_rankOne, InnerProductSpace.rankOne_eq_zero, lipschitz, InnerProductSpace.inner_right_rankOne_apply, HasFDerivWithinAt.hasGradientWithinAt, fderivWithin_of_bilinear, HasFPowerSeriesOnBall.compContinuousLinearMap, PiTensorProduct.liftIsometry_tprodL, NormedSpace.inclusionInDoubleDual_norm_le, InnerProductSpace.rankOne_eq_rankOne_iff_comm, InnerProductSpace.toDual_apply, precompR_apply, ContinuousAlternatingMap.norm_alternatizeUncurryFinCLM_le, InnerProductSpace.comp_rankOne, OrthonormalBasis.starProjection_eq_sum_rankOne, InnerProductSpace.toDualMap_apply, adjoint_inner_left, FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le, apply_norm_eq_sqrt_inner_adjoint_right, ContinuousMultilinearMap.ofSubsingletonāįµ¢_symm_apply, ContinuousAlternatingMap.ofSubsingletonLIE_apply, continuousMultilinearCurryRightEquiv_symm_apply, opNNNorm_le_bound, IsContMDiffRiemannianBundle.exists_contMDiff, Complex.ofRealCLM_nnnorm, InnerProductSpace.rank_rankOne, ContMDiffOn.cle_arrowCongr, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq_inner, InnerProductSpace.toDual_apply_apply, adjointAux_apply, inner_map_map_iff_adjoint_comp_self, hasFDerivAt_integral_of_dominated_loc_of_lip', InnerProductSpace.rankOne_def, coe_flipāįµ¢', IsStarNormal.ker_adjoint_eq_ker, hasFTaylorSeriesUpToOn_succ_iff_right, coe_flipMultilinearEquiv, ContinuousMultilinearMap.norm_map_init_le, norm_iteratedFDeriv_le_of_bilinear, IsStarNormal.adjoint_apply_eq_zero_iff, norm_precompR_le, isBoundedLinearMap_comp_right, fderivWithin_iteratedFDerivWithin, nnnorm_holder_apply_apply_le, IsBoundedBilinearMap.isBoundedLinearMap_deriv, DoubleCentralizer.nnnorm_fst, contMDiffOn_continuousLinearMapCoordChange, InnerProductSpace.enorm_rankOne, Module.Basis.exists_opNNNorm_le, HasGradientAt.hasFDerivAt, isLeast_opNNNorm, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one, hasFTaylorSeriesUpTo_succ_nat_iff_right, hasFTaylorSeriesUpToOn_succ_nat_iff_right, toPMap_adjoint_eq_adjoint_toPMap_of_dense, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, ContinuousLinearEquiv.lipschitz, opNNNorm_le_bound', NormedSpace.equicontinuous_TFAE, HasFPowerSeriesAt.fderiv_eq, coe_restrictScalarsIsometry, PiTensorProduct.dualSeminorms_bounded, opNNNorm_le_of_unit_nnnorm, IsSelfAdjoint.conj_adjoint, ContinuousMultilinearMap.curryMidEquiv_apply, opNorm_mulLeftRight_apply_le, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_le, InnerProductSpace.nullSubmodule_le_ker_toDualMap_left, PiTensorProduct.injectiveSeminorm_apply, isBoundedLinearMap_comp_left, Matrix.l2_opNNNorm_def, ContMDiffAt.clm_precomp, HasFTaylorSeriesUpToOn.hasFDerivAt, flip_add, isSelfAdjoint_iff', MeasureTheory.L1.nnnorm_Integral_le_one, HasFTaylorSeriesUpToOn.shift_of_succ, ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, le_opNormā, InnerProductSpace.rankOne_def', opNorm_mul_le, apply_norm_eq_sqrt_inner_adjoint_left, Complex.conjCLE_nnorm, MeasureTheory.dist_convolution_le', MDifferentiableOn.cle_arrowCongr, InnerProductSpace.innerSL_norm, DoubleCentralizer.nnnorm_fst_eq_snd, sSup_unit_ball_eq_nnnorm, MDifferentiableAt.clm_precomp, opENorm_comp_le, hasGradientAt_iff_hasFDerivAt, FormalMultilinearSeries.leftInv_coeff_one, mdifferentiableOn_continuousLinearMapCoordChange, InnerProductSpace.isStarProjection_rankOne_self, HasFPowerSeriesAt.hasFDerivAt, eventually_enorm_mfderiv_extChartAt_lt, HasFPowerSeriesWithinOnBall.compContinuousLinearMap, LinearMap.mkContinuousā_norm_le, le_opNNNorm, HasFDerivWithinAt.clm_comp, isBoundedBilinearMap_apply, InnerProductSpace.rankOne_comp_rankOne, InnerProductSpace.rankOne_comp, InnerProductSpace.toMatrix_rankOne, PiTensorProduct.liftIsometry_comp_mapL, InnerProductSpace.isSymmetric_rankOne_self, continuousMultilinearCurryLeftEquiv_apply, restrictScalarsIsometry_toLinearMap, WStarAlgebra.exists_predual, PiTensorProduct.liftIsometry_symm_apply, opNNNorm_mul, Complex.conjCLE_enorm, norm_iteratedFDerivWithin_le_of_bilinear, iteratedFDeriv_succ_eq_comp_right, nnnorm_fderiv_norm_rpow_le, HasStrictFDerivAt.approximates_deriv_on_open_nhds, adjoint_toSpanSingleton, ContinuousMultilinearMap.nnnorm_ofSubsingleton, LinearIsometry.enorm_toContinuousLinearMap, HasFPowerSeriesWithinOnBall.fderivWithin_eq, InnerProductSpace.rankOne_one_right_eq_toSpanSingleton, HasFTaylorSeriesUpToOn.hasStrictFDerivAt, FormalMultilinearSeries.div_le_radius_compContinuousLinearMap, InnerProductSpace.toContinuousLinearMap_toDualMap, nndist_le_opNNNorm, opNorm_lsmul_le, InnerProductSpace.toDual_apply_eq_toDualMap_apply, norm_compL_le, fderivWithin_clm_comp, opNNNorm_mul_flip_apply, HasFPowerSeriesOnBall.hasFDerivAt, MeasureTheory.charFun_eq_charFunDual_toDualMap, opNNNorm_comp_le, ContMDiff.clm_postcomp, MDifferentiableWithinAt.clm_postcomp, orthogonal_range, norm_bilinearRestrictScalars, PiTensorProduct.liftIsometry_apply_apply, ProbabilityTheory.covarianceBilin_map, Unitization.nnnorm_eq_sup, MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux, nnnorm_smulRight_apply, MDifferentiableOn.clm_precomp, adjoint_comp, InnerProductSpace.toLinearMap_rankOne, continuousMultilinearCurryRightEquiv_symm_apply', MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq, opNNNorm_eq_of_bounds, ContinuousMultilinearMap.cpolynomialOn_uncurry_compContinuousLinearMap, ContinuousMultilinearMap.analyticWithinAt_uncurry_compContinuousLinearMap, Submodule.adjoint_orthogonalProjection, hasFDerivWithinAt_iff_hasGradientWithinAt, hasFDerivAt_of_bilinear, opNNNorm_le_of_lipschitz, opNorm_flip, FormalMultilinearSeries.radius_compContinuousLinearMap_le, IsPositive.adjoint_conj, star_eq_adjoint, Complex.imCLM_nnnorm, ProperCone.hyperplane_separation_of_notMem, ContinuousAlternatingMap.curryLeftLI_apply, norm_compSL_le, InnerProductSpace.isIdempotentElem_rankOne_self_iff, coe_flipāįµ¢, opNNNorm_subsingleton, IsSelfAdjoint.adjoint_conj, OrthonormalBasis.sum_rankOne_eq_id, adjoint_inner_right, HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt, norm_smulRightL_le, Complex.imCLM_enorm, coe_symm_flipMultilinearEquiv, VectorFourier.norm_fourierSMulRight_le, ContinuousAlternatingMap.nnnorm_ofSubsingleton, Complex.ofRealCLM_enorm, continuousMultilinearCurryRightEquiv_apply', flipāįµ¢'_symm, HasFiniteFPowerSeriesOnBall.hasFDerivAt, HasFDerivAt.hasGradientAt, isAdjointPair_inner, VectorFourier.norm_fourierPowSMulRight_le, nnnorm_id, ContinuousMultilinearMap.analyticOnNhd_uncurry_compContinuousLinearMap, MDifferentiable.clm_precomp, ContinuousLinearEquiv.nnnorm_symm_pos, FormalMultilinearSeries.enorm_compContinuousLinearMap_le, continuousMultilinearCurryLeftEquiv_symm_apply, iteratedFDeriv_succ_eq_comp_left, opNorm_mulLeftRight_le, Module.Basis.opNNNorm_le, ContMDiffWithinAt.clm_precomp, ContinuousMultilinearMap.ofSubsingletonāįµ¢_apply, norm_iteratedFDerivWithin_fderivWithin, le_opENorm, continuousMultilinearCurryFin1_symm_apply, norm_map_iff_adjoint_comp_self, ContinuousMultilinearMap.cpolynomialAt_uncurry_compContinuousLinearMap, norm_adjoint_comp_self, ContMDiff.clm_precomp, opNorm_lsmul, NormedSpace.double_dual_bound, norm_holderL_le, ContinuousAffineMap.toConstProdContinuousLinearMap_fst, HasFiniteFPowerSeriesOnBall.fderiv_eq, HasFPowerSeriesAt.hasStrictFDerivAt, apply_norm_sq_eq_inner_adjoint_right, MeasureTheory.eLpNorm_le_eLpNorm_fderiv, MeasureTheory.dominatedFinMeasAdditive_weightedSMul, isPositive_adjoint_comp_self, Complex.reCLM_enorm, norm_innerSL_le, ContMDiffWithinAt.cle_arrowCongr, continuousMultilinearCurryRightEquiv_apply, HasFPowerSeriesWithinAt.hasFDerivWithinAt, flipāįµ¢_symm, HasGradientWithinAt.hasFDerivWithinAt, FormalMultilinearSeries.rightInv_coeff_one, norm_holder_apply_apply_le, HasStrictFDerivAt.clm_comp, ContinuousMultilinearMap.analyticOn_uncurry_compContinuousLinearMap, fpowerSeries_apply_one, smulRightL_apply_apply, opNNNorm_mul_apply, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, norm_precompL_le, PiTensorProduct.mapLMultilinear_opNorm, HasCompactSupport.convolution_integrand_bound_right, HasFPowerSeriesWithinOnBall.hasFDerivWithinAt, InnerProductSpace.symm_toEuclideanLin_rankOne, isBoundedBilinearMap_smulRight, ContMDiffAt.cle_arrowCongr, HasFDerivAt.clm_comp, adjoint_innerSL_apply, HasCompactSupport.convolution_integrand_bound_right_of_subset, norm_smulRightL_apply, opNorm_le_boundā, fpowerSeriesBilinear_apply_one, le_opNorm_enorm, norm_iteratedFDeriv_fderiv, coe_mulāįµ¢, innerSL_apply_comp, toSesqForm_apply_norm_le, PiTensorProduct.injectiveSeminorm_def, ContMDiff.cle_arrowCongr, InnerProductSpace.nullSubmodule_le_ker_toDualMap_right, adjoint_adjoint, orthogonal_ker, InnerProductSpace.norm_rankOne, hasFDerivAt_integral_of_dominated_loc_of_lip, ContinuousAffineMap.toConstProdContinuousLinearMap_snd, ContinuousMultilinearMap.curryMidEquiv_symm_apply, ContinuousMultilinearMap.uncurryRight_norm, norm_iteratedFDerivWithin_le_of_bilinear_aux, continuousMultilinearCurryFin1_apply, norm_iteratedFDeriv_clm_apply_const
|
toSeminormedRing š | CompOp | 12 mathmath: mulLeftRight_isBoundedBilinear, mulLeftRight_apply, hasFDerivAt_ringInverse, fderiv_inverse, fderivWithin_inv', opNorm_mulLeftRight_apply_le, hasStrictFDerivAt_ringInverse, opNorm_mulLeftRight_apply_apply_le, hasStrictFDerivAt_inv', opNorm_mulLeftRight_le, hasFDerivAt_inv', fderiv_inv'
|