| Name | Category | Theorems |
|---|
gi π | CompOp | β |
instAddCancelCommMonoid π | CompOp | β |
instAlgebraOfReal π | CompOp | 96 mathmath: Seminorm.isBounded_const, MeasureTheory.mulEquivHaarChar_smul_integral_map, SpectrumRestricts.nnreal_of_nonneg, QuasispectrumRestricts.nnreal_iff, cfcβHom_nnreal_eq_restrict, SpectrumRestricts.nnreal_iff, instStarModuleNNRealReal, Continuous.cfc_nnreal', nnnorm_algebraMap_nnreal, CFC.rpow_def, CFC.rpow_algebraMap, ContinuousOn.cfc_nnreal', IsGreatest.nnnorm_cfc_nnreal, SpectrumRestricts.smul_of_nonneg, algebraMap_eq_coe, norm_algebraMap_nnreal, instContinuousMap.UniqueHom, Seminorm.ball_smul, CStarAlgebra.nnnorm_le_iff_of_nonneg, MeasureTheory.lpNorm_smul_measure_of_ne_zero, cfc_real_eq_nnreal, StarAlgHom.realContinuousMapOfNNReal_apply, CFC.posPart_algebraMap_nnreal, coe_mem_spectrum_real_of_nonneg, CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts, MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul, Seminorm.comp_smul, continuousOn_cfc_nnreal, cfc_nnreal_eq_real, Seminorm.bound_of_continuous, StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal, MeasureTheory.Measure.toSignedMeasure_smul, Continuous.cfc_nnreal_of_mem_nhdsSet, Seminorm.const_isBounded, ContinuousOn.cfc_nnreal_of_mem_nhdsSet, CFC.rpow_neg_one_eq_cfc_inv, IsSelfAdjoint.sq_spectrumRestricts, ContinuousOn.cfc_nnreal, CStarAlgebra.mem_Icc_algebraMap_iff_nnnorm_le, Seminorm.closedBall_smul, nnnorm_cfc_nnreal_lt, nnnorm_cfc_nnreal_le, cfc_nnreal_le_iff, Continuous.cfc_nnreal, nnnorm_cfc_nnreal_le_iff, Nonneg.instContinuousFunctionalCalculus, spectralRadius_mem_spectrum, CFC.spectrum_rpow, cfcHom_nnreal_eq_restrict, upperHemicontinuous_spectrum_nnreal, range_cfc_nnreal, Unitization.nnreal_cfcβ_eq_cfc_inr, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul, CFC.abs_algebraMap_nnreal, apply_le_nnnorm_cfc_nnreal, range_cfc_nnreal_eq_image_cfc_real, MeasureTheory.SignedMeasure.singularPart_smul_nnreal, MeasureTheory.JordanDecomposition.toSignedMeasure_smul, StarAlgHom.realContinuousMapOfNNReal_injective, Seminorm.bound_of_shell_sup, Seminorm.finset_sup_smul, Seminorm.isBounded_sup, CFC.sqrt_eq_cfc, QuasispectrumRestricts.nnreal_of_nonneg, Filter.Tendsto.cfc_nnreal, CompactlySupportedContinuousMap.toReal_smul, spectrum.isCompact_nnreal, Seminorm.bound_of_shell_smul, CFC.sqrt_algebraMap, cfc_tsub, ContinuousLinearMap.IsPositive.spectrumRestricts, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, spectrum.instCompactSpaceNNReal, nnnorm_cfc_nnreal_lt_iff, Commute.cfc_nnreal, MonotoneOn.nnnorm_cfc, LinearMap.mem_span_iff_bound, SpectrumRestricts.nnreal_iff_spectralRadius_le, ContinuousMapZero.toNNReal_neg_smul, continuousOn_cfc_nnreal_setProd, CStarAlgebra.nonneg_TFAE, MeasureTheory.lpNorm_smul_measure_of_ne_top, ContinuousMapZero.toNNReal_smul, ContinuousAt.cfc_nnreal, ContinuousWithinAt.cfc_nnreal, ENNReal.toReal_smul, range_cfc_nnreal_subset, IsometricContinuousFunctionalCalculus.isGreatest_spectrum, MeasureTheory.integral_comap_eq_mulEquivHaarChar_smul, CStarAlgebra.nnnorm_mem_spectrum_of_nonneg, SpectrumRestricts.nnreal_iff_nnnorm, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, Seminorm.smul_le_smul, MeasureTheory.addEquivAddHaarChar_smul_integral_map, SpectrumRestricts.nnreal_add, Nonneg.instIsometricContinuousFunctionalCalculus
|
instArchimedean π | CompOp | β |
instCanonicallyOrderedAdd π | CompOp | β |
instCoeReal π | CompOp | β |
instCommMonoidWithZero π | CompOp | β |
instCommSemiring π | CompOp | 315 mathmath: range_cfcβ_nnreal, MeasureTheory.Measure.MutuallySingular.smul_nnreal, Seminorm.isBounded_const, MeasureTheory.Measure.IsHaarMeasure.nnreal_smul, MeasureTheory.mulEquivHaarChar_smul_integral_map, MeasureTheory.Measure.isAddInvariant_eq_smul_of_compactSpace, CFC.monotoneOn_one_sub_one_add_inv, MeasureTheory.integral_smul_nnreal_measure, nnnorm_cfcβ_nnreal_le_iff, MeasureTheory.Measure.WeaklyRegular.smul_nnreal, ENNReal.nnreal_smul_lt_top, MeasureTheory.Measure.rnDeriv_smul_right', MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply, Commute.cfcβ_nnreal, MeasureTheory.llr_smul_nnreal_same, MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top, MeasureTheory.smul_le_stoppedValue_hittingBtwn, QuasispectrumRestricts.nnreal_iff, InformationTheory.klDiv_smul_right_eq_smul_left, MeasureTheory.Measure.haveLebesgueDecompositionSMul, MeasureTheory.le_eLpNorm_of_bddBelow, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal, MeasureTheory.Measure.coe_nnreal_smul_apply, segment_eq_uIcc, MeasureTheory.eLpNorm_smul_measure_of_ne_top', MeasureTheory.Measure.rnDeriv_smul_right, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum, MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound, MeasureTheory.Measure.haarScalarFactor_smul, MeasureTheory.Measure.OuterRegular.smul_nnreal, NumberField.mixedEmbedding.convexBodyLT_volume, instStarModuleNNRealReal, isBoundedSMul, Continuous.cfc_nnreal', nnnorm_algebraMap_nnreal, spectrum_nonempty, CFC.rpow_def, ContinuousAlternatingMap.le_opNNNorm, ContinuousMultilinearMap.le_of_opNNNorm_le, MeasureTheory.Measure.integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport, CFC.rpow_algebraMap, Real.toNNReal_prod_of_nonneg, ediam_smul_le, ContinuousOn.cfc_nnreal', IsGreatest.nnnorm_cfc_nnreal, algebraMap_eq_coe, norm_algebraMap_nnreal, MeasureTheory.addEquivAddHaarChar_smul_preimage, MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN, ENNReal.instSMulPosMonoNNReal, instContinuousMap.UniqueHom, MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto, MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul, strictConcaveOn_sqrt, ContinuousMap.toNNReal_algebraMap, Seminorm.ball_smul, coe_prod, MeasureTheory.Measure.smul_measure_isAddInvariant_le_of_isCompact_closure, SimpleGraph.binomialRandom_apply, nnnorm_cfcβ_nnreal_lt, CStarAlgebra.nnnorm_le_iff_of_nonneg, MeasureTheory.Measure.measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport, MeasureTheory.lpNorm_smul_measure_of_ne_zero, cfc_real_eq_nnreal, StarAlgHom.realContinuousMapOfNNReal_apply, ProbabilityTheory.setBernoulli_apply', MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalize, MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul', coe_multiset_prod, MeasureTheory.FiniteMeasure.pi_pi, infEDist_smulβ, MeasureTheory.ProbabilityMeasure.pi_pi, MeasureTheory.mulEquivHaarChar_smul_map, CFC.posPart_algebraMap_nnreal, MeasureTheory.FiniteMeasure.map_fst_prod, coe_mem_spectrum_real_of_nonneg, CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts, FormalMultilinearSeries.compAlongComposition_nnnorm, MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul, MeasureTheory.Measure.hausdorffMeasure_smulβ, Finset.nnnorm_prod_le', Seminorm.comp_smul, IsGreatest.nnnorm_cfcβ_nnreal, MeasureTheory.SMul.sigmaFinite, MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegular, ENNReal.prod_coe_rpow, continuousOn_cfc_nnreal, cfc_nnreal_eq_real, Seminorm.bound_of_continuous, MeasureTheory.Measure.rnDeriv_smul_left', MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul', CFC.nnrpow_def, MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular, instStarOrderedRing, StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal, Nonneg.instNonUnitalIsometricContinuousFunctionalCalculus, MeasureTheory.Measure.toSignedMeasure_smul, Continuous.cfc_nnreal_of_mem_nhdsSet, MeasureTheory.hausdorffMeasure_lineMap_image, Continuous.cfcβ_nnreal, infEdist_smulβ, NumberField.mixedEmbedding.adjust_f, MeasureTheory.FiniteMeasure.instContinuousSMulNNReal, ContinuousAt.cfcβ_nnreal, MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul, MeasureTheory.Measure.measure_isAddHaarMeasure_eq_smul_of_isOpen, Seminorm.const_isBounded, ContinuousOn.cfc_nnreal_of_mem_nhdsSet, MeasureTheory.Measure.rnDeriv_smul_same, MeasureTheory.Measure.instSMulCommClassDomMulActNNReal, MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure, ENNReal.nnreal_smul_lt_top_iff, cfcβ_tsub, CFC.rpow_neg_one_eq_cfc_inv, ContinuousWithinAt.cfcβ_nnreal, MeasureTheory.smul_le_stoppedValue_hitting, MeasureTheory.Measure.isMulInvariant_eq_smul_of_compactSpace, MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, ENNReal.coe_finset_prod, MeasureTheory.llr_smul_nnreal_left, range_cfcβ_nnreal_eq_image_cfcβ_real, Filter.Tendsto.cfcβ_nnreal, MeasureTheory.JordanDecomposition.smul_posPart, edist_smulβ, MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure, MeasureTheory.FiniteMeasure.smul_testAgainstNN_apply, ContinuousOn.cfc_nnreal, nnnorm_cfcβ_nnreal_lt_iff, MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isEverywherePos, MeasureTheory.Measure.nnreal_smul_coe_apply, CStarAlgebra.mem_Icc_algebraMap_iff_nnnorm_le, MeasureTheory.euclideanHausdorffMeasure_homothety_image, Seminorm.closedBall_smul, nnnorm_cfc_nnreal_lt, MeasureTheory.euclideanHausdorffMeasure_homothety_preimage, MeasureTheory.Measure.addHaarScalarFactor_smul_smul, MeasureTheory.JordanDecomposition.real_smul_posPart_nonneg, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply, MeasureTheory.hausdorffMeasure_homothety_image, cfcβ_real_eq_nnreal, nnnorm_cfc_nnreal_le, ContinuousOn.cfcβ_nnreal_of_mem_nhdsSet, MeasureTheory.Measure.smul_measure_isMulInvariant_le_of_isCompact_closure, cfc_nnreal_le_iff, Continuous.cfc_nnreal, MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_nonzero, MeasureTheory.Measure.measure_isAddHaarMeasure_eq_smul_of_isEverywherePos, nnnorm_cfc_nnreal_le_iff, MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal, MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet, Nonneg.instContinuousFunctionalCalculus, MeasureTheory.FiniteMeasure.normalize_eq_inv_mass_smul_of_nonzero, MeasureTheory.Measure.instSMulCommClassNNRealDomMulAct, ContinuousMapZero.toContinuousMapHom_toNNReal, MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply, spectralRadius_mem_spectrum, CFC.spectrum_rpow, MeasureTheory.Measure.map_right_mul_eq_modularCharacterFun_smul, MeasureTheory.addEquivAddHaarChar_smul_map, upperHemicontinuous_spectrum_nnreal, MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN, ContinuousOn.cfcβ_nnreal', MeasureTheory.isMulLeftInvariant_smul_nnreal, NumberField.mixedEmbedding.convexBodyLT'_volume, range_cfc_nnreal, Unitization.nnreal_cfcβ_eq_cfc_inr, MeasureTheory.instIsProbabilityMeasureHAddMeasureHSMulNNRealToNNRealSymm, MeasureTheory.hausdorffMeasure_smul_right_image, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul, InformationTheory.toReal_klDiv_smul_right_eq_smul_left, MeasureTheory.Measure.measure_isAddLeftInvariant_eq_vadd_of_ne_top, CFC.abs_algebraMap_nnreal, upperHemicontinuous_quasispectrum_nnreal, MeasureTheory.Measure.mul_addHaarScalarFactor_smul, geom_mean_le_arith_mean_weighted, MeasureTheory.Measure.integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, Continuous.cfcβ_nnreal_of_mem_nhdsSet, instMeasurableSMulβENNReal, MeasureTheory.Measure.isMulLeftInvariant_eq_smul, InformationTheory.toReal_klDiv_smul_right, apply_le_nnnorm_cfc_nnreal, segment_eq_Icc, range_cfc_nnreal_eq_image_cfc_real, MeasureTheory.VAddInvariantMeasure.vadd_nnreal, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective, MeasureTheory.SignedMeasure.singularPart_smul_nnreal, MeasureTheory.Measure.InnerRegular.smul_nnreal, MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.isAddRightInvariant_smul_nnreal, range_cfcβ_nnreal_subset, MeasureTheory.SMulInvariantMeasure.smul_nnreal, MeasureTheory.mulEquivHaarChar_smul_preimage, MeasureTheory.JordanDecomposition.toSignedMeasure_smul, StarAlgHom.realContinuousMapOfNNReal_injective, MeasureTheory.Measure.measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport, ENNReal.toNNReal_prod, Nonneg.instNonUnitalContinuousFunctionalCalculus, convex_setOf_holderWith, MeasureTheory.JordanDecomposition.real_smul_posPart_neg, MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_regular, ediam_smulβ, finset_prod_rpow, Seminorm.bound_of_shell_sup, ContinuousMultilinearMap.opNNNorm_le_iff, MeasureTheory.FiniteMeasure.map_smul, Seminorm.finset_sup_smul, quasispectrum.isCompact_nnreal, Seminorm.isBounded_sup, CFC.sqrt_eq_cfc, InformationTheory.toReal_klDiv_smul_same, MeasureTheory.addEquivAddHaarChar_smul_eq_comap, QuasispectrumRestricts.nnreal_of_nonneg, Filter.Tendsto.cfc_nnreal, CompactlySupportedContinuousMap.toReal_smul, norm_cfcβ_one_sub_one_add_inv_lt_one, continuousOn_cfcβ_nnreal, MeasureTheory.mulEquivHaarChar_smul_eq_comap, MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous, MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_innerRegular, MeasureTheory.JordanDecomposition.real_smul_negPart_neg, spectrum.isCompact_nnreal, AlternatingMap.measure_def, Seminorm.bound_of_shell_smul, MeasureTheory.Measure.haarScalarFactor_smul_smul, MeasureTheory.Measure.rnDeriv_smul_left, MeasureTheory.Measure.exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport, cfcβ_nnreal_eq_real, CFC.sqrt_algebraMap, cfc_tsub, ENNReal.smul_toNNReal, StieltjesFunction.measure_smul, MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, spectrum.instCompactSpaceNNReal, MeasureTheory.Measure.Regular.smul_nnreal, nnnorm_cfc_nnreal_lt_iff, MeasureTheory.isLocallyFiniteMeasureSMulNNReal, MeasureTheory.isFiniteMeasureSMulNNReal, MeasureTheory.Integrable.smul_measure_nnreal, MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop, Commute.cfc_nnreal, MeasureTheory.Measure.InnerRegularCompactLTTop.smul_nnreal, MonotoneOn.nnnorm_cfc, convex_setOf_holderOnWith, MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN, LinearMap.mem_span_iff_bound, ContinuousOn.cfcβ_nnreal, MeasureTheory.Measure.IsEverywherePos.smul_measure_nnreal, MeasureTheory.Measure.haveLebesgueDecompositionSMulRight, Finset.nnnorm_prod_le, MeasureTheory.Measure.IsAddHaarMeasure.nnreal_smul, instContinuousMapZero.UniqueHom, MeasureTheory.Measure.mul_haarScalarFactor_smul, ContinuousMapZero.toNNReal_neg_smul, continuousOn_cfc_nnreal_setProd, MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure_of_measurableSet, CStarAlgebra.nonneg_TFAE, MeasureTheory.lpNorm_smul_measure_of_ne_top, ContinuousAlternatingMap.opNNNorm_le_iff, nnnorm_prod, MeasureTheory.JordanDecomposition.real_smul_negPart_nonneg, ContinuousMapZero.toNNReal_smul, MeasureTheory.Measure.euclideanHausdorffMeasure_smulβ, MeasureTheory.isMulRightInvariant_smul_nnreal, MeasureTheory.isAddLeftInvariant_smul_nnreal, MeasureTheory.Measure.map_right_add_eq_addModularCharacterFun_vadd, MeasureTheory.hausdorffMeasure_homothety_preimage, ContinuousAt.cfc_nnreal, MeasureTheory.FiniteMeasure.map_snd_prod, ENNReal.instMeasurableSMulNNReal, MeasureTheory.eLpNorm_smul_measure_of_ne_zero', quasispectrum.instCompactSpaceNNReal, multiset_prod_map_rpow, MeasureTheory.OuterMeasure.mkMetric_nnreal_smul, ContinuousMultilinearMap.le_opNNNorm, MeasureTheory.Measure.singularPart_smul_right, ContinuousWithinAt.cfc_nnreal, nnnorm_cfcβ_nnreal_le, ENNReal.instPosSMulStrictMonoNNReal, apply_le_nnnorm_cfcβ_nnreal, MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN, continuousOn_cfcβ_nnreal_setProd, ENNReal.toReal_smul, strictConcaveOn_rpow, MeasureTheory.Measure.isAddLeftInvariant_eq_smul, ProbabilityTheory.setBernoulli_apply, edist_smul_le, MonotoneOn.nnnorm_cfcβ, range_cfc_nnreal_subset, IsometricContinuousFunctionalCalculus.isGreatest_spectrum, InformationTheory.klDiv_smul_same, MeasureTheory.Measure.addHaarScalarFactor_smul, MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul, InformationTheory.toReal_klDiv_smul_left, MeasureTheory.integral_comap_eq_mulEquivHaarChar_smul, CStarAlgebra.nnnorm_mem_spectrum_of_nonneg, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, MeasureTheory.llr_smul_nnreal_right, MeasureTheory.Measure.singularPart_smul, MeasureTheory.Measure.coe_nnreal_smul, MeasureTheory.Measure.euclideanHausdorffMeasure_def, Seminorm.smul_le_smul, MeasureTheory.addEquivAddHaarChar_smul_integral_map, MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop, MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto, MeasureTheory.measureReal_nnreal_smul_apply, MeasureTheory.FiniteMeasure.mass_pi, Continuous.cfcβ_nnreal', ContinuousAlternatingMap.le_of_opNNNorm_le, Nonneg.instIsometricContinuousFunctionalCalculus, HasSum.isProbabilityMeasure_sum_dirac_nnreal, Icc_subset_segment, concaveOn_rpow, ProbabilityTheory.setBernoulli_eq_map, MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isOpen
|
instConditionallyCompleteLinearOrderBot π | CompOp | 63 mathmath: ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm, iSup_of_not_bddAbove, ENNReal.ofNNReal_limsup, mul_iSup_le, ContinuousLinearMap.nnnorm_def, coe_sSup, limsInf_of_not_isCobounded, segment_eq_uIcc, coe_iSup, ENNReal.toNNReal_sSup, ContinuousLinearMap.sSup_sphere_eq_nnnorm, iSup_eq_zero, natCast_iInf, ENNReal.coe_sSup, image_coe_uIcc, PseudoMetricSpace.dist_ofPreNNDist, iSup_mul_iSup_le, agm_eq_ciSup, ENNReal.toNNReal_iSup, sSup_of_not_bddAbove, iSup_pow_of_ne_zero, ENNReal.coe_essSup, PiLp.nnnorm_eq_ciSup, ENNReal.toNNReal_iInf, le_iInf_mul_iInf, iSup_div, ENNReal.ofNNReal_liminf, BoundedContinuousFunction.nndist_eq_iSup, natCast_iSup, ContinuousLinearMap.sSup_unit_ball_eq_nnnorm, le_mul_iInf, BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm, ContinuousMap.nnnorm_eq_iSup_nnnorm, ContinuousMap.nndist_eq_iSup, limsSup_of_not_isBounded, coe_iInf, limsup_of_not_isBoundedUnder, iSup_empty, IsUltrametricDist.nnnorm_tprod_le, mul_iSup, BoundedContinuousFunction.nndist_eq, liminf_of_not_isCoboundedUnder, sInf_empty, mul_iInf, toReal_limsup, iInf_mul, iInf_empty, le_iInf_add_iInf, agm_eq_ciInf, toReal_liminf, ENNReal.toNNReal_sInf, ENNReal.coe_iInf, le_iInf_mul, iSup_mul, iSup_pow, ENNReal.coe_iSup, ENNReal.image_coe_uIcc, ENNReal.coe_sInf, iSup_mul_le, iInf_const_zero, IsUltrametricDist.nnnorm_tsum_le, PiLp.nndist_eq_iSup, coe_sInf
|
instDenselyOrdered π | CompOp | β |
instDistribLattice π | CompOp | β |
instDistribMulActionOfReal π | CompOp | 32 mathmath: MeasureTheory.integral_smul_nnreal_measure, setIntegral_withDensity_eq_setIntegral_smulβ, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal, instStarModuleNNRealOfReal, integral_withDensity_eq_integral_smul, setIntegral_withDensity_eq_setIntegral_smulβ', CFC.posPart_smul, MeasureTheory.integrable_withDensity_iff_integrable_smulβ, MeasureTheory.Measure.toSignedMeasure_smul, MeasureTheory.memL1_smul_of_L1_withDensity, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply, MeasureTheory.integrable_withDensity_iff_integrable_smul, ConvexBody.smul_le_of_le, convex_iff, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul, setIntegral_withDensity_eq_setIntegral_smul, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective, MeasureTheory.SignedMeasure.singularPart_smul_nnreal, MeasureTheory.JordanDecomposition.toSignedMeasure_smul, MeasureTheory.withDensitySMulLI_apply, MeasureTheory.Measure.addHaar_nnreal_smul, CompactlySupportedContinuousMap.toReal_smul, MeasureTheory.withDensityα΅₯_smul_eq_withDensityα΅₯_withDensity, sub_mem_posTangentConeAt_of_openSegment_subset, instIsStrictOrderedModule, ContinuousMapZero.toNNReal_neg_smul, CFC.negPart_smul, ContinuousMapZero.toNNReal_smul, integral_withDensity_eq_integral_smulβ, ProbabilityTheory.Kernel.integral_withDensity, ConvexBody.coe_smul', MeasureTheory.SignedMeasure.toJordanDecomposition_smul
|
instDiv π | CompOp | 68 mathmath: rpow_sub_intCast, HolderTriple.one_div_nonneg', sqrt_mul_lt_half_add_of_ne, div_lt_one_of_lt, agmSequences_zero, coe_div, half_le_self, young_inequality, nnnorm_div, CFC.abs_nnrpow, nndist_inv_invβ, Real.toNNReal_div, rpow_sub_natCast, ENNReal.toNNReal_div, rpow_sub, rpow_sub', UpperHalfPlane.volume_def, holderConjugate_one_div, CFC.sqrt_eq_nnrpow, PadicAlgCl.valuation_p, PadicComplex.valuation_p, nndist_midpoint_midpoint_le', Real.toNNReal_div', Delone.DeloneSet.mapBilipschitz_packingRadius, ProbabilityTheory.gaussianReal_map_div_const, agm_eq_agm_gm_am, le_gm_and_am_le, UpperHalfPlane.volume_eq_lintegral, HolderTriple.one_div_nonneg, CFC.nnrpow_sqrt, iSup_div, sub_div, HolderTriple.holderConjugate_div_div, HolderConjugate.conjugate_eq, rpow_sub_one, rpow_one_sub', holderConjugate_iff_eq_conjExponent, Metric.coveringNumber_subset_le, div_le_of_le_mul, half_lt_self, nndist_midpoint_midpoint_le, HasStrictFDerivAt.approximates_deriv_on_open_nhds, HolderTriple.one_div_eq, div_le_of_le_mul', summable_one_div_rpow, rpow_sub_one', rpow_sub_natCast', HolderConjugate.div_conj_eq_sub_one, CFC.sqrt_nnrpow, HolderTriple.one_div_add_one_div, ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero, HolderTriple.one_div_pos, sqrt_div, ENNReal.coe_div_le, agmSequences_succ', div_rpow, ProbabilityTheory.gaussianReal_div_const, sqrt_mul_le_half_add, Metric.IsSeparated.image_antilipschitz, ENNReal.coe_div, dist_gm_am_le, ENNReal.coe_div', agmSequences_succ, young_inequality_real, rpow_sub_intCast', ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc, HolderTriple.one_div_pos', finset_sup_div
|
instInhabited π | CompOp | β |
instInv π | CompOp | 93 mathmath: nnnorm_inv, tsum_geometric, HolderTriple.inv_eq, CFC.monotoneOn_one_sub_one_add_inv, MeasureTheory.Measure.rnDeriv_smul_right', ENNReal.coe_inv, AntilipschitzWith.mul_le_nndist, InformationTheory.klDiv_smul_right_eq_smul_left, MeasureTheory.mulEquivHaarChar_symm, MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar_inv, nndist_midpoint_right, MeasureTheory.Measure.rnDeriv_smul_right, AntilipschitzWith.mul_le_dist, Dilation.antilipschitz, FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto, HolderTriple.of_pos, MeasureTheory.FiniteMeasure.normalize_eq_of_nonzero, antilipschitzWith_mul_right, HolderConjugate.inv_add_inv_eq_one, HolderTriple.inv_sub_inv_eq_inv, rpow_neg_one, lipschitzWith_thickenedIndicator, HolderTriple.inv_nonneg, AntilipschitzWith.mul_div_lipschitzWith, ENNReal.coe_inv', HolderTriple.inv_inv_add_inv, CFC.nnrpow_inv_nnrpow, nndist_left_midpoint, inv_rpow, Real.toNNReal_inv, FormalMultilinearSeries.inv_le_ofScalars_radius_of_tendsto, nndist_midpoint_left, DilationEquiv.ratio_inv, CFC.rpow_neg_one_eq_cfc_inv, instContinuousInvβ, AntilipschitzWith.mul_lipschitzWith, HolderConjugate.one_sub_inv_inv, hasSum_geometric, MeasureTheory.euclideanHausdorffMeasure_homothety_preimage, Set.InvOn.one_sub_one_add_inv, ApproximatesLinearOn.antilipschitz, ENNReal.coe_inv_two, MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_nonzero, MeasureTheory.FiniteMeasure.normalize_eq_inv_mass_smul_of_nonzero, coe_inv, CFC.nnrpow_inv_eq, lt_inv_iff_mul_lt, ProbabilityTheory.cauchyPDFReal_def', HolderConjugate.inv_inv, ENNReal.coe_inv_le, HolderTriple.inv_add_inv_eq_inv, InformationTheory.toReal_klDiv_smul_right_eq_smul_left, le_inv_iff_mul_le, HasStrictFDerivAt.approximates_deriv_on_open_nhds, inv_lt_inv, HolderConjugate.one_sub_inv, antilipschitzWith_mul_left, rpow_neg, ApproximatesLinearOn.closedBall_subset_target, MeasureTheory.FiniteMeasure.normalize_testAgainstNN, HolderConjugate.inv_one_sub_inv, HolderTriple.inv_pos', inv_le, nnnorm_commutator_sub_one_le, summable_rpow_inv, Convex.lipschitzWith_gauge, norm_cfcβ_one_sub_one_add_inv_lt_one, HolderTriple.inv_pos, inv_le_of_le_mul, HolderTriple.inv_nonneg', exists_nat_pos_inv_lt, CFC.nnrpow_nnrpow_inv, MeasureTheory.addEquivAddHaarChar_symm, HolderConjugate.inv_add_inv_ennreal, DilationEquiv.ratio_symm, MeasureTheory.hausdorffMeasure_homothety_preimage, nndist_right_midpoint, antilipschitzWith_lineMap, HolderTriple.inv_lt_inv, holderConjugate_iff, inv_lt_one_iff, FormalMultilinearSeries.ofScalars_radius_ge_inv_of_tendsto, sqrt_inv, AntilipschitzWith.add_sub_lipschitzWith, tsum_geometric_nnreal, Mathlib.Meta.NormNum.nnreal_rpow_isRat_eq_inv_nnreal_rpow, ENNReal.toNNReal_inv, egauge_le_of_smul_mem_of_ne, AntilipschitzWith.add_lipschitzWith, ApproximatesLinearOn.to_inv, Mathlib.Meta.NormNum.IsInt.nnreal_rpow_eq_inv_nnreal_pow, holderTriple_iff, ContinuousLinearMap.antilipschitz_of_forall_le_inner_map
|
instIsOrderedRing π | CompOp | β |
instIsStrictOrderedRing π | CompOp | 1 mathmath: coe_expect
|
instLinearOrder π | CompOp | 7 mathmath: image_coe_uIoc, ENNReal.image_coe_uIoc, IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbvDef, ENNReal.image_coe_uIoo, IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDef, ENNReal.coe_rpow_def, image_coe_uIoo
|
instLinearOrderedCommGroupWithZero π | CompOp | 45 mathmath: PadicComplex.valuation_extends, PadicComplex.charZero, PadicComplex.coe_eq, PadicComplex.norm_eq_norm, PadicComplex.coe_natCast, Valued.integer.exists_norm_lt_one, Valued.integer.norm_irreducible_lt_one, WithZeroMulInt.toNNReal_lt_one_iff, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, PadicAlgCl.instUniformContinuousConstSMulPadic, PadicAlgCl.valuation_p, PadicComplex.valuation_p, PadicComplex.norm_extends', WithZeroMulInt.toNNReal_le_one_iff, Valued.integer.norm_le_one, PadicComplex.isNonarchimedean, ModP.preVal_mk, ModP.v_p_lt_preVal, PadicComplex.instIsScalarTowerPadicPadicAlgCl, Valued.integer.coe_span_singleton_eq_closedBall, PadicComplex.norm_eq_norm', Valued.integer.norm_unit, PadicAlgCl.valuation_def, Delone.DeloneSet.mapBilipschitz_trans, PadicAlgCl.valuation_coe, PadicComplex.coe_zero, Valued.integer.exists_nnnorm_lt_one, NormedField.v_eq_valuation, PadicComplex.RankOne.hom_eq_embedding, WithZeroMulInt.toNNReal_strictMono, PadicComplex.norm_extends, Valued.integer.mem_iff, Irreducible.maximalIdeal_eq_closedBall, Valued.integer.isUnit_iff_norm_eq_one, ModP.v_p_lt_val, PreTilt.map_eq_zero, Irreducible.maximalIdeal_pow_eq_closedBall_pow, PadicComplex.nnnorm_extends', NormedField.valuation_apply, Valued.integer.norm_coe_unit, PadicComplex.nnnorm_extends, Valued.integer.exists_norm_coe_lt_one, PadicComplexInt.integers, PadicComplex.isAlgClosed, Valued.integer.norm_irreducible_pos
|
instModuleOfReal π | CompOp | 47 mathmath: range_cfcβ_nnreal, CFC.monotoneOn_one_sub_one_add_inv, nnnorm_cfcβ_nnreal_le_iff, Commute.cfcβ_nnreal, QuasispectrumRestricts.nnreal_iff, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum, cfcβHom_nnreal_eq_restrict, CompactlySupportedContinuousMap.toRealLinearMap_apply_apply, nnnorm_cfcβ_nnreal_lt, CompactlySupportedContinuousMap.coe_toRealLinearMap, CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts, IsGreatest.nnnorm_cfcβ_nnreal, CompactlySupportedContinuousMap.toRealLinearMap_apply, CFC.nnrpow_def, Nonneg.instNonUnitalIsometricContinuousFunctionalCalculus, Continuous.cfcβ_nnreal, ContinuousAt.cfcβ_nnreal, cfcβ_tsub, ContinuousWithinAt.cfcβ_nnreal, range_cfcβ_nnreal_eq_image_cfcβ_real, Filter.Tendsto.cfcβ_nnreal, nnnorm_cfcβ_nnreal_lt_iff, cfcβ_real_eq_nnreal, ContinuousOn.cfcβ_nnreal_of_mem_nhdsSet, InnerProductGeometry.angle_eq_angle_add_angle_iff, ContinuousOn.cfcβ_nnreal', Unitization.nnreal_cfcβ_eq_cfc_inr, upperHemicontinuous_quasispectrum_nnreal, Continuous.cfcβ_nnreal_of_mem_nhdsSet, range_cfcβ_nnreal_subset, Nonneg.instNonUnitalContinuousFunctionalCalculus, quasispectrum.isCompact_nnreal, QuasispectrumRestricts.nnreal_of_nonneg, norm_cfcβ_one_sub_one_add_inv_lt_one, continuousOn_cfcβ_nnreal, cfcβ_nnreal_eq_real, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, signedDist_eq_dist_iff_vsub_mem_span, ContinuousOn.cfcβ_nnreal, instContinuousMapZero.UniqueHom, CStarAlgebra.nonneg_TFAE, quasispectrum.instCompactSpaceNNReal, nnnorm_cfcβ_nnreal_le, apply_le_nnnorm_cfcβ_nnreal, continuousOn_cfcβ_nnreal_setProd, MonotoneOn.nnnorm_cfcβ, Continuous.cfcβ_nnreal'
|
instMulActionOfReal π | CompOp | 19 mathmath: Seminorm.isBounded_const, instPosSMulStrictMono, Seminorm.ball_smul, Seminorm.comp_smul, smulCommClass_left, Seminorm.bound_of_continuous, Seminorm.const_isBounded, Seminorm.closedBall_smul, smul_def, smulCommClass_right, instContinuousSMulOfReal, Seminorm.bound_of_shell_sup, Seminorm.finset_sup_smul, Seminorm.isBounded_sup, Seminorm.bound_of_shell_smul, LinearMap.mem_span_iff_bound, instSMulPosStrictMono, Seminorm.smul_le_smul, instIsScalarTowerOfReal
|
instMulArchimedean π | CompOp | β |
instNNRatCast π | CompOp | 5 mathmath: Real.nnnorm_nnratCast, RCLike.nnnorm_nnratCast, coe_ofScientific, Complex.nnnorm_nnratCast, ENNReal.coe_nnratCast
|
instNoZeroDivisors π | CompOp | β |
instNontrivial π | CompOp | 31 mathmath: range_cfcβ_nnreal, CFC.monotoneOn_one_sub_one_add_inv, nnnorm_cfcβ_nnreal_le_iff, Commute.cfcβ_nnreal, nnnorm_cfcβ_nnreal_lt, IsGreatest.nnnorm_cfcβ_nnreal, CFC.nnrpow_def, Nonneg.instNonUnitalIsometricContinuousFunctionalCalculus, Continuous.cfcβ_nnreal, ContinuousAt.cfcβ_nnreal, cfcβ_tsub, ContinuousWithinAt.cfcβ_nnreal, range_cfcβ_nnreal_eq_image_cfcβ_real, Filter.Tendsto.cfcβ_nnreal, nnnorm_cfcβ_nnreal_lt_iff, cfcβ_real_eq_nnreal, ContinuousOn.cfcβ_nnreal_of_mem_nhdsSet, ContinuousOn.cfcβ_nnreal', Unitization.nnreal_cfcβ_eq_cfc_inr, Continuous.cfcβ_nnreal_of_mem_nhdsSet, range_cfcβ_nnreal_subset, Nonneg.instNonUnitalContinuousFunctionalCalculus, norm_cfcβ_one_sub_one_add_inv_lt_one, continuousOn_cfcβ_nnreal, cfcβ_nnreal_eq_real, ContinuousOn.cfcβ_nnreal, nnnorm_cfcβ_nnreal_le, apply_le_nnnorm_cfcβ_nnreal, continuousOn_cfcβ_nnreal_setProd, MonotoneOn.nnnorm_cfcβ, Continuous.cfcβ_nnreal'
|
instOne π | CompOp | 276 mathmath: MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasure, LipschitzWith.id, Complex.nnnorm_exp_I_mul_ofReal, List.nnnorm_prod, tsum_geometric, LipschitzWith.prodMk_right, Dilation.ratio_one, HolderTriple.one_div_nonneg', Orthonormal.nnnorm_eq_one, ENNReal.coe_eq_one, CFC.monotoneOn_one_sub_one_add_inv, LinearIsometry.nnnorm_toContinuousLinearMap, LinearIsometry.lipschitz, Real.nnnorm_deriv_mulExpNegMulSq_le_one, ENNReal.toNNReal_eq_one_iff, OrthonormalBasis.nnnorm_eq_one, LipschitzWith.mk_one, NumberField.mixedEmbedding.one_le_convexBodyLTFactor, thickenedIndicator_one_of_mem_closure, LipschitzWith.prod_snd, rpow_lt_one, LinearIsometryEquiv.antilipschitz, LipschitzWith.holderWith, IsometryClass.lipschitz, EMetric.NonemptyCompacts.lipschitz_prod, Complex.lipschitz_equivRealProd, PMF.support_bernoulli, List.nnnorm_prod_le', TopologicalSpace.Compacts.lipschitz_prod, coe_le_one, IsometryClass.antilipschitz, AntilipschitzWith.id, div_lt_one_of_lt, MeasureTheory.ProbabilityMeasure.range_toFiniteMeasure, NormedField.exists_nnnorm_lt_one, Dilation.ratio_id, CStarAlgebra.mem_Icc_iff_nnnorm_le_one, UniformOnFun.lipschitzWith_one_ofFun_toFun, Complex.reCLM_nnnorm, IsometryEquiv.toDilationEquiv_ratio, ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm, CFC.nnrpow_one, one_le_rpow, nnnorm_one, rpow_le_one_of_one_le_of_nonpos, lipschitzWith_sup_right, HasOuterApproxClosed.tendsto_apprSeq, LipschitzWith.of_edist_le, TopologicalSpace.Compacts.lipschitz_sup, SemilinearIsometryClass.lipschitz, thickenedIndicator_le_one, PiLp.antilipschitzWith_toLp, isGreatest_Lp, Real.one_lt_toNNReal, LipschitzWith.dist_left, List.nnnorm_prod_le, HolderConjugate.inv_add_inv_eq_one, LipschitzWith.of_le_add, rpow_inv_rpow_eq_iff, lipschitzOnWith_cfc_fun_of_subset, Real.toNNReal_le_one, AffineIsometry.lipschitz, WithZeroMulInt.toNNReal_lt_one_iff, LipschitzWith.prod_fst, MeasureTheory.Measure.addModularCharacterFun_map_zero, LipschitzWith.projIcc, TopologicalSpace.NonemptyCompacts.lipschitz_prod, UpperHalfPlane.volume_def, one_le_coe, LipschitzWith.list_prod, ENNReal.toNNReal_one, holderConjugate_one_div, lipschitzWith_one_norm', MeasureTheory.mulEquivHaarChar_refl, ProbabilityTheory.map_pi_eq_stdGaussian, Polynomial.cauchyBound_C, Filter.IsIncreasingApproximateUnit.eventually_nnnorm, Complex.ofRealCLM_nnnorm, LipschitzOnWith.mk_one, TopologicalSpace.Closeds.lipschitz_sup, CFC.sqrt_eq_nnrpow, PiLp.lipschitzWith_ofLp, Real.lipschitzWith_sin, indicator_le_thickenedIndicator, Isometry.toDilation_ratio, lipschitzOnWith_cfc_fun, WithLp.prod_antilipschitzWith_toLp, one_lt_rpow_of_pos_of_lt_one_of_neg, zero_rpow_def, PadicAlgCl.valuation_p, ENNReal.coe_one, PadicComplex.valuation_p, WithZeroMulInt.toNNReal_le_one_iff, coe_lt_one, MeasureTheory.ProbabilityMeasure.apply_le_one, IsUltrametricDist.nnnorm_add_one_le_max_nnnorm_one, WithLp.prod_lipschitzWith_ofLp, ContinuousMap.toNNReal_one, MeasureTheory.Lp.lipschitzWith_pos_part, Real.toNNReal_one, PiNat.exists_lipschitz_retraction_of_isClosed, one_le_thickenedIndicator_apply', ENNReal.coe_le_one_iff, rpow_le_one, MeasureTheory.addEquivAddHaarChar_eq_one_of_compactSpace, Polynomial.cauchyBound_one, CStarAlgebra.nnnorm_le_one_iff_of_nonneg, lp.lipschitzWith_one_eval, NormedField.exists_one_lt_nnnorm, rpow_eq_left_iff, list_prod_map_rpow', UpperHalfPlane.volume_eq_lintegral, lipschitzOnWith_cfcβ_fun, HolderTriple.one_div_nonneg, HolderConjugate.one_sub_inv_inv, SemilinearIsometryClass.antilipschitz, thickenedIndicator_tendsto_indicator_closure, ENNReal.one_eq_coe, one_le_rpow_of_pos_of_le_one_of_nonpos, Real.toNNReal_lt_one, UniformOnFun.lipschitzWith_eval, hasSum_geometric, one_lt_rpow, RCLike.lipschitzWith_re, MeasureTheory.L1.nnnorm_Integral_le_one, Set.InvOn.one_sub_one_add_inv, HolderConjugate.conjugate_eq, sqrt_eq_one, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id, TopologicalSpace.Closeds.lipschitz_prod, HasOuterApproxClosed.apprSeq_apply_eq_one, Real.lipschitzWith_one_mulExpNegMulSq, AntilipschitzWith.subtype_coe, IsPrimitiveRoot.nnnorm_eq_one, Complex.conjCLE_nnorm, MeasureTheory.MeasuredSets.lipschitzWith_measureReal, LipschitzWith.dist_right, lt_inv_iff_mul_lt, Real.one_le_toNNReal, CompletelyRegularSpace.exists_BCNN, Polynomial.one_le_cauchyBound, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, holderConjugate_iff_eq_conjExponent, LinearIsometry.antilipschitz, LipschitzWith.prodMk_left, one_le_sqrt, rpow_lt_one_of_one_lt_of_neg, MeasureTheory.Measure.modularCharacterFun_map_one, lipschitzWith_negPart, MeasureTheory.FiniteMeasure.testAgainstNN_one, Real.lipschitzWith_toNNReal, le_inv_iff_mul_le, ContinuousLinearMap.opNNNorm_mul, lipschitzWith_one_nnnorm, HolderTriple.one_div_eq, lipschitzOnWith_cfcβ_fun_of_subset, rpow_rpow_inv_eq_iff, Valued.integer.exists_nnnorm_lt_one, Polynomial.cauchyBound_zero, LipschitzWith.eval, Isometry.lipschitz, DilationEquiv.ratio_refl, HolderConjugate.one_sub_inv, summable_one_div_rpow, WithZeroMulInt.toNNReal_eq_one_iff, exists_lt_rieszContentAux_add_pos, Submodule.lipschitzWith_starProjection, Int.nnnorm_coe_units, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, BoundedContinuousFunction.lipschitz_compContinuous, HolderConjugate.inv_one_sub_inv, HolderConjugate.div_conj_eq_sub_one, holderWith_id, LipschitzOnWith.of_le_add, coe_mulIndicator, TopologicalSpace.NonemptyCompacts.lipschitz_sup, rpow_eq_rpow_right_iff, Complex.nnnorm_exp_ofReal_mul_I, GromovHausdorff.toGHSpace_lipschitz, inv_le, PMF.bernoulli_apply, WithZeroMulInt.toNNReal_strictMono, ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le, IsUltrametricDist.nnnorm_intCast_le_one, PreTilt.valAux_one, norm_cfcβ_one_sub_one_add_inv_lt_one, RCLike.lipschitzWith_ofReal, Isometry.antilipschitz, Metric.lipschitz_infDist_pt, Complex.imCLM_nnnorm, Submodule.lipschitzWith_orthogonalProjection, MeasureTheory.Measure.haarScalarFactor_self, HasOuterApproxClosed.indicator_le_apprSeq, sqrt_one, Real.lipschitzWith_cos, ProbabilityTheory.stdGaussian_eq_map_pi_orthonormalBasis, HolderTriple.one_div_add_one_div, holderOnWith_one, ENNReal.one_lt_coe_iff, EMetric.Closeds.lipschitz_sup, IsUltrametricDist.nnnorm_natCast_le_one, PMF.mem_support_bernoulli_iff, AffineIsometryEquiv.lipschitz, sqrt_le_one, MeasureTheory.ProbabilityMeasure.testAgainstNN_lipschitz, LinearIsometryEquiv.lipschitz, ContinuousMultilinearMap.nnnorm_ofSubsingleton_id, MeasureTheory.addEquivAddHaarChar_refl, Metric.lipschitz_infDist_set, rpow_zero, thickenedIndicator_one, LipschitzOnWith.holderOnWith, unitInterval.toNNReal_symm_add_toNNReal, one_rpow, BoundedContinuousFunction.lipschitz_eval_const, MeasureTheory.mulEquivHaarChar_eq_one_of_compactSpace, Polynomial.cauchyBound_X_add_C, CStarAlgebra.inr_mem_Icc_iff_nnnorm_le, ContinuousLinearMap.nnnorm_id, HolderTriple.one_div_pos, coe_one, Complex.nnnorm_I, IsUnifLocDoublingMeasure.one_le_scalingConstantOf, coe_mulSingle, AffineIsometryEquiv.antilipschitz, Real.toNNReal_eq_one, Polynomial.cauchyBound_X_sub_C, one_lt_coe, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id_le, BoundedContinuousFunction.lipschitz_evalx, ENNReal.one_le_coe_iff, AffineIsometry.antilipschitz, lipschitzWith_one_nnnorm', MeasureTheory.ProbabilityMeasure.coeFn_univ, HolderConjugate.sub_one_pos, Dilation.ratio_of_trivial, lipschitzWith_max, ContinuousLinearMap.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm, NumberField.mixedEmbedding.one_le_convexBodyLT'Factor, Delone.DeloneSet.mapBilipschitz_refl, HolderConjugate.sub_one_mul_conj, list_prod_map_rpow, exists_continuous_add_one_of_isCompact_nnreal, lipschitzWith_posPart, Polynomial.cauchyBound_X, ENNReal.coe_lt_one_iff, Complex.nnnorm_eq_one_of_pow_eq_one, NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal, holderConjugate_iff, one_le_thickenedIndicator_apply, EMetric.NonemptyCompacts.lipschitz_sup, inv_lt_one_iff, HasOuterApproxClosed.apprSeq_apply_le_one, lipschitzWith_min, one_le_nnnorm_one, coe_eq_one, UniformOnFun.lipschitzWith_restrict, coe_list_prod, LipschitzWith.subtype_val, Metric.lipschitz_infNndist_pt, HasOuterApproxClosed.exAppr, tsum_geometric_nnreal, unitInterval.toNNReal_add_toNNReal_symm, RCLike.lipschitzWith_im, MeasureTheory.Measure.addHaarScalarFactor_self, unitInterval.toNNReal_one, Dilation.ratio_of_subsingleton, holderWith_one, RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict, tendsto_pow_atTop_nhds_zero_iff, UniformOnFun.lipschitzWith_one_ofFun_toFun', HolderTriple.one_div_pos', MeasureTheory.BorelCantelli.process_difference_le, lipschitzWith_one_norm, UniformFun.lipschitzWith_eval, ContinuousMap.exists_mul_le_one_eqOn_ge
|
instOrderBot π | CompOp | 26 mathmath: Seminorm.finset_sup_apply, Pi.norm_def', BoxIntegral.Prepartition.distortion_biUnionTagged, bot_eq_zero, mul_finset_sup, Pi.nnnorm_def', NumberField.canonicalEmbedding.nnnorm_eq, ENNReal.coe_finset_sup, Pi.norm_def, BoundedContinuousFunction.nnnorm_sum_eq_sup, nndist_pi_def, IsUltrametricDist.nnnorm_sum_eq_sup_of_pairwise_ne, IsUltrametricDist.nnnorm_prod_eq_sup_of_pairwise_ne, BoxIntegral.TaggedPrepartition.distortion_biUnionPrepartition, BoxIntegral.Prepartition.distortion_biUnion, Pi.nnnorm_def, dist_pi_def, Finset.nnnorm_sum_le_sup_nnnorm, finset_sup_mul, Finset.nnnorm_prod_le_sup_nnnorm, ContinuousMap.nnnorm_sum_eq_sup, Matrix.linfty_opNNNorm_def, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, Matrix.linfty_opNorm_def, Matrix.norm_eq_sup_sup_nnnorm, finset_sup_div
|
instOrderedSub π | CompOp | β |
instPartialOrder π | CompOp | 720 math, 2 bridgemath: SpectrumRestricts.le_nnreal_iff, summable_and_Lr_rpow_le_Lp_mul_Lq_tsum, MeasureTheory.FiniteMeasure.mass_map_le, pow_arith_mean_le_arith_mean_pow, orderIsoIccZeroCoe_apply_coe_coe, hasSum_lt, Matrix.frobenius_nnnorm_mul, summable_and_inner_le_Lp_mul_Lq_tsum, toReal_lt, Real.toNNReal_lt_natCast', IsometricContinuousFunctionalCalculus.isGreatest_nnnorm_spectrum, HolderTriple.one_div_nonneg', eq_zero_or_nnnorm_pos, IsPicardLindelof.of_contDiffAt_one, thickenedIndicator_mono_infEDist, nnnorm_le_insert', nnnorm_le_nnnorm_add_nnnorm_div', nnnorm_cfcβ_nnreal_le_iff, pi_nnnorm_lt_iff', nnnorm_cfc_lt, WithLp.prod_nndist_eq_of_L2, Real.nnnorm_deriv_mulExpNegMulSq_le_one, ENNReal.exists_nnreal_pos_mul_lt, isCompact_setOf_finiteMeasure_le_of_isCompact, AntilipschitzWith.mul_le_nndist, mul_iSup_le, pow_antitone_exp, pi_nnnorm_le_iff, NumberField.mixedEmbedding.one_le_convexBodyLTFactor, MeasureTheory.addEquivAddHaarChar_pos, nndist_pi_le_iff, IsUltrametricDist.nnnorm_tprod_le_of_forall_le, rpow_lt_one, Real.toNNReal_le_toNNReal_iff', eventually_enorm_mfderivWithin_symm_extChartAt_lt, exists_lt_of_strictMono, Real.tendsto_toNNReal_atTop_iff, nnnorm_cfcβ_lt_iff, CFC.nnnorm_sqrt, List.nnnorm_prod_le', nnnorm_nsmul_le, sqrt_le_iff_le_sq, MeasureTheory.ProbabilityMeasure.exists_lt_measure_biUnion_of_isOpen, sqrt_mul_lt_half_add_of_ne, MeasureTheory.Lp.nnnorm_le_of_ae_bound, IsGreatest.nnnorm_cfcβ, nnnorm_sum_le, Real.toNNReal_le_ofNat, inner_le_Lp_mul_Lq_hasSum, rpow_add_rpow_le_add, coe_le_one, ENNReal.lt_iff_exists_add_pos_lt, ContinuousLinearMap.opNNNorm_le_iff, segment_eq_uIcc, nnnorm_le_add_nnnorm_add, nnnorm_le_mul_nnnorm_add, div_lt_one_of_lt, orderIsoRpow_apply, agmSequences_zero, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum, ContinuousLinearMap.ebound, MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure, MeasureTheory.exists_upperSemicontinuous_le_lintegral_le, agm_lt_max_of_ne, nnnorm_le_nnnorm_add_nnnorm_sub, Real.le_toNNReal_iff_coe_le, pi_pos, not_summable_iff_tendsto_nat_atTop, IsUltrametricDist.nnnorm_pow_le, sqrt_sq, EuclideanSpace.nndist_eq, rpow_lt_rpow_iff_of_neg, sqrt_pos, Matrix.nnnorm_lt_iff, ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective, NormedField.exists_lt_nnnorm_lt, Real.nnnorm_exp_I_mul_ofReal_sub_one_le, NormedField.exists_nnnorm_lt_one, le_sqrt_iff_sq_le, sqrt_eq_rpow, CStarAlgebra.mem_Icc_iff_nnnorm_le_one, Metric.exists_continuous_nnreal_forall_closedBall_subset, nnnorm_le_insert, PiLp.nnnorm_eq_of_L2, ENNReal.toNNReal_le_toNNReal, half_le_self, MeasureTheory.MemLp.meas_ge_lt_top, agm_le_agmSequences_snd, FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius, nndist_nnnorm_nnnorm_le_nnnorm_inv_mul, HolderTriple.nonneg', EMetric.exists_continuous_nnreal_forall_closedBall_subset, sqrt_zero, WithLp.nndist_fst_le, NonUnitalStarAlgHom.nnnorm_apply_le, young_inequality, map_coe_atTop, ContinuousAlternatingMap.le_opNNNorm, rpow_inv_lt_iff_of_pos, nndist_add_add_le, ContinuousMultilinearMap.le_of_opNNNorm_le, Real.toNNReal_lt_toNNReal_iff_of_nonneg, HolderTriple.left_pos, Matrix.linfty_opNNNorm_mulVec, ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm, eventually_pow_one_div_le, ApproximatesLinearOn.norm_fderiv_sub_le, IsGreatest.nnnorm_cfc_nnreal, rpow_zero_pos, rpow_lt_rpow_of_neg, agmSequences_fst_le_agm, ENNReal.coe_mem_upperBounds, HolderOnWith.nndist_le_of_le, image_coe_Ico, MeasureTheory.uniformIntegrable_iff, FormalMultilinearSeries.nnnorm_changeOrigin_le, instPosSMulStrictMono, one_le_rpow, rpow_le_one_of_one_le_of_nonpos, eq_one_or_nnnorm_pos, rpow_lt_rpow, FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum, nnnorm_mul_le, ENNReal.image_coe_Iic, Matrix.frobenius_nnnorm_one, thickenedIndicator_le_one, ENNReal.instSMulPosMonoNNReal, count_const_le_le_of_tsum_le, BoxIntegral.Prepartition.distortion_le_of_mem, NormedField.exists_nnnorm_lt, MeasureTheory.Lp.nnnorm_le_mul_nnnorm_of_ae_le_mul, nnnorm_mulβ_le, strictConcaveOn_sqrt, arith_mean_le_rpow_mean, MeasureTheory.mulEquivHaarChar_pos, WithZeroMulInt.toNNReal_pos, sqrt_le_sqrt, pi_nnnorm_lt_iff, ENNReal.natCast_le_ofNNReal, isGreatest_Lp, Real.one_lt_toNNReal, LinearMap.exists_antilipschitzWith, isCoboundedUnder_le_toReal, nndist_smul_le, nnnorm_cfcβ_nnreal_lt, CStarAlgebra.nnnorm_le_iff_of_nonneg, List.nnnorm_prod_le, nnnorm_le_mul_nnnorm_add', BoxIntegral.Box.nndist_le_distortion_mul, MeasureTheory.SimpleFunc.nnnorm_approxOn_le, eventually_nnnorm_sub_lt, ENNReal.iSup_coe_lt_top, Real.toNNReal_le_one, closedBall_zero_eq_Icc, lt_iff_exists_rat_btwn, Real.toNNReal_monotone, WithZeroMulInt.toNNReal_lt_one_iff, nndist_le_pi_nndist, nnnorm_zpow_le_mul_norm, rpow_le_rpow, CompactlySupportedContinuousMap.nnrealPart_add_le_add_nnrealPart, comap_coe_atTop, MeasureTheory.ProbabilityMeasure.apply_mono, rpow_sum_le_const_mul_sum_rpow, PiLp.nndist_apply_le, BoundedContinuousFunction.nndist_set_exists, BoundedContinuousFunction.Lp_nnnorm_le, dist_le_coe, iSup_mul_iSup_le, isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le, antilipschitzWith_iff_le_mul_nndist, FormalMultilinearSeries.compAlongComposition_nnnorm, MeasureTheory.FiniteMeasure.pos_mono, rpow_le_rpow_of_exponent_ge, IsGreatest.nnnorm_cfc, SemilinearMapClass.nnbound_of_continuous, nndist_triangle_right, one_le_coe, Real.toNNReal_le_toNNReal_iff, Finset.nnnorm_prod_le', sqrt_eq_iff_eq_sq, SpectrumRestricts.nnreal_lt_iff, HolderTriple.inv_nonneg, exists_spanning_measurableSet_le, addLeftMono, ENNReal.le_coe_iff, ENNReal.coe_lt_coe, nnnorm_multiset_sum_le, Valuation.RankOne.exists_val_lt, IsGreatest.nnnorm_cfcβ_nnreal, Matrix.l2_opNNNorm_mulVec, PiLp.nnnorm_apply_le, map_coe_nhdsGT, MeasureTheory.SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral, Complex.antilipschitz_equivRealProd, AntilipschitzWith.le_mul_nnnorm', rpow_lt_rpow_of_exponent_gt, bddAbove_range_agmSequences_fst, image_coe_Iio, isBoundedUnder_ge_toReal, FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le, nnnorm_apply_le_nnnorm_cfcβ, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le, nnnorm_pow_le, BoxIntegral.TaggedPrepartition.distortion_le_of_mem, rpow_lt_rpow_of_exponent_lt, ENNReal.toNNReal_pos, ContinuousLinearMap.opNNNorm_le_bound, Filter.IsIncreasingApproximateUnit.eventually_nnnorm, Real.toNNReal_le_natCast, MeasureTheory.UniformIntegrable.spec', ENNReal.coe_le_coe, QuasispectrumRestricts.le_nnreal_iff, ProbabilityTheory.Kernel.HasSubgaussianMGF.add, WithLp.prod_nnnorm_eq_of_L2, ENNReal.orderIsoIicCoe_symm_apply_coe, Valuation.RankOne.strictMono, instStarOrderedRing, nnnorm_mul_le', nnnorm_pos', IsUltrametricDist.nnnorm_mul_le_max, agmSequences_fst_lt_snd_of_ne, FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, MeasureTheory.measureUnivNNReal_pos, indicator_le_thickenedIndicator, ContinuousMap.nnnorm_lt_iff, SpectrumRestricts.nnreal_le_iff, bot_eq_zero, sqrt_mul, Real.ofNat_lt_toNNReal, SchauderBasis.bddAbove_range_nnnorm_proj, rpow_arith_mean_le_arith_mean_rpow, le_add_nndist, one_lt_rpow_of_pos_of_lt_one_of_neg, ENNReal.le_toNNReal_of_coe_le, ContinuousLinearMap.nnnorm_holder_apply_apply_le, instIsOrderBornology, ENNReal.toNNReal_strict_mono, tendsto_real_toNNReal_atTop, MeasureTheory.FiniteMeasure.apply_iUnion_le, add_rpow_le_rpow_add, sqrt_eq_zero, SemilinearMapClass.ebound_of_continuous, Real.comap_toNNReal_atTop, MeasureTheory.FiniteMeasure.apply_mono, WithZeroMulInt.toNNReal_le_one_iff, MeasureTheory.L1.nnnorm_integral_le, coe_lt_one, Module.Basis.exists_opNNNorm_le, MeasureTheory.ProbabilityMeasure.apply_le_one, mul_self_sqrt, isCompact_setOf_finiteMeasure_le_of_compactSpace, ENNReal.ofNNReal_le_natCast, Real.toNNReal_pos, strictMono_rpow_of_pos, lt_rpow_inv_iff, agmSequences_fst_monotone, ContinuousLinearMap.isLeast_opNNNorm, MeasureTheory.FiniteMeasure.testAgainstNN_mono, IsUltrametricDist.nnnorm_add_one_le_max_nnnorm_one, CStarAlgebra.nnnorm_sub_mul_self_le, MeasureTheory.exists_lt_lintegral_simpleFunc_of_lt_lintegral, nndist_midpoint_midpoint_le', Real.toNNReal_lt_iff_lt_coe, ModP.v_p_lt_preVal, Real.toNNReal_lt_toNNReal_iff, exists_pow_lt_of_lt_one, geom_mean_le_arith_mean4_weighted, tendsto_rpow_atTop, tsum_comp_le_tsum_of_inj, one_le_thickenedIndicator_apply', ENat.floor_coe, ENNReal.coe_le_one_iff, Delone.DeloneSet.packingRadius_pos, HolderTriple.lt, rpow_le_one, ContinuousLinearMap.opNNNorm_le_bound', Matrix.l2_opNNNorm_mul, nndist_vsub_vsub_le, Pi.sum_nnnorm_apply_le_nnnorm, nndist_nnnorm_nnnorm_le_nnnorm_neg_add, geom_mean_le_arith_mean2_weighted, image_coe_Ioc, pi_nnnorm_le_iff', Matrix.nnnorm_entry_le_entrywise_sup_nnnorm, nnnorm_cfc_le_iff, CStarAlgebra.nnnorm_le_one_iff_of_nonneg, ContinuousLinearMap.opNNNorm_le_of_unit_nnnorm, rpow_inv_le_iff_of_pos, Metric.exists_continuous_nnreal_forall_closedEBall_subset, ContinuousMap.nnnorm_lt_iff_of_nonempty, nnnorm_prod_le_of_le, ValuativeRel.RankLeOneStruct.strictMono, Dilation.ratio_pos, nnnorm_le_pi_nnnorm, QuasispectrumRestricts.lt_nnreal_iff, nndist_mul_mul_le, NormedField.exists_one_lt_nnnorm, nndist_triangle, rpow_le_self_of_le_one, Real.toNNReal_add_le, agm_eq_agm_gm_am, MeasureTheory.FiniteMeasure.mass_comap_le, AntilipschitzWith.le_mul_nndist, rpow_lt_rpow_iff, rpow_inv_le_iff, le_gm_and_am_le, AntilipschitzWith.pos, isBoundedUnder_le_toReal, continuous_sqrt, ContinuousMultilinearMap.isLeast_opNNNorm, HolderTriple.one_div_nonneg, image_coe_Ici, min_le_agm, le_iInf_mul_iInf, uniformity_basis_edist_nnreal_le, nndist_triangle_left, one_le_rpow_of_pos_of_le_one_of_nonpos, IsUltrametricDist.nnnorm_sum_le_of_forall_le, isCoboundedUnder_ge_toReal, MeasureTheory.mul_le_addHaar_image_of_lt_det, Real.toNNReal_lt_one, nnnorm_cfcβ_nnreal_lt_iff, ContinuousLinearMap.nonlinearRightInverseOfSurjective_def, exists_pos_sum_of_countable, Pi.sum_nnnorm_apply_le_nnnorm', rieszContentAux_sup_le, one_lt_rpow, isOpen_Ico_zero, CStarAlgebra.mem_Icc_algebraMap_iff_nnnorm_le, nnnorm_cfc_nnreal_lt, MeasureTheory.L1.nnnorm_Integral_le_one, Units.nnnorm_pos, HolderTriple.pos', ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos, le_rpow_inv_iff, edist_lt_coe, Tactic.NormNum.isNNRat_nnrealSqrt_of_isNNRat, enorm_lt_coe, Real.toNNReal_mono, IsUltrametricDist.nnnorm_tsum_le_of_forall_le, Set.InvOn.one_sub_one_add_inv, rpow_add_rpow_le, ENNReal.iSup_coe_eq_top, BoundedContinuousFunction.nndist_coe_le_nndist, nnnorm_cfc_nnreal_le, nnnorm_inner_le_nnnorm, sqrt_eq_one, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnnorm_quasispectrum, IsometricContinuousFunctionalCalculus.nnnorm_spectrum_le, cfc_nnreal_le_iff, sqrt_pos_of_pos, nnnorm_pow_le_mul_norm, ENNReal.coe_lt_natCast, nnnorm_cfc_nnreal_le_iff, BoxIntegral.TaggedPrepartition.distortion_filter_le, Real.toNNReal_le_toNNReal, ENNReal.coe_pos, ENNReal.exists_pos_sum_of_countable, nndist_pi_const_le, pi_nnnorm_const_le', Real.toNNReal_lt_ofNat, rpow_inv_le_iff_of_neg, ENNReal.toNNReal_mono, Set.OrdConnected.preimage_coe_nnreal_ennreal, WithLp.nnnorm_fst_le, MeasureTheory.nnnorm_indicatorConstLp_le, enorm_le_coe, IsUltrametricDist.nnnorm_nsmul_le, agmSequences_monotone_and_antitone, rpow_add_le_mul_rpow_add_rpow, rieszContentAux_mono, ENNReal.exists_pos_tsum_mul_lt_of_countable, sum_mul_le_sqrt_mul_sqrt, rpow_le_rpow_of_nonpos, lt_inv_iff_mul_lt, Real.one_le_toNNReal, le_rpow_inv_iff_of_neg, eventually_enorm_mfderiv_extChartAt_lt, MeasureTheory.addHaar_image_le_mul_of_det_lt, Polynomial.one_le_cauchyBound, tsum_lt_tsum, MeasureTheory.ProbabilityMeasure.apply_iUnion_le, nnnorm_smul_le, ball_zero_eq_Ico', thickenedIndicator_subset, ContinuousLinearMap.le_opNNNorm, nnnorm_cfc_le, ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos, HolderTriple.right_pos, ENNReal.image_coe_Iio, one_le_sqrt, lt_rpow_inv_iff_of_neg, div_le_of_le_mul, Lp_add_le_hasSum, convex_iff, le_mul_iInf, coe_expect, nnnorm_le_nnnorm_add_nnnorm_div, nnnorm_apply_le_nnnorm_cfc, IsometricContinuousFunctionalCalculus.spectrum_le, nnnorm_pow_le', Real.le_toNNReal_iff_coe_le', rpow_lt_one_of_one_lt_of_neg, BoundedContinuousFunction.nnnorm_coe_le_nnnorm, SchauderBasis.nnnorm_proj_le_nnnormProjBound, dist_lt_coe, nndist_nnnorm_nnnorm_le', half_lt_self, inner_le_weight_mul_Lp, le_toNNReal_of_coe_le, BoundedContinuousFunction.nnnorm_le, ProbabilityTheory.HasSubgaussianMGF.add, iInf_real_pos_eq_iInf_nnreal_pos, MeasureTheory.SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge, edist_le_coe, lt_rpow_inv_iff_of_pos, rpow_le_rpow_iff_of_neg, geom_mean_le_arith_mean_weighted, Set.OrdConnected.image_real_toNNReal, le_inv_iff_mul_le, AntilipschitzWith.le_mul_nnnorm, nndist_midpoint_midpoint_le, image_coe_Iic, Lr_le_Lp_mul_Lq, Delone.DeloneSet.mapBilipschitz_trans, MeasureTheory.ProbabilityMeasure.apply_union_le, BoundedContinuousFunction.nnnorm_const_le, nnnorm_tsum_le, nnnorm_fderiv_norm_rpow_le, orderIsoIccZeroCoe_symm_apply_coe, ContinuousAlternatingMap.isLeast_opNNNorm, ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm, apply_le_nnnorm_cfc_nnreal, setOf_riemannianEDist_lt_subset_nhds, eventually_riemannianEDist_le_edist_extChartAt, segment_eq_Icc, coe_mono, exists_le_hasSum_of_le, WithLp.nnnorm_snd_le, div_le_of_le_mul', LipschitzWith.nnorm_le_mul', Valued.integer.exists_nnnorm_lt_one, inv_lt_inv, BoxIntegral.Prepartition.distortion_le_iff, instOrderTopology, agmSequences_fst_le_snd, ContinuousLinearMap.nndist_le_opNNNorm, Real.toNNReal_le_toNNReal_iff_of_pos, Matrix.linfty_opNNNorm_mul, thickenedIndicator_mono_infEdist, image_coe_Ioi, nhds_zero, Valuation.RankLeOne.exists_val_lt, Real.natCastle_toNNReal', monotone_nnrpow_const, LipschitzWith.nndist_le, ContinuousLinearMap.opNNNorm_comp_le, rpow_add_le_add_rpow, PreTilt.valAux_add, MemHolder.nnHolderNorm_add_le, Metric.isBounded_iff_nndist, mul_lt_of_lt_div, convex_setOf_holderWith, orderIsoRpow_symm_eq, ENNReal.toNNReal_lt_toNNReal, agmSequences_fst_lt_agm_of_pos_of_ne, exists_lt_rieszContentAux_add_pos, Lp_add_le_tsum', MeasureTheory.Measure.exists_positive_of_not_mutuallySingular, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, NonUnitalIsometricContinuousFunctionalCalculus.quasispectrum_le, bddAbove_natCast_image_iff, addLeftReflectLT, HolderTriple.inv_pos', MeasureTheory.Content.mono', ContinuousMultilinearMap.opNNNorm_le_iff, image_coe_Ioo, nnnorm_multiset_prod_le, HolderTriple.pos, rpow_inv_lt_iff, inv_le, ENNReal.orderIsoIicCoe_apply_coe, nnnorm_commutator_sub_one_le, CFC.sqrt_eq_cfc, coe_lt_coe, WithZeroMulInt.toNNReal_strictMono, ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le, toReal_le, nnnorm_cfcβ_le_iff, IsUltrametricDist.nnnorm_intCast_le_one, MeasureTheory.Measure.modularCharacterFun_pos, HolderTriple.all_pos, rpow_arith_mean_le_arith_mean2_rpow, monotone_rpow_of_nonneg, exists_mem_Ico_zpow, tsum_strict_mono, nnnorm_cfc_lt_iff, IsUltrametricDist.nnnorm_tprod_le, Lr_rpow_le_Lp_mul_Lq_tsum, ContinuousLinearMap.opNNNorm_le_of_lipschitz, Int.abs_le_floor_nnreal_iff, Metric.boundedSpace_iff_nndist, MeasureTheory.eLpNormEssSup_lt_top_iff_isBoundedUnder, UnconditionalSchauderBasis.bddAbove_range_nnnorm_proj, Finset.nnnorm_sum_le_sup_nnnorm, MeasureTheory.UniformIntegrable.spec, HasOuterApproxClosed.indicator_le_apprSeq, sqrt_one, inner_le_Lp_mul_Lq_tsum', ENNReal.coe_le_iff, Lp_add_le, nnnorm_commutator_units_sub_one_le, CFC.sqrt_algebraMap, coe_pos, ENNReal.one_lt_coe_iff, HolderTriple.inv_pos, hasSum_strict_mono, IsUltrametricDist.nnnorm_natCast_le_one, MeasureTheory.FiniteMeasure.apply_le_mass, Set.OrdConnected.preimage_coe_nnreal_real, coe_lt_enorm, ENNReal.coe_mono, Mathlib.Meta.Positivity.nnabs_pos_of_pos, sqrt_le_one, HolderWith.nnholderNorm_le, ENNReal.image_coe_Ici, nnnorm_sum_le_of_le, ball_zero_eq_Ico, ENNReal.coe_strictMono, Real.toNNReal_le_iff_le_coe, nnnorm_sub_mul_le, ModP.v_p_lt_val, ENNReal.image_coe_Ioi, MeasureTheory.SimpleFunc.exists_upperSemicontinuous_le_lintegral_le, Real.nnreal_trichotomy, IsUltrametricDist.nnnorm_zpow_le, nnnorm_cfc_nnreal_lt_iff, ENNReal.toNNReal_lt_of_lt_coe, nnnorm_le_nnnorm_add_nnnorm_sub', min_lt_agm_of_pos_of_ne, UnconditionalSchauderBasis.nnnorm_proj_le_nnnormProjBound, Real.toNNReal_lt_natCast, geom_mean_le_arith_mean3_weighted, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, inv_le_of_le_mul, HolderTriple.inv_nonneg', agmSequences_snd_antitone, spectrum.le_nnnorm_of_mem, summable_iff_not_tendsto_nat_atTop, NormedField.denselyOrdered_range_nnnorm, exists_nat_pos_inv_lt, ENNReal.natCast_lt_coe, nndist_pi_lt_iff, BoxIntegral.TaggedPrepartition.distortion_le_iff, Real.nnabs_pos, MeasureTheory.Measure.addModularCharacterFun_pos, CStarAlgebra.inr_mem_Icc_iff_nnnorm_le, agm_pos, convex_setOf_holderOnWith, rpow_le_rpow_of_exponent_le, HolderTriple.one_div_pos, sqrt_div, Matrix.nnnorm_le_iff, tendsto_coe_atTop, ENNReal.image_coe_Ioo, le_iInf_add_iInf, ContinuousLinearEquiv.nnnorm_symm_pos, Finset.nnnorm_prod_le_sup_nnnorm, pi_nnnorm_const_le, Finset.nnnorm_prod_le, instIsStrictOrderedModule, EuclideanSpace.nnnorm_eq, nhds_zero_basis, IsUnifLocDoublingMeasure.one_le_scalingConstantOf, tsum_le_of_sum_range_le, HolderOnWith.nndist_le, MeasureTheory.exists_upperSemicontinuous_le_integral_le, ContinuousLinearMap.nnbound, agmSequences_succ', uniformity_basis_edist_nnreal, one_lt_coe, nndist_nnnorm_nnnorm_le, Module.Basis.opNNNorm_le, MeasureTheory.Measure.toSphereBallBound_pos, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id_le, tsum_of_nnnorm_bounded, CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_le, closedBall_zero_eq_Icc', Real.coe_sqrt, ENNReal.one_le_coe_iff, ContinuousAlternatingMap.opNNNorm_le_iff, Real.tendsto_toNNReal_atTop, inner_le_Lp_mul_Lq_tsum, instSMulPosStrictMono, nnnorm_prod_le, MeasureTheory.exists_eLpNorm_indicator_le, ENat.ceil_coe, sum_sqrt_mul_sqrt_le, mulLeftMono, ModP.preVal_add, HolderConjugate.sub_one_pos, CompactlySupportedContinuousMap.monotone_of_nnreal, TensorProduct.nndist_tmul_le, lipschitzExtensionConstant_pos, sqrt_mul_le_half_add, Real.map_toNNReal_atTop, Real.lt_toNNReal_iff_coe_lt, Lr_rpow_le_Lp_mul_Lq, MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz_estimate, MeasureTheory.Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure, ContinuousLinearMap.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm, ENNReal.image_coe_Ico, NumberField.mixedEmbedding.one_le_convexBodyLT'Factor, ENNReal.image_coe_Icc, nnnorm_sub_mul_le', SpectrumRestricts.lt_nnreal_iff, rpow_le_rpow_iff, nnnorm_sub_le, HolderTriple.nonneg, ContinuousMultilinearMap.le_opNNNorm, nnnorm_cfcβ_le, ENNReal.coe_lt_one_iff, MeasureTheory.distribHaarChar_pos, Real.ofNat_le_toNNReal, image_coe_Icc, nnnorm_cfcβ_nnreal_le, BoxIntegral.IntegrationParams.MemBaseSet.exists_common_compl, LinearMap.injective_iff_antilipschitz, le_iInf_mul, ENNReal.instPosSMulStrictMonoNNReal, nnnorm_mul_le_of_le, apply_le_nnnorm_cfcβ_nnreal, ENNReal.tendsto_coe_nhds_top, HolderTriple.inv_lt_inv, tsum_pos, Valuation.RankLeOne.strictMono', nndist_vadd_vadd_le, nnnorm_add_le, coe_le_coe, NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal, holderConjugate_iff, ENNReal.toNNReal_pos_iff, sqrt_mul_self, strictConcaveOn_rpow, one_le_thickenedIndicator_apply, le_rpow_inv_iff_of_pos, nnnorm_le_add_nnnorm_add', Lp_add_le_tsum, inv_lt_one_iff, HasOuterApproxClosed.apprSeq_apply_le_one, sqrt_inv, one_le_nnnorm_one, MeasureTheory.FiniteMeasure.apply_union_le, IsometricContinuousFunctionalCalculus.isGreatest_spectrum, dist_gm_am_le, coe_le_enorm, IsUltrametricDist.nnnorm_prod_le_of_forall_le, IsUltrametricDist.nnnorm_add_le_max, HasOuterApproxClosed.exAppr, CStarAlgebra.nnnorm_le_natCast_iff_of_nonneg, Lr_le_Lp_mul_Lq_tsum, agm_lt_agmSequences_snd_of_ne, EMetric.exists_pos_forall_lt_edist, bddAbove_coe, nnnorm_pos, NormedField.exists_lt_nnnorm, Real.toNNReal_lt_toNNReal_iff', HolderWith.nndist_le, agmSequences_succ, nnnorm_zsmul_le, young_inequality_real, Tactic.NormNum.isNat_nnrealSqrt, BoundedContinuousFunction.apply_le_nndist_zero, SpectrumRestricts.nnreal_iff_nnnorm, BoundedContinuousFunction.nndist_le_two_nnnorm, BoundedContinuousFunction.NNReal.upper_bound, CStarAlgebra.le_nnnorm_of_mem_quasispectrum, map_coe_nhdsGE, sqrt_lt_sqrt, PiLp.nndist_eq_of_L2, IsUltrametricDist.nnnorm_zsmul_le, inner_le_Lp_mul_Lq, rpow_inv_lt_iff_of_neg, NonUnitalIsometricContinuousFunctionalCalculus.nnnorm_quasispectrum_le, Polynomial.card_mahlerMeasure_le_prod, Real.natCast_le_toNNReal, le_of_forall_lt_one_mul_le, iSup_mul_le, exists_mem_Ioc_zpow, Metric.exists_pos_forall_lt_edist, WithLp.nndist_snd_le, Polynomial.IsRoot.norm_lt_cauchyBound, nnnorm_le_pi_nnnorm', bddAbove_range_natCast_iff, rpow_pos, nnnorm_div_le, sq_sqrt, tendsto_pow_atTop_nhds_zero_iff, IsUltrametricDist.nnnorm_tsum_le, MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite, agm_le_max, nndist_pi_eq_iff, HolderTriple.one_div_pos', ContinuousAlternatingMap.le_of_opNNNorm_le, MeasureTheory.Content.sup_le', LipschitzWith.nnorm_le_mul, Icc_subset_segment, Real.natCast_lt_toNNReal, holderTriple_iff, FormalMultilinearSeries.comp_summable_nnreal, concaveOn_rpow, rieszContentAux_le, HolderWith.nndist_le_of_le, Delone.DeloneSet.coveringRadius_pos, ENNReal.image_coe_Ioc, thickenedIndicator_mono, ContinuousMap.exists_mul_le_one_eqOn_ge, IsCoercive.antilipschitz, nnnorm_cfcβ_lt
bridge: BoxIntegral.IntegrationParams.MemBaseSet.exists_compl, BoxIntegral.IntegrationParams.MemBaseSet.distortion_le
|
instSMulNNRat π | CompOp | 3 mathmath: coe_nnqsmul, NNRat.instContinuousSMulNNReal, RCLike.nnnorm_nnqsmul
|
instSemifield π | CompOp | 12 mathmath: SpectrumRestricts.nnreal_of_nonneg, cfcβHom_nnreal_eq_restrict, SpectrumRestricts.nnreal_iff, SpectrumRestricts.smul_of_nonneg, IsSelfAdjoint.sq_spectrumRestricts, cfcHom_nnreal_eq_restrict, coe_expect, PadicComplex.RankOne.hom_eq_embedding, ContinuousLinearMap.IsPositive.spectrumRestricts, SpectrumRestricts.nnreal_iff_spectralRadius_le, SpectrumRestricts.nnreal_iff_nnnorm, SpectrumRestricts.nnreal_add
|
instSemilatticeInf π | CompOp | 5 mathmath: ENNReal.coe_min, agmSequences_min_max, min_le_agm, coe_min, min_lt_agm_of_pos_of_ne
|
instSemilatticeSup π | CompOp | 69 mathmath: BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot', Fin.nndist_insertNth_insertNth, Seminorm.finset_sup_apply, BoundedContinuousFunction.nnnorm_add_eq_max, Pi.norm_def', agm_lt_max_of_ne, ENNReal.coe_max, BoxIntegral.TaggedPrepartition.distortion_disjUnion, LipschitzOnWith.prodMk, BoxIntegral.Prepartition.distortion_biUnionTagged, nndist_single_single, Prod.nnnorm_def, HolderOnWith.of_le_of_le, IsUltrametricDist.nnnorm_mul_le_max, LipschitzWith.min, LipschitzWith.prodMk, IsUltrametricDist.nnnorm_add_eq_max_of_nnnorm_ne_nnnorm, agmSequences_min_max, IsUltrametricDist.nnnorm_add_one_le_max_nnnorm_one, mul_finset_sup, Pi.nnnorm_def', mul_sup, NumberField.canonicalEmbedding.nnnorm_eq, ENNReal.coe_finset_sup, Pi.norm_def, BoundedContinuousFunction.nnnorm_sum_eq_sup, nndist_pi_def, IsUltrametricDist.nnnorm_sum_eq_sup_of_pairwise_ne, nndist_eq, IsUltrametricDist.nnnorm_prod_eq_sup_of_pairwise_ne, ContinuousMultilinearMap.opNNNorm_prod, BoxIntegral.TaggedPrepartition.distortion_biUnionPrepartition, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, BoxIntegral.Prepartition.distortion_disjUnion, BoxIntegral.Prepartition.distortion_biUnion, WithLp.prod_nndist_eq_sup, WithLp.prod_nnnorm_eq_sup, LipschitzWith.max, ContinuousMap.nnnorm_add_eq_max, PreTilt.valAux_add, Pi.nnnorm_def, Prod.nnnorm_mk', Unitization.nnnorm_eq_sup, BoundedContinuousFunction.nnnorm_sub_eq_max, dist_pi_def, sup_mul, Finset.nnnorm_sum_le_sup_nnnorm, IsUltrametricDist.nnnorm_div_eq_max_of_nnnorm_div_ne_nnnorm_div, BoxIntegral.TaggedPrepartition.distortion_unionComplToSubordinate, finset_sup_mul, Finset.nnnorm_prod_le_sup_nnnorm, IsUltrametricDist.nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm, Prod.nnnorm_def', ModP.preVal_add, IsUltrametricDist.nnnorm_sub_eq_max_of_nnnorm_sub_ne_nnnorm_sub, ContinuousAlternatingMap.opNNNorm_prod, ContinuousMap.nnnorm_sum_eq_sup, Matrix.linfty_opNNNorm_def, IsUltrametricDist.nnnorm_add_le_max, Prod.nnnorm_mk, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, Matrix.linfty_opNorm_def, NumberField.house_eq_sup', coe_max, Matrix.norm_eq_sup_sup_nnnorm, agm_le_max, HolderWith.of_le_of_le, finset_sup_div, ContinuousMap.nnnorm_sub_eq_max
|
instSemiring π | CompOp | 753 mathmath: Delone.DeloneSet.mapBilipschitz_coveringRadius, HolderConjugate.mul_eq_add, summable_and_Lr_rpow_le_Lp_mul_Lq_tsum, PiLp.lipschitzWith_toLp, pow_arith_mean_le_arith_mean_pow, Seminorm.isBounded_const, PiLp.norm_toLp_const', summable_coe, PiLp.nndist_eq_sum, Matrix.frobenius_nnnorm_mul, summable_and_inner_le_Lp_mul_Lq_tsum, rpow_sub_intCast, ProbabilityTheory.gaussianReal_map_const_mul, List.nnnorm_prod, tsum_geometric, Real.toNNReal_lt_natCast', ENNReal.toNNReal_pow, HolderTriple.inv_eq, CFC.monotoneOn_one_sub_one_add_inv, ProbabilityTheory.measure_sum_ge_le_of_HasCondSubgaussianMGF, MeasureTheory.integral_smul_nnreal_measure, nnnorm_le_insert', nnnorm_le_nnnorm_add_nnnorm_div', rpowMonoidHom_apply, MemHolder.comp, ENNReal.ofNNReal_add_natCast, ProbabilityTheory.gaussianReal_const_mul, WithLp.prod_nndist_eq_of_L2, MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply, parallelogram_law_with_nnnorm, PreTilt.valAux_eq, ApproximatesLinearOn.lipschitz, HolderOnWith.interpolate, AntilipschitzWith.mul_le_nndist, mul_iSup_le, Real.toNNReal_mul, pow_antitone_exp, setIntegral_withDensity_eq_setIntegral_smulβ, MeasureTheory.addHaarScalarFactor_smul_inv_eq_distribHaarChar, coe_toRealHom, PiLp.norm_toLp_one, HolderWith.of_le, HasSum.toNNReal, ENNReal.ofNNReal_natCast_sub, exists_lt_of_strictMono, Complex.nndist_self_conj, List.nnnorm_prod_le', nnnorm_nsmul_le, sqrt_le_iff_le_sq, HolderOnWith.comp, NumberField.FinitePlace.norm_def', ENNReal.coe_finset_sum, ProbabilityTheory.HasSubgaussianMGF.sum_of_iIndepFun, sqrt_mul_lt_half_add_of_ne, MeasureTheory.ProbabilityMeasure.prod_prod, MeasureTheory.Lp.nnnorm_le_of_ae_bound, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal, nnnorm_sum_le, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, ENNReal.summable_toNNReal_of_tsum_ne_top, ENNReal.smul_def, CFC.abs_nnrpow_two, inner_le_Lp_mul_Lq_hasSum, instStarModuleNNRealOfReal, rpow_add_rpow_le_add, FormalMultilinearSeries.changeOriginSeries_summable_auxβ, ContinuousLinearMap.opNNNorm_le_iff, NumberField.HeightOneSpectrum.rankOne_hom'_def, MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar_inv, segment_eq_uIcc, pow_rpow_inv_natCast, nnnorm_le_add_nnnorm_add, ProbabilityTheory.Kernel.HasSubgaussianMGF.add_compProd, nnnorm_le_mul_nnnorm_add, CompactlySupportedContinuousMap.nnrealPart_smul_neg, nndist_midpoint_right, summable_sigma, WithLp.prod_nnnorm_eq_add, nndist_smulβ, agmSequences_zero, rpow_natCast, nnnorm_le_nnnorm_add_nnnorm_sub, coe_add, Real.toNNReal_pow, not_summable_iff_tendsto_nat_atTop, sqrt_sq, EuclideanSpace.nndist_eq, HolderWith.add, summable_geometric, ProbabilityTheory.HasSubgaussianMGF.const_mul, NumberField.mixedEmbedding.convexBodyLT_volume, instStarModuleNNRealReal, le_sqrt_iff_sq_le, nnnorm_le_insert, PiLp.nnnorm_eq_of_L2, half_le_self, Real.toNNReal_add, nndist_right_lineMap, FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius, ENNReal.tsum_toNNReal_eq, Similar.exists_nndist_eq, ENat.map_coe_nnreal, young_inequality, ContinuousAlternatingMap.le_opNNNorm, nndist_add_add_le, ContinuousMultilinearMap.le_of_opNNNorm_le, LipschitzOnWith.sub, Metric.coveringNumber_two_mul_le_externalCoveringNumber, Matrix.linfty_opNNNorm_mulVec, nndist_left_lineMap, tsum_mul_right, Dilation.ratio_mul, Mathlib.Meta.NormNum.IsNat.nnreal_rpow_isNNRat, MeasureTheory.FiniteMeasure.testAgainstNN_eq_mass_mul, ProbabilityTheory.Kernel.HasSubgaussianMGF.add_comp, natCast_iInf, HolderOnWith.nndist_le_of_le, rpow_add_intCast', FormalMultilinearSeries.nnnorm_changeOrigin_le, instPosSMulStrictMono, HolderTriple.of_pos, NNRealRMK.lintegral_rieszMeasure, WithLp.prod_nndist_eq_of_L1, ProbabilityTheory.gaussianReal_map_continuousLinearMap, MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN, HolderWith.holderWith_zero_of_bounded, FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum, nnnorm_mul_le, Hamming.nndist_eq_hammingDist, CompactlySupportedContinuousMap.toRealLinearMap_apply_apply, similar_iff_exists_nndist_eq, Matrix.frobenius_nnnorm_one, integral_withDensity_eq_integral_smul, isSquare, MeasureTheory.FiniteMeasure.mass_prod, PiLp.nnnorm_toLp_one, MeasureTheory.FiniteMeasure.testAgainstNN_const, MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto, MeasureTheory.Lp.nnnorm_le_mul_nnnorm_of_ae_le_mul, nnnorm_mulβ_le, rieszContentAux_image_nonempty, MeasureTheory.FiniteMeasure.normalize_eq_of_nonzero, LipschitzWith.mul_end, Real.toNNReal_sum_of_nonneg, strictConcaveOn_sqrt, arith_mean_le_rpow_mean, WithZeroMulInt.toNNReal_pos, ContinuousMap.toNNReal_algebraMap, InnerProductSpace.nnnorm_rankOne, ENNReal.natCast_le_ofNNReal, MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar, Seminorm.ball_smul, isGreatest_Lp, CFC.abs_nnrpow, CompactlySupportedContinuousMap.exists_add_of_le, nndist_smul_le, CFC.nnrpow_sqrt_two, ProbabilityTheory.Kernel.HasSubgaussianMGF.const_mul, nndist_inv_invβ, NumberField.HeightOneSpectrum.adicAbv_def, natCast_natAbs, nnnorm_smul, List.nnnorm_prod_le, CompactlySupportedContinuousMap.coe_toRealLinearMap, nnnorm_le_mul_nnnorm_add', HolderConjugate.inv_add_inv_eq_one, ENNReal.toNNReal_add, BoxIntegral.Box.nndist_le_distortion_mul, rpow_sub_natCast, Hamming.nnnorm_eq_hammingNorm, StarAlgHom.realContinuousMapOfNNReal_apply, hasLipschitzAdd, MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalize, MeasureTheory.FiniteMeasure.self_eq_mass_mul_normalize, Real.toNNReal_ofNat, Real.nnabs_of_nonneg, WithZeroMulInt.toNNReal_lt_one_iff, Dilation.nndist_eq, nnnorm_zpow_le_mul_norm, ENNReal.coe_tsum, LipschitzWith.pow_end, CompactlySupportedContinuousMap.nnrealPart_add_le_add_nnrealPart, rpow_sum_le_const_mul_sum_rpow, PseudoMetricSpace.dist_ofPreNNDist, MeasureTheory.distribHaarChar_apply, MeasureTheory.Content.sup_disjoint', BoundedContinuousFunction.Lp_nnnorm_le, iSup_mul_iSup_le, hasSum_real_toNNReal_of_nonneg, ENNReal.instIsScalarTowerNNReal, MeasureTheory.FiniteMeasure.map_fst_prod, antilipschitzWith_iff_le_mul_nndist, FormalMultilinearSeries.compAlongComposition_nnnorm, Metric.packingNumber_two_mul_le_externalCoveringNumber, PiLp.nnnorm_toLp_const', UpperHalfPlane.volume_def, selfAdjoint.nnnorm_pow_two_pow, ModP.preVal_mul, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, SemilinearMapClass.nnbound_of_continuous, rpow_add_natCast', Metric.IsCover.image_lipschitz_of_surjective, setIntegral_withDensity_eq_setIntegral_smulβ', nndist_triangle_right, Dilation.ratioHom_apply, sqrt_eq_iff_eq_sq, exists_spanning_measurableSet_le, summable_nat_add, addLeftMono, LipschitzWith.list_prod, ProbabilityTheory.gaussianReal_map_linearMap, nnnorm_multiset_sum_le, Valuation.RankOne.exists_val_lt, Seminorm.comp_smul, CompactlySupportedContinuousMap.toRealLinearMap_apply, Matrix.l2_opNNNorm_mulVec, LipschitzWith.comp_lipschitzOnWith, Complex.antilipschitz_equivRealProd, TensorProduct.nnnorm_tmul, AntilipschitzWith.le_mul_nnnorm', smulCommClass_left, CFC.posPart_smul, FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le, nnnorm_algebraMap, nnnorm_pow, Real.coe_nnabs, agm_mul_distrib, MeasureTheory.integrable_withDensity_iff_integrable_smulβ, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le, Seminorm.bound_of_continuous, nnnorm_pow_le, summable_mul_rpow_of_Lp_Lq, Real.toNNReal_le_natCast, WithZeroMulInt.toNNReal_neg_apply, CompactlySupportedContinuousMap.toRealPositiveLinear_apply, HolderTriple.inv_inv_add_inv, ProbabilityTheory.Kernel.HasSubgaussianMGF.add, WithLp.prod_nnnorm_eq_of_L2, Valuation.RankOne.strictMono, ProbabilityTheory.HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun, nndist_left_midpoint, nnnorm_mul_le', WithLp.prod_nnnorm_eq_of_L1, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, lipschitzWith_sub, instIsTopologicalSemiring, CFC.sqrt_eq_nnrpow, lipschitzWith_circleMap, IsSelfAdjoint.nnnorm_mul_self, FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal, tsum_eq_add_tsum_ite, rpow_ofNat, sqrt_mul, MeasureTheory.Measure.modularCharacterFun_map_mul, MeasureTheory.Measure.toSignedMeasure_smul, HolderConjugate.two_two, CFC.abs_nnrpow_two_mul, rpow_arith_mean_le_arith_mean_rpow, HolderWith.interpolate_const, iSup_pow_of_ne_zero, le_add_nndist, MeasureTheory.Measure.addHaarScalarFactor_eq_mul, PadicAlgCl.valuation_p, PadicComplex.valuation_p, ContinuousLinearMap.nnnorm_holder_apply_apply_le, ENat.toENNRealOrderEmbedding_apply, MeasureTheory.FiniteMeasure.testAgainstNN_add, NumberField.mixedEmbedding.adjust_f, MeasureTheory.FiniteMeasure.apply_iUnion_le, add_rpow_le_rpow_add, rpow_two, WithZeroMulInt.toNNReal_le_one_iff, nndist_midpoint_left, MeasureTheory.FiniteMeasure.instContinuousSMulNNReal, Module.Basis.exists_opNNNorm_le, PreTilt.valAux_mul, mul_self_sqrt, Mathlib.Meta.NormNum.IsNNRat.nnreal_rpow_isNNRat, MeasureTheory.distribHaarChar_eq_of_measure_smul_eq_mul, ProbabilityTheory.gaussianReal_conv_gaussianReal, ENNReal.ofNNReal_le_natCast, ContinuousMap.nnnorm_smul_const, ENNReal.coe_add, Seminorm.const_isBounded, LipschitzOnWith.extend_finite_dimension, nndist_midpoint_midpoint_le', rpow_natCast_mul, exists_pow_lt_of_lt_one, geom_mean_le_arith_mean4_weighted, mul_finset_sup, ProbabilityTheory.gaussianReal_mul_const, tsum_comp_le_tsum_of_inj, Dilation.ratio_pow, nndist_center_homothety, LipschitzWith.vadd, ENat.floor_coe, Real.toNNReal_eq_natCast, summable_nat_add_iff, rpow_add_natCast, Matrix.l2_opNNNorm_mul, nndist_vsub_vsub_le, coe_natCast, Pi.sum_nnnorm_apply_le_nnnorm, geom_mean_le_arith_mean2_weighted, coe_tsum_of_nonneg, mul_sup, MeasureTheory.Measure.addModularCharacterFun_map_add, WithLp.prod_nndist_eq_add, coe_sum, Real.nnnorm_mul_toNNReal, ENNReal.coe_two, nnnorm_prod_le_of_le, ValuativeRel.RankLeOneStruct.strictMono, CompactlySupportedContinuousMap.integralLinearMap_apply, nndist_mul_mul_le, nndist_triangle, Real.toNNReal_add_le, agm_eq_agm_gm_am, AntilipschitzWith.le_mul_nndist, tendsto_sum_nat_add, ENNReal.toNNReal_natCast, MeasureTheory.memL1_smul_of_L1_withDensity, list_prod_map_rpow', le_gm_and_am_le, UpperHalfPlane.volume_eq_lintegral, Real.nnnorm_two, Real.toNNReal_mul_nnnorm, LipschitzWith.uncurry, Mathlib.Meta.NormNum.IsNat.nnreal_rpow_eq_nnreal_pow, CFC.nnrpow_sqrt, HolderOnWith.interpolate_const, nndist_lineMap_right, le_iInf_mul_iInf, WithLp.prod_lipschitzWith_toLp, nndist_triangle_left, rpow_add', MeasureTheory.FiniteMeasure.smul_testAgainstNN_apply, exists_pos_sum_of_countable, ENNReal.coe_ofNNRealHom, Pi.sum_nnnorm_apply_le_nnnorm', HolderOnWith.holderOnWith_zero_of_bounded, rieszContentAux_sup_le, LipschitzWith.add, HolderWith.comp_holderOnWith, rpow_add, summable_comp_injective, hasSum_geometric, MeasureTheory.euclideanHausdorffMeasure_homothety_image, Seminorm.closedBall_smul, ENNReal.smulCommClass_left, NumberField.FinitePlace.norm_def_int, MeasureTheory.euclideanHausdorffMeasure_homothety_preimage, coe_two, coe_nsmul, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply, Tactic.NormNum.isNNRat_nnrealSqrt_of_isNNRat, summable_of_sum_range_le, MeasureTheory.mulEquivHaarChar_trans, Set.InvOn.one_sub_one_add_inv, rpow_add_rpow_le, ProbabilityTheory.gaussianReal_map_mul_const, nnnorm_inner_le_nnnorm, ENNReal.coe_inv_two, nnnorm_pow_le_mul_norm, InnerProductGeometry.angle_eq_angle_add_angle_iff, ENNReal.coe_lt_natCast, MeasureTheory.integrable_withDensity_iff_integrable_smul, PiLp.antilipschitzWith_ofLp, ConvexBody.smul_le_of_le, MeasureTheory.FiniteMeasure.normalize_eq_inv_mass_smul_of_nonzero, natCast_iSup, ContinuousMap.toNNReal_mul_add_neg_mul_add_mul_neg_eq, ENNReal.coe_mul, LipschitzWith.sub, hasSum_iff_tendsto_nat, LipschitzWith.vsub, Complex.nnnorm_ofNat, LipschitzWith.iterate, ContinuousMapZero.toNNReal_mul_add_neg_mul_add_mul_neg_eq, MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply, MeasureTheory.FiniteMeasure.coeFn_add, ProbabilityTheory.gaussianReal_add_gaussianReal_of_indepFun, smul_def, MeasureTheory.nnnorm_indicatorConstLp_le, summable_Lp_add, ProbabilityTheory.HasSubgaussianMGF.sub_of_indepFun, rpow_add_le_mul_rpow_add_rpow, sum_mul_le_sqrt_mul_sqrt, smulCommClass_right, lt_inv_iff_mul_lt, rpow_add_intCast, LipschitzOnWith.add, CFC.nnrpow_nnrpow, MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN, NNRealRMK.le_rieszMeasure_of_isCompact_tsupport_subset, tsum_lt_tsum, MeasureTheory.ProbabilityMeasure.apply_iUnion_le, nnnorm_smul_le, Real.nndist_eq, CompactlySupportedContinuousMap.toReal_add, NumberField.mixedEmbedding.convexBodyLT'_volume, tsum_eq_toNNReal_tsum, ContinuousLinearMap.le_opNNNorm, Metric.coveringNumber_subset_le, ENNReal.ofNNReal_sub_natCast, Lp_add_le_hasSum, convex_iff, le_mul_iInf, ProbabilityTheory.gaussianPDFReal_inv_mul, coe_expect, nnnorm_le_nnnorm_add_nnnorm_div, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul, rpow_add_one, setIntegral_withDensity_eq_setIntegral_smul, HolderTriple.inv_add_inv_eq_inv, nnnorm_pow_le', ContinuousMapZero.toNNReal_add_add_neg_add_neg_eq, half_lt_self, FormalMultilinearSeries.changeOriginSeries_summable_auxβ, inner_le_weight_mul_Lp, rpow_add_one', ProbabilityTheory.HasSubgaussianMGF.add, ProbabilityTheory.measure_sum_ge_le_of_hasCondSubgaussianMGF, MeasureTheory.Measure.mul_addHaarScalarFactor_smul, CompactlySupportedContinuousMap.toNNRealLinear_apply, geom_mean_le_arith_mean_weighted, le_inv_iff_mul_le, AntilipschitzWith.le_mul_nnnorm, nndist_midpoint_midpoint_le, Lr_le_Lp_mul_Lq, Delone.DeloneSet.mapBilipschitz_trans, MeasureTheory.ProbabilityMeasure.apply_union_le, MemHolder.nnHolderNorm_nsmul, PiLp.norm_toLp_const, nnnorm_tsum_le, nnnorm_fderiv_norm_rpow_le, HasStrictFDerivAt.approximates_deriv_on_open_nhds, TrivSqZeroExt.nnnorm_def, similar_iff_exists_pairwise_nndist_eq, mul_eq_mul_left, ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm, HolderTriple.one_div_eq, segment_eq_Icc, exists_le_hasSum_of_le, instContinuousSMulOfReal, LipschitzWith.nnorm_le_mul', ENNReal.tsum_coe_ne_top_iff_summable, Complex.nnnorm_natCast, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective, Complex.nndist_conj_self, MeasureTheory.SignedMeasure.singularPart_smul_nnreal, ContinuousLinearMap.nndist_le_opNNNorm, DilationEquiv.ratio_trans, NNRealRMK.le_rieszMeasure_of_tsupport_subset, Summable.toNNReal, Matrix.linfty_opNNNorm_mul, Real.toNNReal_add_toNNReal, AntilipschitzWith.comp, Real.nnabs_coe, MemHolder.nnHolderNorm_smul, CFC.nnrpow_three, Valuation.RankLeOne.exists_val_lt, LipschitzWith.mul, MeasureTheory.JordanDecomposition.toSignedMeasure_smul, StarAlgHom.realContinuousMapOfNNReal_injective, Real.natCastle_toNNReal', SeminormedAddCommGroup.lipschitzWith_sub, RCLike.nnnorm_two, summable_one_div_rpow, LipschitzWith.nndist_le, WithZeroMulInt.toNNReal_eq_one_iff, ContinuousLinearMap.opNNNorm_comp_le, rpow_add_le_add_rpow, FormalMultilinearSeries.changeOriginSeries_summable_auxβ, MemHolder.nnHolderNorm_add_le, mul_lt_of_lt_div, convex_setOf_holderWith, coe_pow, Dilation.ratio_comp, exists_lt_rieszContentAux_add_pos, ProbabilityTheory.HasSubgaussianMGF.add_of_hasCondSubgaussianMGF, Lp_add_le_tsum', MeasureTheory.FiniteMeasure.normalize_testAgainstNN, rpow_sub_natCast', HolderOnWith.comp_holderWith, Real.toNNReal_abs, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun, PiLp.nnnorm_eq_of_L1, MeasureTheory.withDensitySMulLI_apply, MeasureTheory.Measure.addHaar_nnreal_smul, bddAbove_natCast_image_iff, addLeftReflectLT, sum_add_tsum_nat_add, tendsto_pow_atTop_nhds_zero_of_lt_one, Seminorm.bound_of_shell_sup, ContinuousLinearMap.nnnorm_smulRight_apply, ContinuousMultilinearMap.opNNNorm_le_iff, MeasureTheory.FiniteMeasure.map_smul, indicator_summable, nnnorm_multiset_prod_le, inv_le, Seminorm.finset_sup_smul, LipschitzWith.comp, nnnorm_commutator_sub_one_le, Seminorm.isBounded_sup, ENNReal.coe_pow, sup_mul, summable_rpow_inv, WithZeroMulInt.toNNReal_strictMono, Valued.toNormedField.norm_def, instTrivialStarNNReal, rpow_arith_mean_le_arith_mean2_rpow, CompactlySupportedContinuousMap.toReal_smul, norm_cfcβ_one_sub_one_add_inv_lt_one, Valuation.norm_def, MeasureTheory.FiniteMeasure.prod_prod, MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous, tsum_strict_mono, FormalMultilinearSeries.summable_nnnorm_mul_pow, Lr_rpow_le_Lp_mul_Lq_tsum, Int.abs_le_floor_nnreal_iff, nnnormHom_apply, Seminorm.bound_of_shell_smul, MeasureTheory.distribHaarChar_eq_div, nndist_lineMap_lineMap, MeasureTheory.withDensityα΅₯_smul_eq_withDensityα΅₯_withDensity, CFC.sqrt_nnrpow_two, Real.toNNReal_coe_nat, Int.nnnorm_natCast, coe_multiset_sum, mul_iSup, inner_le_Lp_mul_Lq_tsum', Lp_add_le, CFC.sqrt_nnrpow, Metric.lipschitz_infDist, nnnorm_commutator_units_sub_one_le, Dilation.ratio_comp', rpow_one_add', MeasureTheory.distribHaarChar_mul, HolderTriple.one_div_add_one_div, sub_mem_posTangentConeAt_of_openSegment_subset, CompactlySupportedContinuousMap.eq_toRealPositiveLinear_toReal, ENNReal.smul_toNNReal, StieltjesFunction.measure_smul, Real.nnnorm_natCast, Mathlib.Meta.Positivity.nnabs_pos_of_pos, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, HolderOnWith.of_le, MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous, nnnorm_sum_le_of_le, nnnorm_sub_mul_le, WithZeroMulInt.toNNReal_pos_apply, mk_natCast, summable_of_le, finset_sup_mul, mul_iInf, coe_mul, summable_schlomilch_iff, ENNReal.toNNReal_mul, CompactlySupportedContinuousMap.nnrealPart_smul_pos, nnnorm_le_nnnorm_add_nnnorm_sub', iInf_mul, Real.toNNReal_lt_natCast, geom_mean_le_arith_mean3_weighted, Int.toNat_add_toNat_neg_eq_nnnorm, summable_iff_not_tendsto_nat_atTop, signedDist_eq_dist_iff_vsub_mem_span, exists_nat_pos_inv_lt, PiLp.nnnorm_eq_sum, Unitization.antilipschitzWith_addEquiv, ENNReal.natCast_lt_coe, unitInterval.toNNReal_symm_add_toNNReal, nnnorm_mul, nndist_homothety_center, Real.nnabs_pos, Polynomial.cauchyBound_X_add_C, convex_setOf_holderOnWith, MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN, Matrix.frobenius_nnnorm_def, summable_mul_of_Lp_Lq, LinearMap.mem_span_iff_bound, ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero, ENNReal.coe_nsmul, tsum_mul_left, ENNReal.toNNReal_sum, le_iInf_add_iInf, instIsStrictOrderedModule, EuclideanSpace.nnnorm_eq, RCLike.nnnorm_natCast, MeasureTheory.Measure.mul_haarScalarFactor_smul, ContinuousMapZero.toNNReal_neg_smul, tsum_le_of_sum_range_le, HolderOnWith.nndist_le, LipschitzOnWith.comp, CStarRing.nnnorm_self_mul_star, ContinuousLinearMap.nnbound, Polynomial.cauchyBound_X_sub_C, rpow_mul_natCast, agmSequences_succ', Module.Basis.opNNNorm_le, hasSum_coe, hasSum_nat_add_iff, ContinuousAlternatingMap.opNNNorm_le_iff, ContinuousMultilinearMap.nnnorm_smulRight, ENNReal.hasSum_coe, inner_le_Lp_mul_Lq_tsum, MeasureTheory.addEquivAddHaarChar_trans, instSMulPosStrictMono, AEMeasurable.nnreal_tsum, nnnorm_prod_le, tendsto_tsum_compl_atTop_zero, summable_condensed_iff, rpow_inv_natCast_pow, ENat.ceil_coe, sum_sqrt_mul_sqrt_le, mulLeftMono, ContinuousMap.toNNReal_add_add_neg_add_neg_eq, NNRealRMK.integral_rieszMeasure, CFC.negPart_smul, CompactlySupportedContinuousMap.monotone_of_nnreal, Matrix.l2_opNNNorm_conjTranspose_mul_self, ContinuousMapZero.toNNReal_smul, TensorProduct.nndist_tmul_le, instBoundedMulNNReal, ProbabilityTheory.gaussianPDFReal_mul, coe_tsum, coe_list_sum, sqrt_mul_le_half_add, rpow_add_of_nonneg, MeasureTheory.Measure.euclideanHausdorffMeasure_smulβ, Lr_rpow_le_Lp_mul_Lq, Unitization.lipschitzWith_addEquiv, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz_estimate, NumberField.FinitePlace.norm_embedding', RCLike.nnnorm_nsmul, ProbabilityTheory.HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF, rpow_of_add_eq, Matrix.linfty_opNNNorm_replicateRow, MeasureTheory.Measure.haarScalarFactor_eq_mul, Valuation.RankOne.hom_eq_zero_iff, integral_withDensity_eq_integral_smulβ, parallelogram_law_with_nnnorm_mul, HolderConjugate.sub_one_mul_conj, list_prod_map_rpow, HolderWith.smul, MeasureTheory.FiniteMeasure.map_snd_prod, nndist_right_midpoint, PiLp.nnnorm_toLp_const, Valuation.RankOne.restrict_RankOne_hom_eq, exists_continuous_add_one_of_isCompact_nnreal, mul_rpow, nnnorm_sub_mul_le', rieszContentAux_union, nnnorm_sub_le, ContinuousMultilinearMap.le_opNNNorm, MeasureTheory.distribHaarChar_pos, ENNReal.coe_natCast, ProbabilityTheory.HasSubgaussianMGF_add_of_HasCondSubgaussianMGF, ENNReal.smulCommClass_right, le_iInf_mul, Real.nndist_eq', nnnorm_mul_le_of_le, tsum_pos, iSup_mul, Valuation.RankLeOne.strictMono', MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN, nndist_vadd_vadd_le, nnnorm_add_le, NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal, holderConjugate_iff, sqrt_mul_self, LipschitzOnWith.div, strictConcaveOn_rpow, WithLp.unitization_nnnorm_def, Real.exists_lt_of_strictMono, nnnorm_le_add_nnnorm_add', ProbabilityTheory.Kernel.integral_withDensity, Lp_add_le_tsum, iSup_pow, ENNReal.ofNNReal_natCast_add, nndist_self_homothety, MeasureTheory.FiniteMeasure.apply_union_le, Metric.IsCover.image_lipschitz, dist_gm_am_le, Matrix.linfty_opNNNorm_def, coe_list_prod, NumberField.FinitePlace.norm_embedding_int, CStarRing.nnnorm_star_mul_self, CStarAlgebra.nnnorm_le_natCast_iff_of_nonneg, Lr_le_Lp_mul_Lq_tsum, HolderWith.interpolate, tsum_geometric_nnreal, HolderWith.nndist_le, agmSequences_succ, Measurable.nnreal_tsum, LipschitzWith.div, nnnorm_zsmul_le, nndist_homothety_self, young_inequality_real, LipschitzOnWith.mul, Tactic.NormNum.isNat_nnrealSqrt, ProbabilityTheory.HasSubgaussianMGF_sum_of_HasCondSubgaussianMGF, ConvexBody.coe_smul', DilationEquiv.ratio_pow, BoundedContinuousFunction.nndist_le_two_nnnorm, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, unitInterval.toNNReal_add_toNNReal_symm, HolderWith.comp, PiLp.nndist_eq_of_L2, inner_le_Lp_mul_Lq, Polynomial.card_mahlerMeasure_le_prod, Real.natCast_le_toNNReal, Matrix.linfty_opNorm_def, CompactlySupportedContinuousMap.exists_add_nnrealPart_add_eq, Seminorm.smul_le_smul, instIsScalarTowerOfReal, NumberField.FinitePlace.norm_def, MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto, Similar.exists_pairwise_nndist_eq, iSup_mul_le, lintegral_mul_le_Lp_mul_Lq, ApproximatesLinearOn.to_inv, Real.cast_natAbs_eq_nnabs_cast, Mathlib.Meta.NormNum.IsInt.nnreal_rpow_eq_inv_nnreal_pow, HolderWith.smul_iff, bddAbove_range_natCast_iff, nnnorm_div_le, ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc, nndist_lineMap_left, sq_sqrt, tendsto_pow_atTop_nhds_zero_iff, summable_rpow, IsSelfAdjoint.nnnorm_pow_two_pow, CFC.nnrpow_two, ContinuousAlternatingMap.le_of_opNNNorm_le, MeasureTheory.Content.sup_le', LipschitzWith.nnorm_le_mul, Icc_subset_segment, Real.natCast_lt_toNNReal, holderTriple_iff, PiLp.nndist_eq_of_L1, FormalMultilinearSeries.comp_summable_nnreal, LipschitzWith.dist, concaveOn_rpow, WithLp.prod_antilipschitzWith_ofLp, rieszContentAux_le, HolderWith.nndist_le_of_le, ContinuousMap.exists_mul_le_one_eqOn_ge, CFC.nnrpow_add, instContinuousStar
|
instSub π | CompOp | 39 mathmath: tsum_geometric, CFC.monotoneOn_one_sub_one_add_inv, ENNReal.ofNNReal_natCast_sub, ENNReal.toNNReal_sub, HolderTriple.inv_sub_inv_eq_inv, MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_pos, AntilipschitzWith.mul_div_lipschitzWith, lipschitzWith_sub, sub_def, cfcβ_tsub, AntilipschitzWith.mul_lipschitzWith, HolderConjugate.one_sub_inv_inv, hasSum_geometric, sub_div, Set.InvOn.one_sub_one_add_inv, ApproximatesLinearOn.antilipschitz, HolderConjugate.conjugate_eq, nndist_eq, coe_sub_def, holderConjugate_iff_eq_conjExponent, ENNReal.ofNNReal_sub_natCast, HolderConjugate.one_sub_inv, ENNReal.coe_sub, HolderConjugate.inv_one_sub_inv, HolderConjugate.div_conj_eq_sub_one, instContinuousSub, PMF.bernoulli_apply, norm_cfcβ_one_sub_one_add_inv_lt_one, instBoundedSubNNReal, cfc_tsub, summable_schlomilch_iff, HolderConjugate.sub_one_pos, HolderConjugate.sub_one_mul_conj, AntilipschitzWith.add_sub_lipschitzWith, coe_sub_of_lt, tsum_geometric_nnreal, AntilipschitzWith.add_lipschitzWith, ApproximatesLinearOn.to_inv, coe_sub
|
instZero π | CompOp | 285 mathmath: HolderTriple.one_div_nonneg', eq_zero_or_nnnorm_pos, IsPicardLindelof.of_contDiffAt_one, Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure, ENNReal.toNNReal_top_mul, ENNReal.toNNReal_eq_zero_iff, ENNReal.toNNReal_top, ENNReal.exists_nnreal_pos_mul_lt, coe_indicator, iSup_of_not_bddAbove, isCompact_setOf_finiteMeasure_le_of_isCompact, nndist_self, zero_rpow, MeasureTheory.addEquivAddHaarChar_pos, eventually_enorm_mfderivWithin_symm_extChartAt_lt, PMF.support_bernoulli, nndist_eq_zero, Summable.countable_support_nnreal, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal, MeasureTheory.FiniteMeasure.zero_testAgainstNN, limsInf_of_not_isCobounded, ContinuousMap.toNNReal_neg_algebraMap, ENNReal.lt_iff_exists_add_pos_lt, CompactlySupportedContinuousMap.nnrealPart_smul_neg, ContinuousLinearMap.ebound, MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure, tendsto_atTop_zero_of_summable, ProbabilityTheory.gaussianReal_zero_var, pi_pos, sqrt_pos, ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective, NormedField.exists_nnnorm_lt_one, Metric.exists_continuous_nnreal_forall_closedBall_subset, isBoundedSMul, ENNReal.toNNReal_mul_top, FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius, HolderTriple.nonneg', EMetric.exists_continuous_nnreal_forall_closedBall_subset, sqrt_zero, MeasureTheory.Lp.nnnorm_eq_zero_iff, HolderTriple.left_pos, rpow_zero_pos, iSup_eq_zero, instPosSMulStrictMono, NNRealRMK.lintegral_rieszMeasure, thickenedIndicator_zero, HolderWith.holderWith_zero_of_bounded, eq_one_or_nnnorm_pos, HasOuterApproxClosed.tendsto_apprSeq, CompactlySupportedContinuousMap.toRealLinearMap_apply_apply, ENNReal.zero_eq_coe, NormedField.exists_nnnorm_lt, rieszContentAux_image_nonempty, coe_eq_zero, MeasureTheory.mulEquivHaarChar_pos, WithZeroMulInt.toNNReal_pos, LinearMap.exists_antilipschitzWith, CompactlySupportedContinuousMap.exists_add_of_le, CompactlySupportedContinuousMap.coe_toRealLinearMap, MeasureTheory.condExpIndSMul_empty, unitInterval.toNNReal_zero, closedBall_zero_eq_Icc, indiscreteTopology_iff_forall_nnnorm_eq_zero, CompactlySupportedContinuousMap.nnrealPart_add_le_add_nnrealPart, holderWith_zero_iff, PseudoMetricSpace.dist_ofPreNNDist, MeasureTheory.FiniteMeasure.pos_mono, SemilinearMapClass.nnbound_of_continuous, HolderTriple.inv_nonneg, coe_zero, indiscreteTopology_iff_forall_nnnorm_eq_zero', CompactlySupportedContinuousMap.toRealLinearMap_apply, MeasureTheory.measureUnivNNReal_eq_zero, MeasureTheory.FiniteMeasure.zero_testAgainstNN_apply, MeasureTheory.ProbabilityMeasure.coeFn_empty, CompactlySupportedContinuousMap.nnrealPart_neg_toReal_eq, ENNReal.toNNReal_pos, nnHolderNorm_zero, ProbabilityTheory.HasSubgaussianMGF.fun_zero, PreTilt.valAux_zero, CompactlySupportedContinuousMap.toRealPositiveLinear_apply, MeasureTheory.FiniteMeasure.coeFn_zero, Metric.coveringNumber_zero, sSup_of_not_bddAbove, nnnorm_pos', nnHolderNorm_const, CompactlySupportedContinuousMap.toReal_apply, MeasureTheory.measureUnivNNReal_pos, indicator_le_thickenedIndicator, tsum_eq_add_tsum_ite, bot_eq_zero, zero_rpow_def, sqrt_eq_zero, SemilinearMapClass.ebound_of_continuous, MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_mass, ProbabilityTheory.HasCondSubgaussianMGF.zero, Module.Basis.exists_opNNNorm_le, Real.toNNReal_pos, ENNReal.coe_eq_zero, nnnorm_eq_zero', MeasureTheory.FiniteMeasure.restrict_eq_zero_iff, Delone.DeloneSet.packingRadius_pos, instContinuousInvβ, Metric.exists_continuous_nnreal_forall_closedEBall_subset, Dilation.ratio_pos, CompactlySupportedContinuousMap.integralLinearMap_apply, rpow_eq_left_iff, tendsto_sum_nat_add, nnnorm_indicator_eq_indicator_nnnorm, ProbabilityTheory.gaussianPDF_zero_var, AntilipschitzWith.pos, CFC.nnrpow_zero, HolderTriple.one_div_nonneg, MeasureTheory.FiniteMeasure.testAgainstNN_zero, thickenedIndicator_tendsto_indicator_closure, rpow_eq_zero, MeasureTheory.FiniteMeasure.mono_null, uniformity_basis_edist_nnreal_le, MeasureTheory.mul_le_addHaar_image_of_lt_det, ContinuousLinearMap.nonlinearRightInverseOfSurjective_def, exists_pos_sum_of_countable, HolderOnWith.holderOnWith_zero_of_bounded, Real.toNNReal_eq_zero, isOpen_Ico_zero, Units.nnnorm_pos, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply, HolderTriple.pos', ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos, sqrt_pos_of_pos, ENNReal.coe_pos, ENNReal.exists_pos_sum_of_countable, ENNReal.coe_zero, nnnorm_zero, ContinuousMapZero.toNNReal_mul_add_neg_mul_add_mul_neg_eq, ENNReal.exists_pos_tsum_mul_lt_of_countable, CompletelyRegularSpace.exists_BCNN, eventually_enorm_mfderiv_extChartAt_lt, NNRealRMK.le_rieszMeasure_of_isCompact_tsupport_subset, MeasureTheory.addHaar_image_le_mul_of_det_lt, Real.toNNReal_of_nonpos, CompactlySupportedContinuousMap.toReal_add, ball_zero_eq_Ico', ProbabilityTheory.Kernel.HasSubgaussianMGF.zero, ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos, HolderTriple.right_pos, hasConstantSpeedOnWith_zero_iff, ContinuousMapZero.toNNReal_add_add_neg_add_neg_eq, nnnorm_eq_zero, iInf_real_pos_eq_iInf_nnreal_pos, CompactlySupportedContinuousMap.toNNRealLinear_apply, BoxIntegral.Prepartition.distortion_bot, ProbabilityTheory.gaussianPDFReal_zero_var, ENNReal.coe_rpow_def, MeasureTheory.SimpleFunc.map_coe_nnreal_restrict, setOf_riemannianEDist_lt_subset_nhds, eventually_riemannianEDist_le_edist_extChartAt, Valued.integer.exists_nnnorm_lt_one, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective, NNRealRMK.le_rieszMeasure_of_tsupport_subset, MeasureTheory.FiniteMeasure.zero_mass, nhds_zero, LipschitzOnWith.zero_iff, ModP.preVal_zero, exists_lt_rieszContentAux_add_pos, MeasureTheory.tendstoInMeasure_iff_tendsto_toNNReal, ProbabilityTheory.HasCondSubgaussianMGF.fun_zero, nnnorm_one', ProbabilityTheory.cauchyPDFReal_scale_zero, limsSup_of_not_isBounded, MeasureTheory.Measure.exists_positive_of_not_mutuallySingular, tendsto_pow_atTop_nhds_zero_of_lt_one, HolderTriple.inv_pos', ProbabilityTheory.cauchyPDF_scale_zero, rpow_eq_rpow_right_iff, indicator_summable, HolderTriple.pos, rpow_eq_zero_iff, Real.toNNReal_zero, MeasureTheory.Measure.modularCharacterFun_pos, HolderTriple.all_pos, MeasureTheory.measureUnivNNReal_zero, limsup_of_not_isBoundedUnder, CompactlySupportedContinuousMap.toReal_smul, zero_eq_nndist, ODE.FunSpace.apply_of_zero, iSup_empty, HasOuterApproxClosed.indicator_le_apprSeq, coe_pos, HolderTriple.inv_pos, CompactlySupportedContinuousMap.nnrealPart_apply, PMF.mem_support_bernoulli_iff, liminf_of_not_isCoboundedUnder, ContinuousLinearMap.opNNNorm_subsingleton, CompactlySupportedContinuousMap.eq_toRealPositiveLinear_toReal, continuousOn_rpow_const_compl_zero, Mathlib.Meta.Positivity.nnabs_pos_of_pos, ball_zero_eq_Ico, coeNNRealReal_zero, WithZeroMulInt.toNNReal_pos_apply, sInf_empty, Real.nnreal_trichotomy, Inseparable.nndist_eq_zero, Metric.inseparable_iff_nndist, CompactlySupportedContinuousMap.nnrealPart_smul_pos, HolderTriple.inv_nonneg', ContinuousMap.toNNReal_neg_one, IndiscreteTopology.nnnorm_eq_zero', Metric.packingNumber_zero, iInf_empty, Real.nnabs_pos, MeasureTheory.Measure.addModularCharacterFun_pos, agm_pos, PreTilt.map_eq_zero, HolderTriple.one_div_pos, MeasureTheory.FiniteMeasure.testAgainstNN_smul, MeasureTheory.FiniteMeasure.mass_zero_iff, MemHolder.nnHolderNorm_eq_zero, ContinuousLinearEquiv.nnnorm_symm_pos, instIsStrictOrderedModule, nhds_zero_basis, ContinuousMapZero.toNNReal_neg_smul, ContinuousLinearMap.nnbound, uniformity_basis_edist_nnreal, MeasureTheory.Measure.toSphereBallBound_pos, ProbabilityTheory.HasSubgaussianMGF.zero, closedBall_zero_eq_Icc', nndist_zero_eq_val', LipschitzWith.const, tendsto_tsum_compl_atTop_zero, MeasureTheory.exists_eLpNorm_indicator_le, NNRealRMK.integral_rieszMeasure, HolderConjugate.sub_one_pos, IndiscreteTopology.nnnorm_eq_zero, CompactlySupportedContinuousMap.monotone_of_nnreal, ContinuousMapZero.toNNReal_smul, lipschitzExtensionConstant_pos, agm_zero_left, coe_list_sum, ModP.preVal_eq_zero, agm_zero_right, MeasureTheory.ProbabilityMeasure.null_iff_toMeasure_null, MeasureTheory.Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure, Valuation.RankOne.hom_eq_zero_iff, exists_continuous_add_one_of_isCompact_nnreal, HolderTriple.nonneg, Metric.isCover_zero, MeasureTheory.distribHaarChar_pos, LinearMap.injective_iff_antilipschitz, ENNReal.instPosSMulStrictMonoNNReal, tsum_pos, ContinuousMapZero.continuous_toNNReal, continuousOn_cfcβ_nnreal_setProd, ENNReal.toNNReal_pos_iff, tendsto_cofinite_zero_of_summable, HasOuterApproxClosed.exAppr, EMetric.exists_pos_forall_lt_edist, nndist_zero_eq_val, nnnorm_pos, ContinuousMapZero.toNNReal_apply, LipschitzWith.zero_iff, CompactlySupportedContinuousMap.nnrealPart_neg_eq_zero_of_nonneg, BoundedContinuousFunction.apply_le_nndist_zero, Metric.externalCoveringNumber_zero, BoundedContinuousFunction.NNReal.upper_bound, coe_single, CompactlySupportedContinuousMap.exists_add_nnrealPart_add_eq, ENNReal.coe_indicator, ProbabilityTheory.cauchyMeasure_zero_scale, Metric.exists_pos_forall_lt_edist, MeasureTheory.Lp.nnnorm_zero, iInf_const_zero, rpow_pos, MeasureTheory.SimpleFunc.map_coe_ennreal_restrict, BoundedContinuousFunction.lintegral_le_edist_mul, tendsto_pow_atTop_nhds_zero_iff, MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite, HolderTriple.one_div_pos', holderTriple_iff, FormalMultilinearSeries.comp_summable_nnreal, rieszContentAux_le, ENNReal.toNNReal_zero, Delone.DeloneSet.coveringRadius_pos, ProbabilityTheory.Kernel.HasSubgaussianMGF.fun_zero, IsCoercive.antilipschitz, MeasureTheory.FiniteMeasure.null_iff_toMeasure_null
|
orderIsoIccZeroCoe π | CompOp | 2 mathmath: orderIsoIccZeroCoe_apply_coe_coe, orderIsoIccZeroCoe_symm_apply_coe
|
toReal π | CompOp | 544 mathmath: SpectrumRestricts.le_nnreal_iff, MeasureTheory.exists_lt_lowerSemicontinuous_integral_gt_nnreal, MeasureTheory.tendsto_integral_thickenedIndicator_of_isClosed, PiLp.norm_toLp_const', orderIsoIccZeroCoe_apply_coe_coe, summable_coe, SchauderBasis.norm_proj_le_nnnormProjBound, HasDerivAt.le_of_lipschitz, toReal_lt, LipschitzOnWith.norm_sub_le, MeasureTheory.integrable_withDensity_iff_integrable_coe_smul, ProbabilityTheory.measure_sum_ge_le_of_HasCondSubgaussianMGF, NumberField.mixedEmbedding.convexBodyLT'_mem, ContractingWith.dist_fixedPoint_le, ProbabilityTheory.variance_fun_id_gaussianReal, coe_indicator, BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub, HolderOnWith.interpolate, Seminorm.finset_sup_apply, ODE.FunSpace.dist_comp_iterate_next_le, ProbabilityTheory.hasSum_integral_poissonMeasure, HolderWith.edist_le_of_le, coe_toRealHom, LipschitzWith.dist_le_mul, PiLp.norm_toLp_one, PMF.bernoulli_expectation, HolderWith.of_le, LipschitzWith.norm_inv_mul_le_of_le, MeasureTheory.smul_le_stoppedValue_hittingBtwn, FormalMultilinearSeries.norm_le_div_pow_of_pos_of_lt_radius, Pi.norm_def', canLift, HolderOnWith.comp, ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse, NumberField.FinitePlace.norm_def', coe_sSup, NormedAddGroupHom.opNorm_le_of_lipschitz, ODE.FunSpace.range_toContinuousMap, MeasureTheory.hasFiniteIntegral_iff_ofNNReal, LipschitzWith.norm_sub_le_of_le, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal, egauge_ball_le_of_one_lt_norm, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div, HasConstantSpeedOnWith.ratio, ContinuousMap.toNNReal_neg_algebraMap, coe_le_one, ProbabilityTheory.cgf_gaussianReal, ProbabilityTheory.HasSubgaussianMGF.mgf_le, HasFDerivAt.le_of_lipschitzOn, ContinuousMap.coeNNRealReal_apply, Dilation.mapsTo_sphere, enorm_eq, AntilipschitzWith.mul_le_dist, Real.le_toNNReal_iff_coe_le, coe_add, coe_iSup, Metric.ediam_thickening_le, ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero, ContinuousMap.toLp_norm_le, coe_div, Metric.exists_continuous_nnreal_forall_closedBall_subset, coe_nndist, HolderOnWith.ediam_image_le_of_subset_of_le, LipschitzWith.dist_le_mul_of_le, enorm_fderiv_norm_rpow_le, aemeasurable_coe_nnreal_real_iff, MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part, young_inequality, map_coe_atTop, antilipschitzWith_iff_le_mul_dist, NumberField.mixedEmbedding.convexBodyLT_mem, ENNReal.coe_toReal, AntilipschitzWith.le_mul_norm, LipschitzWith.le_add_mul, Metric.isCover_iff_subset_cthickening, algebraMap_eq_coe, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex, coe_nnnorm', CStarMatrix.norm_le_of_forall_inner_le, HolderOnWith.nndist_le_of_le, AntilipschitzWith.le_mul_dist, image_coe_uIoc, image_coe_Ico, coe_rpow, Real.coe_toNNReal_le, norm_algebraMap_nnreal, LipschitzWith.norm_div_le, similar_iff_exists_dist_eq, HolderWith.holderWith_zero_of_bounded, norm_lineDeriv_le_of_lipschitz, CompactlySupportedContinuousMap.toRealLinearMap_apply_apply, MeasureTheory.integrable_thickenedIndicator, AntilipschitzWith.le_mul_norm', coe_eq_zero, lipschitzOnWith_iff_norm_inv_mul_le, LipschitzOnWith.norm_sub_le_of_le, Real.toNNReal_eq_iff_eq_coe, ContinuousMap.toNNReal_algebraMap, Differentiable.hasFPowerSeriesOnBall, image_coe_uIcc, Seminorm.ball_smul, isCoboundedUnder_le_toReal, coe_prod, Real.coe_toNNReal', PseudoMetricSpace.le_two_mul_dist_ofPreNNDist, dist_le_of_approx_trajectories_ODE, NumberField.HeightOneSpectrum.adicAbv_def, continuous_coe, ContractingWith.aposteriori_dist_iterate_fixedPoint_le, bddBelow_coe, Similar.exists_dist_eq, LipschitzOnWith.norm_neg_add_le, isEmbedding_coe, cfc_real_eq_nnreal, ODE.FunSpace.dist_iterate_iterate_next_le_of_lipschitzWith, LipschitzWith.mapsTo_ball, coe_multiset_prod, comap_coe_atTop, PseudoMetricSpace.dist_ofPreNNDist, dist_le_coe, coe_mem_spectrum_real_of_nonneg, ContractingWith.apriori_dist_iterate_fixedPoint_le, one_le_coe, HolderConjugate.coe, SpectrumRestricts.nnreal_lt_iff, coe_zero, ProbabilityTheory.HasCondSubgaussianMGF.ae_condExp_le, IsPicardLindelof.lipschitzOnWith, range_coe, isClosedEmbedding_coe, map_coe_nhdsGT, norm_fderiv_le_of_lipschitz, image_coe_Iio, HolderWith.ediam_image_le, isBoundedUnder_ge_toReal, Real.coe_nnabs, Dilation.mapsTo_closedBall, lipschitz_with_lipschitz_const_mul, MeasureTheory.Submartingale.eLpNorm_stoppedAbove_le, ENNReal.log_of_nnreal, lipschitzOnWith_iff_norm_div_le, cfc_nnreal_eq_real, ProbabilityTheory.complexMGF_gaussianReal, PseudoMetricSpace.dist_ofPreNNDist_le, Metric.ediam_cthickening_le, LipschitzOnWith.norm_inv_mul_le, MeasureTheory.tendsto_indicator_ge, MeasureTheory.MemLp.eLpNormEssSup_indicator_norm_ge_eq_zero, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq_inner, coe_mk, CompactlySupportedContinuousMap.toRealPositiveLinear_apply, ProbabilityTheory.cauchyPDFReal_def, norm_deriv_le_of_lipschitzOn, similar_iff_exists_pairwise_dist_eq, HasFPowerSeriesWithinOnBall.uniform_geometric_approx', eq_iff, QuasispectrumRestricts.le_nnreal_iff, ProbabilityTheory.HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun, BoxIntegral.Box.dist_le_distortion_mul, MeasureTheory.Lp.coe_nnnorm, CompactlySupportedContinuousMap.toReal_apply, PositiveLinearMap.exists_norm_apply_le, val_eq_coe, ContractingWith.dist_le_mul, StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal, SpectrumRestricts.nnreal_le_iff, BoundedContinuousFunction.abs_self_eq_nnrealPart_add_nnrealPart_neg, LipschitzWith.dist_iterate_succ_le_geometric, ProbabilityTheory.mgf_fun_id_gaussianReal, ENNReal.coe_toNNReal_eq_toReal, IsPicardLindelof.continuousOn_uncurry, Metric.emetric_ball_nnreal, MeasureTheory.MemLp.integral_indicator_norm_ge_nonneg_le_of_meas, nnrpow_def, MeasureTheory.Submartingale.eLpNorm_stoppedAbove_le', sub_def, ProbabilityTheory.gaussianPDFReal_def, LipschitzWith.dist_lt_mul_of_lt, coe_lt_one, dist_nndist, lipschitzWith_iff_norm_div_le, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one, MeasureTheory.eLpNorm_nnreal_eq_eLpNorm', Real.toNNReal_lt_iff_lt_coe, OneHomClass.bound_of_antilipschitz, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt', coe_comp_nnnorm', geom_mean_le_arith_mean4_weighted, FormalMultilinearSeries.isLittleO_one_of_lt_radius, dimH_eq_iInf, ProbabilityTheory.variance_continuousLinearMap_gaussianReal, lipschitzWith_iff_norm_sub_le, coe_natCast, geom_mean_le_arith_mean2_weighted, MeasureTheory.lpNorm_nnreal_eq_integral_norm_rpow, image_coe_Ioc, HasFPowerSeriesOnBall.tendstoUniformlyOn, ContinuousLinearMap.NonlinearRightInverse.bound, MeasureTheory.smul_le_stoppedValue_hitting, coe_sum, ContinuousLinearMap.opNorm_extend_le, le_radius_cauchyPowerSeries, AntilipschitzWith.le_mul_norm_div, UnconditionalSchauderBasis.norm_proj_le_nnnormProjBound, QuasispectrumRestricts.lt_nnreal_iff, CompactlySupportedContinuousMap.integralLinearMap_apply, MeasureTheory.llr_smul_nnreal_left, isBoundedUnder_le_toReal, image_coe_Ici, LipschitzOnWith.norm_div_le_of_le, Pi.norm_def, BoundedContinuousFunction.Lp_norm_le, Set.OrdConnected.image_coe_nnreal_real, isCoboundedUnder_ge_toReal, coe_min, coe_nnqsmul, HolderOnWith.holderOnWith_zero_of_bounded, HolderWith.comp_holderOnWith, LipschitzWith.norm_neg_add_le_of_le, Seminorm.closedBall_smul, NumberField.FinitePlace.norm_def_int, Measurable.coe_nnreal_real, coe_two, coe_nsmul, norm_deriv_le_of_lipschitz, spectralNorm_smul, cfcβ_real_eq_nnreal, PMF.binomial_apply_of_le, MeasureTheory.Measure.haarScalarFactor_eq_integral_div, HasFPowerSeriesOnBall.tendstoUniformlyOn', coe_ofScientific, coe_real_pi, hasFPowerSeriesOn_cauchy_integral, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt, DifferentiableOn.hasFPowerSeriesOnBall, MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le, CFC.rpow_sqrt_nnreal, LipschitzWith.norm_neg_add_le, LipschitzOnWith.le_add_mul, Dilation.mapsTo_ball, MeasureTheory.eLpNorm_nnreal_eq_lintegral, Real.coe_toNNReal, LipschitzWith.norm_sub_le, ENNReal.toReal_le_coe_of_le_coe, LipschitzOnWith.norm_div_le, HasFPowerSeriesOnBall.uniform_geometric_approx', LipschitzWith.norm_le_mul, MeasureTheory.Lp.norm_le_of_ae_bound, coe_inv, norm_lineDeriv_le_of_lipschitzOn, Delone.DeloneSet.packingRadius_lt_dist_of_mem_ne, smul_def, ODE.FunSpace.exists_forall_closedBall_funSpace_dist_le_mul, ContractingWith.dist_inequality, MeasureTheory.MemLp.integral_indicator_norm_ge_nonneg_le, ProbabilityTheory.cauchyPDFReal_def', MeasureTheory.JordanDecomposition.coe_smul, FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius, ENNReal.ofReal_lt_coe_iff, coe_sub_def, ProbabilityTheory.HasSubgaussianMGF.measureReal_le_le_exp, IsPicardLindelof.norm_le, Metric.coe_infNndist, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, ball_zero_eq_Ico', HolderTriple.coe, ProbabilityTheory.HasSubgaussianMGF.cgf_le, spectrum.coe_le_norm_of_mem, ENNReal.tsum_coe_ne_top_iff_summable_coe, ODE.FunSpace.mem_closedBall, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn, ENNReal.ofReal_le_coe, coe_expect, ProbabilityTheory.poissonMeasure_singleton, LipschitzOnWith.iff_le_add_mul, holderTriple_coe_iff, BoxIntegral.Box.diam_Icc_le_of_distortion_le, lipschitzWith_iff_dist_le_mul, ProbabilityTheory.integral_poissonMeasure, MeasureTheory.MemLp.integral_indicator_norm_ge_le, MeasureTheory.norm_stoppedValue_leastGE_le, MeasureTheory.Measure.toSphereBallBound_mul_measureReal_unitBall_le_toSphere_ball, InformationTheory.toReal_klDiv_smul_right_eq_smul_left, Mathlib.Meta.Positivity.nnreal_coe_pos, Real.le_toNNReal_iff_coe_le', dist_lt_coe, NormedAddGroupHom.ofLipschitz_norm_le, ZeroHomClass.bound_of_antilipschitz, iInf_real_pos_eq_iInf_nnreal_pos, ProbabilityTheory.measure_sum_ge_le_of_hasCondSubgaussianMGF, ContinuousOn.ofReal_map_toNNReal, CompactlySupportedContinuousMap.toNNRealLinear_apply, geom_mean_le_arith_mean_weighted, image_coe_Iic, spectrum.differentiableOn_inverse_one_sub_smul, ProbabilityTheory.variance_id_gaussianReal, MeasureTheory.FiniteMeasure.measureReal_eq_coe_coeFn, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt, FormalMultilinearSeries.isLittleO_of_lt_radius, aemeasurable_withDensity_iff, PiLp.norm_toLp_const, MeasureTheory.lpNorm_const_smul, ContractingWith.dist_le_of_fixedPoint, nnnorm_fderiv_norm_rpow_le, abs_eq, orderIsoIccZeroCoe_symm_apply_coe, BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le, PadicAlgCl.valuation_coe, ODE.FunSpace.dist_iterate_next_le, InformationTheory.toReal_klDiv_smul_right, MeasureTheory.SimpleFunc.map_coe_nnreal_restrict, coe_mono, HasFDerivAt.le_of_lipschitz, ContractingWith.one_sub_K_pos, ODE.FunSpace.dist_iterate_next_iterate_next_le, coe_nnnorm, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt', AntilipschitzWith.le_mul_norm_sub, LipschitzWith.iff_le_add_mul, LipschitzOnWith.dist_le_mul, Real.nnabs_coe, image_coe_Ioi, holderConjugate_coe_iff, Metric.emetric_closedBall_nnreal, IsPicardLindelof.mul_max_le, dist_le_of_approx_trajectories_ODE_of_mem, IsUltrametricDist.isUltrametricDist_iff_isNonarchimedean_nnnorm, HolderOnWith.ediam_image_le_of_le, coe_pow, LipschitzWith.norm_div_le_of_le, CFC.exists_measure_nnrpow_eq_integral_cfcβ_rpowIntegrandββ, ApproximatesLinearOn.closedBall_subset_target, HasFPowerSeriesWithinOnBall.tendstoUniformlyOn, HasLineDerivAt.le_of_lipschitzOn, ENNReal.coe_nnreal_eq, Metric.frontier_cthickening_disjoint, HolderOnWith.comp_holderWith, measurable_coe_nnreal_real, coe_nonneg, ENNReal.ofReal_coe_nnreal, NormedAddGroupHom.lift_norm_le, isUniformEmbedding_coe, MeasureTheory.ae_bdd_condExp_of_ae_bdd, ProbabilityTheory.HasSubgaussianMGF.measure_ge_le, lipschitzOnWith_iff_dist_le_mul, ProbabilityTheory.poissonMeasure_real_singleton, coe_iInf, coe_mulIndicator, image_coe_Ioo, nnnorm_eq, BoundedContinuousFunction.toReal_lintegral_coe_eq_integral, ENNReal.tsum_coe_eq_top_iff_not_summable_coe, ConvexBody.iInter_smul_eq_self, dist_pi_def, InformationTheory.toReal_klDiv_smul_same, MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq, hausdorffMeasure_of_dimH_lt, coe_lt_coe, lipschitzOnWith_iff_norm_neg_add_le, MeasureTheory.integrable_withDensity_iff_integrable_coe_smulβ, ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun, Valued.toNormedField.norm_def, toReal_le, BoundedContinuousFunction.toLp_norm_le, Similar.exists_pairwise_dist_eq, unitInterval.coe_toNNReal, ProbabilityTheory.complexMGF_id_gaussianReal, Valuation.norm_def, HasFPowerSeriesWithinOnBall.tendstoUniformlyOn', MeasureTheory.MemLp.eLpNorm_indicator_norm_ge_pos_le, norm_fderiv_le_of_lipschitzOn, Dilation.diam_range, ContinuousLinearMap.opNorm_le_iff_lipschitz, EReal.coe_nnreal_eq_coe_real, Dilation.diam_image, Real.toNNReal_coe, MeasureTheory.maximal_ineq, LipschitzWith.norm_le_mul', MeasureTheory.lintegral_coe_le_coe_iff_integral_le, coe_multiset_sum, ProbabilityTheory.meas_ge_le_evariance_div_sq, coe_image, coe_ofNat, cfcβ_nnreal_eq_real, coe_pos, LipschitzOnWith.norm_neg_add_le_of_le, div_le_egauge_ball, CompactlySupportedContinuousMap.eq_toRealPositiveLinear_toReal, CFC.nnrpow_eq_cfcβ_real, Set.OrdConnected.preimage_coe_nnreal_real, Metric.IsCover.subset_iUnion_closedBall, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, HolderOnWith.of_le, ProbabilityTheory.mgf_gaussianReal, coe_injective, Metric.IsCover.subset_cthickening, MeasureTheory.Integrable.real_toNNReal, Real.toNNReal_le_iff_le_coe, ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le, ProbabilityTheory.variance_linearMap_gaussianReal, ProbabilityTheory.mgf_id_gaussianReal, HolderOnWith.edist_le, Real.nnreal_trichotomy, ODE.FunSpace.mem_closedBallβ, HolderOnWith.ediam_image_inter_le_of_le, isometry_coe, CFC.sqrt_rpow_nnreal, ProbabilityTheory.hasSum_one_poissonMeasure, toReal_limsup, coe_mul, MeasureTheory.Measure.haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos, coe_comp_nnnorm, MeasureTheory.ProbabilityMeasure.measureReal_eq_coe_coeFn, geom_mean_le_arith_mean3_weighted, tendsto_coe, Real.nnreal_dichotomy, ContractingWith.fixedPoint_lipschitz_in_map, Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable, Metric.isCover_iff_subset_iUnion_closedBall, LipschitzWith.norm_inv_mul_le, HolderOnWith.dist_le, HolderWith.edist_le, HolderWith.dist_le_of_le, div_le_egauge_closedBall, dist_le_of_trajectories_ODE, CFC.nnrpow_eq_rpow, SpectrumRestricts.nnreal_iff_spectralRadius_le, FormalMultilinearSeries.radius_eq_top_iff_summable_norm, HolderOnWith.ediam_image_inter_le, dist_eq, tendsto_coe_atTop, coe_one, Dilation.dist_eq, tendsto_coe', zero_le_coe, Metric.cthickening_subset_thickening, Metric.eball_coe, coe_mulSingle, HolderOnWith.nndist_le, FormalMultilinearSeries.summable_norm_mul_pow, MeasureTheory.exists_upperSemicontinuous_le_integral_le, SemiNormedGrp.explicitCokernelDesc_norm_le_of_norm_le, one_lt_coe, hasSum_coe, closedBall_zero_eq_Icc', Real.coe_sqrt, MeasureTheory.stoppedAbove_le, HolderWith.dist_le, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith, LipschitzWith.mapsTo_closedBall, NNRealRMK.integral_rieszMeasure, ODE.FunSpace.compProj_mem_closedBall, lipschitzWith_iff_norm_inv_mul_le, DiffContOnCl.hasFPowerSeriesOnBall, Metric.closedEBall_coe, coe_tsum, coe_list_sum, toReal_eq, Real.lt_toNNReal_iff_coe_lt, MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral, Metric.uniformity_edist_aux, ContractingWith.dist_fixedPoint_fixedPoint_of_dist_le', NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, HolderOnWith.ediam_image_le, NumberField.FinitePlace.norm_embedding', HolderOnWith.edist_le_of_le, lipschitzWith_iff_norm_neg_add_le, MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div_of_continuous_nonneg_pos, coe_zpow, toReal_liminf, AEMeasurable.coe_nnreal_real, Polynomial.finite_mahlerMeasure_le, ProbabilityTheory.charFun_gaussianReal, IsUltrametricDist.isNonarchimedean_nnnorm, LipschitzWith.diam_image_le, SpectrumRestricts.lt_nnreal_iff, ProbabilityTheory.integrable_poissonMeasure_iff, LipschitzWith.norm_compLp_le, image_coe_Icc, HolderOnWith.hausdorffMeasure_image_le, hasConstantSpeedOnWith_iff_ordered, dimH_def, coe_le_coe, HasLineDerivAt.le_of_lipschitz, coe_inj, Real.exists_lt_of_strictMono, ContinuousLinearMap.bound_of_antilipschitz, ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_le, ContinuousLinearMap.NonlinearRightInverse.bound', image_coe_uIoo, CFC.nnnorm_nnrpow, ProbabilityTheory.integral_poissonMeasure', coe_eq_one, HolderOnWith.ediam_image_le_of_subset, BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg, coe_list_prod, NumberField.FinitePlace.norm_embedding_int, FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius, LipschitzOnWith.norm_inv_mul_le_of_le, CFC.norm_nnrpow, HolderWith.interpolate, coe_sub_of_lt, bddAbove_coe, ODE.FunSpace.dist_iterate_next_apply_le, dist_le_of_trajectories_ODE_of_mem, MeasureTheory.lintegral_coe_eq_integral, MeasureTheory.integral_coe_le_of_lintegral_coe_le, HolderWith.nndist_le, InformationTheory.toReal_klDiv_smul_left, LipschitzWith.norm_compLp_sub_le, SpectrumRestricts.nnreal_iff_nnnorm, MeasureTheory.llr_smul_nnreal_right, HasDerivAt.le_of_lipschitzOn, map_coe_nhdsGE, HolderWith.comp, lipschitzOnWith_iff_norm_sub_le, coe_single, measurable_coe_nnreal_real_iff, aestronglyMeasurable_withDensity_iff, Polynomial.card_mahlerMeasure_le_prod, Matrix.linfty_opNorm_def, NumberField.house_eq_sup', ContinuousLinearMap.opNorm_le_of_lipschitz, hasConstantSpeedOnWith_iff_variationOnFromTo_eq, NumberField.FinitePlace.norm_def, norm_eq, coe_max, MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le', coe_sub, lipschitz_with_lipschitz_const_add, Matrix.norm_eq_sup_sup_nnnorm, ENNReal.coe_lt_ofReal, hausdorffMeasure_of_lt_dimH, MeasureTheory.MemLp.eLpNorm_indicator_norm_ge_le, Delone.DeloneSet.exists_dist_le_coveringRadius, MeasureTheory.measureReal_nnreal_smul_apply, HolderOnWith.dist_le_of_le, Real.le_coe_toNNReal, SeparationQuotient.liftNormedAddGroupHom_norm_le, HolderWith.nndist_le_of_le, MeasureTheory.BorelCantelli.process_difference_le, BoundedContinuousFunction.integrable_of_nnreal, coe_sInf
|
toRealHom π | CompOp | 1 mathmath: coe_toRealHom
|
zpow π | CompOp | 14 mathmath: rpow_intCast_mul, rpow_mul_intCast, ENNReal.coe_zpow, rpow_add_intCast', WithZeroMulInt.toNNReal_neg_apply, DilationEquiv.ratio_zpow, rpow_intCast, rpow_add_intCast, Real.toNNReal_zpow, exists_mem_Ico_zpow, coe_zpow, nnnorm_zpow, rpow_sub_intCast', exists_mem_Ioc_zpow
|
Β«termββ₯0Β» π | CompOp | β |