| Metric | Count |
|---|
DefinitionsevalNNRealtoReal, evalRealNNAbs, evalRealToNNReal, gi, instAlgebraOfReal, instCoeReal, instConditionallyCompleteLinearOrderBot, instDistribMulActionOfReal, instDiv, instInv, instLinearOrder, instLinearOrderedCommGroupWithZero, instMax, instMin, instModuleOfReal, instMulActionOfReal, instNNRatCast, instOrderBot, instSMulNNRat, instSemifield, instSub, orderIsoIccZeroCoe, toReal, toRealHom, zpow, «termℝ≥0», nnabs, toNNReal, instAddCancelCommMonoidNNReal, instCommMonoidWithZeroNNReal, instCommSemiringNNReal, instDistribLatticeNNReal, instInhabitedNNReal, instNontrivialNNReal, instOneNNReal, instPartialOrderNNReal, instReprNNReal, instSemilatticeInfNNReal, instSemilatticeSupNNReal, instSemiringNNReal, instZeroNNReal | 41 |
Theoremsnnabs_pos_of_pos, nnreal_coe_pos, abs_eq, addLeftMono, addLeftReflectLT, algebraMap_eq_coe, bddAbove_coe, bddBelow_coe, bot_eq_zero, canLift, coe_add, coe_div, coe_eq_one, coe_eq_zero, coe_iInf, coe_iSup, coe_image, coe_inj, coe_injective, coe_inv, coe_le_coe, coe_le_one, coe_lt_coe, coe_lt_one, coe_max, coe_min, coe_mk, coe_mono, coe_mul, coe_natCast, coe_ne_one, coe_ne_zero, coe_nnqsmul, coe_nonneg, coe_nsmul, coe_ofNat, coe_ofScientific, coe_one, coe_pos, coe_pow, coe_sInf, coe_sSup, coe_sub, coe_sub_def, coe_toRealHom, coe_two, coe_zero, coe_zpow, div_le_of_le_mul, div_le_of_le_mul', div_lt_one_of_lt, eq, eq_iff, exists, exists_lt_of_strictMono, exists_mem_Ico_zpow, exists_mem_Ioc_zpow, exists_nat_pos_inv_lt, exists_pow_lt_of_lt_one, forall, half_le_self, half_lt_self, iInf_const_zero, iInf_empty, iSup_empty, iSup_eq_zero, iSup_of_not_bddAbove, instArchimedean, instCanonicallyOrderedAdd, instDenselyOrdered, instIsOrderedRing, instIsScalarTowerOfReal, instIsStrictOrderedModule, instIsStrictOrderedRing, instMulArchimedean, instNoZeroDivisors, instOrderedSub, instPosSMulStrictMono, instSMulPosStrictMono, inv_le, inv_le_of_le_mul, inv_lt_inv, inv_lt_one_iff, le_inv_iff_mul_le, le_of_forall_lt_one_mul_le, le_toNNReal_of_coe_le, lt_iff_exists_rat_btwn, lt_inv_iff_mul_lt, mk_natCast, mk_one, mk_zero, mulLeftMono, mul_eq_mul_left, mul_lt_of_lt_div, mul_sup, ne_iff, one_le_coe, one_lt_coe, orderIsoIccZeroCoe_apply_coe_coe, orderIsoIccZeroCoe_symm_apply_coe, pow_antitone_exp, sInf_empty, sSup_of_not_bddAbove, smulCommClass_left, smulCommClass_right, smul_def, sub_def, sup_mul, val_eq_coe, zero_le_coe, cast_natAbs_eq_nnabs_cast, coe_nnabs, coe_toNNReal, coe_toNNReal', coe_toNNReal_le, exists_lt_of_strictMono, le_coe_toNNReal, le_toNNReal_iff_coe_le, le_toNNReal_iff_coe_le', lt_of_toNNReal_lt, lt_toNNReal_iff_coe_lt, natCast_le_toNNReal, natCast_lt_toNNReal, natCastle_toNNReal', nnabs_coe, nnabs_of_nonneg, nnabs_pos, nnreal_dichotomy, nnreal_induction_on, nnreal_induction_on', nnreal_trichotomy, ofNat_le_toNNReal, ofNat_lt_toNNReal, one_le_toNNReal, one_lt_toNNReal, toNNReal_abs, toNNReal_add, toNNReal_add_le, toNNReal_add_toNNReal, toNNReal_coe, toNNReal_coe_nat, toNNReal_div, toNNReal_div', toNNReal_eq_iff_eq_coe, toNNReal_eq_natCast, toNNReal_eq_ofNat, toNNReal_eq_one, toNNReal_eq_toNNReal_iff, toNNReal_eq_zero, toNNReal_inv, toNNReal_le_iff_le_coe, toNNReal_le_natCast, toNNReal_le_ofNat, toNNReal_le_one, toNNReal_le_toNNReal, toNNReal_le_toNNReal_iff, toNNReal_le_toNNReal_iff', toNNReal_le_toNNReal_iff_of_pos, toNNReal_lt_iff_lt_coe, toNNReal_lt_natCast, toNNReal_lt_natCast', toNNReal_lt_ofNat, toNNReal_lt_one, toNNReal_lt_toNNReal_iff, toNNReal_lt_toNNReal_iff', toNNReal_lt_toNNReal_iff_of_nonneg, toNNReal_mono, toNNReal_monotone, toNNReal_mul, toNNReal_ofNat, toNNReal_of_nonneg, toNNReal_of_nonpos, toNNReal_one, toNNReal_pos, toNNReal_pow, toNNReal_zero, toNNReal_zpow, image_coe_nnreal_real, image_real_toNNReal, preimage_coe_nnreal_real, preimage_real_toNNReal | 181 |
| Total | 222 |
| Name | Category | Theorems |
|---|
gi 📖 | CompOp | — |
instAlgebraOfReal 📖 | CompOp | 73 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, nnnorm_algebraMap_nnreal, CFC.rpow_def, CFC.rpow_algebraMap, 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, 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, nonneg_iff_isSelfAdjoint_and_spectrumRestricts, Seminorm.const_isBounded, CFC.rpow_neg_one_eq_cfc_inv, IsSelfAdjoint.sq_spectrumRestricts, CStarAlgebra.mem_Icc_algebraMap_iff_nnnorm_le, Seminorm.closedBall_smul, nnnorm_cfc_nnreal_lt, nnnorm_cfc_nnreal_le, Nonneg.instContinuousFunctionalCalculus, cfcHom_nnreal_eq_restrict, upperHemicontinuous_spectrum_nnreal, range_cfc_nnreal, Unitization.nnreal_cfcₙ_eq_cfc_inr, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul, CFC.abs_algebraMap_nnreal, range_cfc_nnreal_eq_image_cfc_real, MeasureTheory.SignedMeasure.singularPart_smul_nnreal, MeasureTheory.JordanDecomposition.toSignedMeasure_smul, StarAlgHom.realContinuousMapOfNNReal_injective, Seminorm.finset_sup_smul, Seminorm.isBounded_sup, CFC.sqrt_eq_cfc, QuasispectrumRestricts.nnreal_of_nonneg, CompactlySupportedContinuousMap.toReal_smul, spectrum.isCompact_nnreal, CFC.sqrt_algebraMap, ContinuousLinearMap.IsPositive.spectrumRestricts, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, spectrum.instCompactSpaceNNReal, Commute.cfc_nnreal, 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, ENNReal.toReal_smul, 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, Nonneg.instIsometricContinuousFunctionalCalculus
|
instCoeReal 📖 | CompOp | — |
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
|
instDistribMulActionOfReal 📖 | CompOp | 31 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, 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 | 63 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', holderConjugate_one_div, CFC.sqrt_eq_nnrpow, PadicAlgCl.valuation_p, PadicComplex.valuation_p, nndist_midpoint_midpoint_le', Real.toNNReal_div', Delone.DeloneSet.mapBilipschitz_packingRadius, agm_eq_agm_gm_am, le_gm_and_am_le, 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, sqrt_mul_le_half_add, Metric.IsSeparated.image_antilipschitz, ENNReal.coe_div, dist_gm_am_le, agmSequences_succ, young_inequality_real, rpow_sub_intCast', ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc, HolderTriple.one_div_pos', finset_sup_div
|
instInv 📖 | CompOp | 81 mathmath: nnnorm_inv, HolderTriple.inv_eq, CFC.monotoneOn_one_sub_one_add_inv, MeasureTheory.Measure.rnDeriv_smul_right', ENNReal.coe_inv, AntilipschitzWith.mul_le_nndist, 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, 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₀, HolderConjugate.one_sub_inv_inv, hasSum_geometric, Set.InvOn.one_sub_one_add_inv, 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, HolderConjugate.inv_inv, ENNReal.coe_inv_le, HolderTriple.inv_add_inv_eq_inv, Probability.cauchyPDFReal_def', le_inv_iff_mul_le, HasStrictFDerivAt.approximates_deriv_on_open_nhds, inv_lt_inv, HolderConjugate.one_sub_inv, antilipschitzWith_mul_left, rpow_neg, 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, tsum_geometric_nnreal, Mathlib.Meta.NormNum.nnreal_rpow_isRat_eq_inv_nnreal_rpow, ENNReal.toNNReal_inv, egauge_le_of_smul_mem_of_ne, Mathlib.Meta.NormNum.IsInt.nnreal_rpow_eq_inv_nnreal_pow, holderTriple_iff, ContinuousLinearMap.antilipschitz_of_forall_le_inner_map
|
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 | 32 mathmath: PadicComplex.valuation_extends, PadicComplex.coe_eq, PadicComplex.norm_def, PadicComplex.coe_natCast, Valued.integer.exists_norm_lt_one, WithZeroMulInt.toNNReal_lt_one_iff, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, PadicAlgCl.instUniformContinuousConstSMulPadic, PadicAlgCl.valuation_p, PadicComplex.valuation_p, WithZeroMulInt.toNNReal_le_one_iff, Valued.integer.norm_le_one, PadicComplex.isNonarchimedean, PadicComplex.instIsScalarTowerPadicPadicAlgCl, Valued.integer.coe_span_singleton_eq_closedBall, 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, WithZeroMulInt.toNNReal_strictMono, PadicComplex.norm_extends, Valued.integer.mem_iff, Valued.integer.isUnit_iff_norm_eq_one, PadicComplex.rankOne_hom_eq, NormedField.valuation_apply, Valued.integer.norm_coe_unit, PadicComplex.nnnorm_extends, Valued.integer.exists_norm_coe_lt_one, PadicComplexInt.integers
|
instMax 📖 | CompOp | 39 mathmath: BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot', Fin.nndist_insertNth_insertNth, agm_lt_max_of_ne, ENNReal.coe_max, BoxIntegral.TaggedPrepartition.distortion_disjUnion, LipschitzOnWith.prodMk, 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_sup, nndist_eq, ContinuousMultilinearMap.opNNNorm_prod, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, BoxIntegral.Prepartition.distortion_disjUnion, WithLp.prod_nndist_eq_sup, WithLp.prod_nnnorm_eq_sup, LipschitzWith.max, PreTilt.valAux_add, Prod.nnnorm_mk', Unitization.nnnorm_eq_sup, sup_mul, IsUltrametricDist.nnnorm_div_eq_max_of_nnnorm_div_ne_nnnorm_div, BoxIntegral.TaggedPrepartition.distortion_unionComplToSubordinate, 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, IsUltrametricDist.nnnorm_add_le_max, Prod.nnnorm_mk, coe_max, agm_le_max, HolderWith.of_le_of_le
|
instMin 📖 | CompOp | 5 mathmath: ENNReal.coe_min, agmSequences_min_max, min_le_agm, coe_min, min_lt_agm_of_pos_of_ne
|
instModuleOfReal 📖 | CompOp | 31 mathmath: range_cfcₙ_nnreal, CFC.monotoneOn_one_sub_one_add_inv, 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, CompactlySupportedContinuousMap.toRealLinearMap_apply, CFC.nnrpow_def, Nonneg.instNonUnitalIsometricContinuousFunctionalCalculus, nonneg_iff_isSelfAdjoint_and_spectrumRestricts, range_cfcₙ_nnreal_eq_image_cfcₙ_real, cfcₙ_real_eq_nnreal, InnerProductGeometry.angle_eq_angle_add_angle_iff, Unitization.nnreal_cfcₙ_eq_cfc_inr, upperHemicontinuous_quasispectrum_nnreal, 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, instContinuousMapZero.UniqueHom, CStarAlgebra.nonneg_TFAE, quasispectrum.instCompactSpaceNNReal, nnnorm_cfcₙ_nnreal_le, continuousOn_cfcₙ_nnreal_setProd
|
instMulActionOfReal 📖 | CompOp | 17 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.finset_sup_smul, Seminorm.isBounded_sup, LinearMap.mem_span_iff_bound, instSMulPosStrictMono, Seminorm.smul_le_smul, instIsScalarTowerOfReal
|
instNNRatCast 📖 | CompOp | 5 mathmath: Real.nnnorm_nnratCast, RCLike.nnnorm_nnratCast, coe_ofScientific, Complex.nnnorm_nnratCast, ENNReal.coe_nnratCast
|
instOrderBot 📖 | CompOp | 24 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, 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, Matrix.linfty_opNNNorm_def, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, Matrix.linfty_opNorm_def, Matrix.norm_eq_sup_sup_nnnorm, finset_sup_div
|
instSMulNNRat 📖 | CompOp | 3 mathmath: coe_nnqsmul, NNRat.instContinuousSMulNNReal, RCLike.nnnorm_nnqsmul
|
instSemifield 📖 | CompOp | 9 mathmath: SpectrumRestricts.nnreal_of_nonneg, cfcₙHom_nnreal_eq_restrict, SpectrumRestricts.nnreal_iff, IsSelfAdjoint.sq_spectrumRestricts, cfcHom_nnreal_eq_restrict, coe_expect, ContinuousLinearMap.IsPositive.spectrumRestricts, SpectrumRestricts.nnreal_iff_spectralRadius_le, SpectrumRestricts.nnreal_iff_nnnorm
|
instSub 📖 | CompOp | 38 mathmath: 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, tsum_geometric_nnreal, AntilipschitzWith.add_lipschitzWith, ApproximatesLinearOn.to_inv, coe_sub, instOrderedSub
|
orderIsoIccZeroCoe 📖 | CompOp | 2 mathmath: orderIsoIccZeroCoe_apply_coe_coe, orderIsoIccZeroCoe_symm_apply_coe
|
toReal 📖 | CompOp | 477 mathmath: SpectrumRestricts.le_nnreal_iff, MeasureTheory.tendsto_integral_thickenedIndicator_of_isClosed, PiLp.norm_toLp_const', orderIsoIccZeroCoe_apply_coe_coe, summable_coe, HasDerivAt.le_of_lipschitz, 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, HolderWith.edist_le_of_le, coe_toRealHom, LipschitzWith.dist_le_mul, PiLp.norm_toLp_one, PMF.bernoulli_expectation, HolderWith.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, 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', 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.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, continuous_coe, ContractingWith.aposteriori_dist_iterate_fixedPoint_le, bddBelow_coe, Similar.exists_dist_eq, isEmbedding_coe, cfc_real_eq_nnreal, 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, 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, MeasureTheory.tendsto_indicator_ge, MeasureTheory.MemLp.eLpNormEssSup_indicator_norm_ge_eq_zero, coe_mk, CompactlySupportedContinuousMap.toRealPositiveLinear_apply, 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, NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, le_radius_cauchyPowerSeries, AntilipschitzWith.le_mul_norm_div, QuasispectrumRestricts.lt_nnreal_iff, CompactlySupportedContinuousMap.integralLinearMap_apply, 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, Valued.norm_def, 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, MeasureTheory.Measure.haarScalarFactor_eq_integral_div, HasFPowerSeriesOnBall.tendstoUniformlyOn', coe_ofScientific, coe_real_pi, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt, MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le, CFC.rpow_sqrt_nnreal, 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, 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, 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, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn, ENNReal.ofReal_le_coe, coe_expect, LipschitzOnWith.iff_le_add_mul, holderTriple_coe_iff, BoxIntegral.Box.diam_Icc_le_of_distortion_le, lipschitzWith_iff_dist_le_mul, MeasureTheory.MemLp.integral_indicator_norm_ge_le, MeasureTheory.norm_stoppedValue_leastGE_le, MeasureTheory.Measure.toSphereBallBound_mul_measureReal_unitBall_le_toSphere_ball, Mathlib.Meta.Positivity.nnreal_coe_pos, Real.le_toNNReal_iff_coe_le', dist_lt_coe, NormedAddGroupHom.ofLipschitz_norm_le, Probability.cauchyPDFReal_def', 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, MeasureTheory.SimpleFunc.map_coe_nnreal_restrict, coe_mono, HasFDerivAt.le_of_lipschitz, ContractingWith.one_sub_K_pos, 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, isUniformEmbedding_coe, ProbabilityTheory.HasSubgaussianMGF.measure_ge_le, lipschitzOnWith_iff_dist_le_mul, 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, hausdorffMeasure_of_dimH_lt, coe_lt_coe, MeasureTheory.integrable_withDensity_iff_integrable_coe_smul₀, ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun, BoundedContinuousFunction.toLp_norm_le, Similar.exists_pairwise_dist_eq, unitInterval.coe_toNNReal, ProbabilityTheory.complexMGF_id_gaussianReal, 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', coe_multiset_sum, ProbabilityTheory.meas_ge_le_evariance_div_sq, coe_image, coe_ofNat, cfcₙ_nnreal_eq_real, coe_pos, div_le_egauge_ball, CompactlySupportedContinuousMap.eq_toRealPositiveLinear_toReal, CFC.nnrpow_eq_cfcₙ_real, Set.OrdConnected.preimage_coe_nnreal_real, Metric.IsCover.subset_iUnion_closedBall, HolderOnWith.of_le, NumberField.toNNReal_valued_eq_adicAbv, 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, CFC.sqrt_rpow_nnreal, toReal_limsup, coe_mul, 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, Metric.isCover_iff_subset_iUnion_closedBall, 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.eball_coe, coe_mulSingle, HolderOnWith.nndist_le, FormalMultilinearSeries.summable_norm_mul_pow, 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, Metric.closedEBall_coe, coe_tsum, coe_list_sum, Real.lt_toNNReal_iff_coe_lt, MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral, Metric.uniformity_edist_aux, ContractingWith.dist_fixedPoint_fixedPoint_of_dist_le', HolderOnWith.ediam_image_le, HolderOnWith.edist_le_of_le, 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, 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, coe_eq_one, HolderOnWith.ediam_image_le_of_subset, BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg, coe_list_prod, FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius, CFC.norm_nnrpow, HolderWith.interpolate, bddAbove_coe, dist_le_of_trajectories_ODE_of_mem, MeasureTheory.integral_coe_le_of_lintegral_coe_le, HolderWith.nndist_le, LipschitzWith.norm_compLp_sub_le, SpectrumRestricts.nnreal_iff_nnnorm, 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, 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, HolderWith.nndist_le_of_le, MeasureTheory.BorelCantelli.process_difference_le, BoundedContinuousFunction.integrable_of_nnreal, Probability.cauchyPDFReal_def, 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 | — |
| Name | Category | Theorems |
|---|
instAddCancelCommMonoidNNReal 📖 | CompOp | — |
instCommMonoidWithZeroNNReal 📖 | CompOp | — |
instCommSemiringNNReal 📖 | CompOp | 264 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, MeasureTheory.Measure.WeaklyRegular.smul_nnreal, ENNReal.nnreal_smul_lt_top, MeasureTheory.Measure.rnDeriv_smul_right', MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply, Commute.cfcₙ_nnreal, MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top, MeasureTheory.smul_le_stoppedValue_hittingBtwn, QuasispectrumRestricts.nnreal_iff, MeasureTheory.Measure.haveLebesgueDecompositionSMul, MeasureTheory.le_eLpNorm_of_bddBelow, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal, MeasureTheory.Measure.coe_nnreal_smul_apply, NNReal.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, NNReal.isBoundedSMul, nnnorm_algebraMap_nnreal, 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, NNReal.algebraMap_eq_coe, norm_algebraMap_nnreal, MeasureTheory.addEquivAddHaarChar_smul_preimage, MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN, ENNReal.instSMulPosMonoNNReal, NNReal.instContinuousMap.UniqueHom, MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto, MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul, NNReal.strictConcaveOn_sqrt, ContinuousMap.toNNReal_algebraMap, Seminorm.ball_smul, NNReal.coe_prod, MeasureTheory.Measure.smul_measure_isAddInvariant_le_of_isCompact_closure, 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', NNReal.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, FormalMultilinearSeries.compAlongComposition_nnnorm, MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul, MeasureTheory.Measure.hausdorffMeasure_smul₀, Finset.nnnorm_prod_le', Seminorm.comp_smul, 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, NNReal.instStarOrderedRing, StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal, Nonneg.instNonUnitalIsometricContinuousFunctionalCalculus, MeasureTheory.Measure.toSignedMeasure_smul, MeasureTheory.hausdorffMeasure_lineMap_image, infEdist_smul₀, NumberField.mixedEmbedding.adjust_f, MeasureTheory.FiniteMeasure.instContinuousSMulNNReal, nonneg_iff_isSelfAdjoint_and_spectrumRestricts, MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul, MeasureTheory.Measure.measure_isAddHaarMeasure_eq_smul_of_isOpen, Seminorm.const_isBounded, MeasureTheory.Measure.instSMulCommClassDomMulActNNReal, MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure, ENNReal.nnreal_smul_lt_top_iff, CFC.rpow_neg_one_eq_cfc_inv, 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, range_cfcₙ_nnreal_eq_image_cfcₙ_real, MeasureTheory.JordanDecomposition.smul_posPart, edist_smul₀, MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure, MeasureTheory.FiniteMeasure.smul_testAgainstNN_apply, MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isEverywherePos, MeasureTheory.Measure.nnreal_smul_coe_apply, CStarAlgebra.mem_Icc_algebraMap_iff_nnnorm_le, Seminorm.closedBall_smul, nnnorm_cfc_nnreal_lt, 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, MeasureTheory.Measure.smul_measure_isMulInvariant_le_of_isCompact_closure, MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_nonzero, MeasureTheory.Measure.measure_isAddHaarMeasure_eq_smul_of_isEverywherePos, 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, NNReal.spectralRadius_mem_spectrum, MeasureTheory.Measure.map_right_mul_eq_modularCharacterFun_smul, MeasureTheory.addEquivAddHaarChar_smul_map, upperHemicontinuous_spectrum_nnreal, MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN, 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, MeasureTheory.Measure.measure_isAddLeftInvariant_eq_vadd_of_ne_top, CFC.abs_algebraMap_nnreal, upperHemicontinuous_quasispectrum_nnreal, MeasureTheory.Measure.mul_addHaarScalarFactor_smul, NNReal.geom_mean_le_arith_mean_weighted, MeasureTheory.Measure.integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, NNReal.instMeasurableSMul₂ENNReal, MeasureTheory.Measure.isMulLeftInvariant_eq_smul, 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, 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₀, NNReal.finset_prod_rpow, ContinuousMultilinearMap.opNNNorm_le_iff, MeasureTheory.FiniteMeasure.map_smul, Seminorm.finset_sup_smul, quasispectrum.isCompact_nnreal, Seminorm.isBounded_sup, CFC.sqrt_eq_cfc, MeasureTheory.addEquivAddHaarChar_smul_eq_comap, QuasispectrumRestricts.nnreal_of_nonneg, 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, MeasureTheory.maximal_ineq, 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, ENNReal.smul_toNNReal, StieltjesFunction.measure_smul, MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, spectrum.instCompactSpaceNNReal, MeasureTheory.Measure.Regular.smul_nnreal, MeasureTheory.isLocallyFiniteMeasureSMulNNReal, MeasureTheory.isFiniteMeasureSMulNNReal, MeasureTheory.Integrable.smul_measure_nnreal, MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop, NNReal.instMulArchimedean, Commute.cfc_nnreal, MeasureTheory.Measure.InnerRegularCompactLTTop.smul_nnreal, convex_setOf_holderOnWith, MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN, LinearMap.mem_span_iff_bound, MeasureTheory.Measure.IsEverywherePos.smul_measure_nnreal, MeasureTheory.Measure.haveLebesgueDecompositionSMulRight, Finset.nnnorm_prod_le, MeasureTheory.Measure.IsAddHaarMeasure.nnreal_smul, NNReal.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.isMulRightInvariant_smul_nnreal, MeasureTheory.isAddLeftInvariant_smul_nnreal, MeasureTheory.Measure.map_right_add_eq_addModularCharacterFun_vadd, MeasureTheory.hausdorffMeasure_homothety_preimage, MeasureTheory.FiniteMeasure.map_snd_prod, ENNReal.instMeasurableSMulNNReal, MeasureTheory.eLpNorm_smul_measure_of_ne_zero', quasispectrum.instCompactSpaceNNReal, NNReal.multiset_prod_map_rpow, MeasureTheory.OuterMeasure.mkMetric_nnreal_smul, ContinuousMultilinearMap.le_opNNNorm, MeasureTheory.Measure.singularPart_smul_right, nnnorm_cfcₙ_nnreal_le, ENNReal.instPosSMulStrictMonoNNReal, MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN, continuousOn_cfcₙ_nnreal_setProd, ENNReal.toReal_smul, NNReal.strictConcaveOn_rpow, MeasureTheory.Measure.isAddLeftInvariant_eq_smul, ProbabilityTheory.setBernoulli_apply, edist_smul_le, IsometricContinuousFunctionalCalculus.isGreatest_spectrum, MeasureTheory.Measure.addHaarScalarFactor_smul, MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul, MeasureTheory.integral_comap_eq_mulEquivHaarChar_smul, CStarAlgebra.nnnorm_mem_spectrum_of_nonneg, MeasureTheory.SignedMeasure.toJordanDecomposition_smul, MeasureTheory.Measure.singularPart_smul, 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, ContinuousAlternatingMap.le_of_opNNNorm_le, Nonneg.instIsometricContinuousFunctionalCalculus, NNReal.Icc_subset_segment, NNReal.concaveOn_rpow, ProbabilityTheory.setBernoulli_eq_map, MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isOpen
|
instDistribLatticeNNReal 📖 | CompOp | — |
instInhabitedNNReal 📖 | CompOp | — |
instNontrivialNNReal 📖 | CompOp | 30 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, 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'
|
instOneNNReal 📖 | CompOp | 240 mathmath: MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasure, LipschitzWith.id, Complex.nnnorm_exp_I_mul_ofReal, List.nnnorm_prod, LipschitzWith.prodMk_right, Dilation.ratio_one, NNReal.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, NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, LipschitzWith.mk_one, NumberField.mixedEmbedding.one_le_convexBodyLTFactor, thickenedIndicator_one_of_mem_closure, LipschitzWith.prod_snd, LinearIsometryEquiv.antilipschitz, LipschitzWith.holderWith, IsometryClass.lipschitz, EMetric.NonemptyCompacts.lipschitz_prod, Complex.lipschitz_equivRealProd, List.nnnorm_prod_le', TopologicalSpace.Compacts.lipschitz_prod, NNReal.coe_le_one, IsometryClass.antilipschitz, AntilipschitzWith.id, NNReal.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, nnnorm_one, lipschitzWith_sup_right, HasOuterApproxClosed.tendsto_apprSeq, LipschitzWith.of_edist_le, TopologicalSpace.Compacts.lipschitz_sup, SemilinearIsometryClass.lipschitz, thickenedIndicator_le_one, PiLp.antilipschitzWith_toLp, NNReal.isGreatest_Lp, Real.one_lt_toNNReal, LipschitzWith.dist_left, List.nnnorm_prod_le, NNReal.HolderConjugate.inv_add_inv_eq_one, LipschitzWith.of_le_add, lipschitzOnWith_cfc_fun_of_subset, Real.toNNReal_le_one, AffineIsometry.lipschitz, LipschitzWith.prod_fst, MeasureTheory.Measure.addModularCharacterFun_map_zero, LipschitzWith.projIcc, TopologicalSpace.NonemptyCompacts.lipschitz_prod, NNReal.one_le_coe, LipschitzWith.list_prod, ENNReal.toNNReal_one, lipschitzWith_one_norm', MeasureTheory.mulEquivHaarChar_refl, 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, PadicAlgCl.valuation_p, ENNReal.coe_one, PadicComplex.valuation_p, NNReal.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, Polynomial.cauchyBound_one, CStarAlgebra.nnnorm_le_one_iff_of_nonneg, NormedField.exists_one_lt_nnnorm, NNReal.list_prod_map_rpow', lipschitzOnWith_cfcₙ_fun, NNReal.HolderTriple.one_div_nonneg, SemilinearIsometryClass.antilipschitz, thickenedIndicator_tendsto_indicator_closure, ENNReal.one_eq_coe, Real.toNNReal_lt_one, UniformOnFun.lipschitzWith_eval, RCLike.lipschitzWith_re, MeasureTheory.L1.nnnorm_Integral_le_one, Set.InvOn.one_sub_one_add_inv, NNReal.HolderConjugate.conjugate_eq, NNReal.sqrt_eq_one, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id, 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, NNReal.lt_inv_iff_mul_lt, Real.one_le_toNNReal, CompletelyRegularSpace.exists_BCNN, Polynomial.one_le_cauchyBound, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, LinearIsometry.antilipschitz, LipschitzWith.prodMk_left, NNReal.one_le_sqrt, MeasureTheory.Measure.modularCharacterFun_map_one, lipschitzWith_negPart, MeasureTheory.FiniteMeasure.testAgainstNN_one, Real.lipschitzWith_toNNReal, NNReal.le_inv_iff_mul_le, ContinuousLinearMap.opNNNorm_mul, lipschitzWith_one_nnnorm, NNReal.HolderTriple.one_div_eq, lipschitzOnWith_cfcₙ_fun_of_subset, Valued.integer.exists_nnnorm_lt_one, Polynomial.cauchyBound_zero, LipschitzWith.eval, Isometry.lipschitz, DilationEquiv.ratio_refl, NNReal.HolderConjugate.one_sub_inv, NNReal.summable_one_div_rpow, WithZeroMulInt.toNNReal_eq_one_iff, exists_lt_rieszContentAux_add_pos, Submodule.lipschitzWith_starProjection, Int.nnnorm_coe_units, BoundedContinuousFunction.lipschitz_compContinuous, NNReal.HolderConjugate.div_conj_eq_sub_one, holderWith_id, LipschitzOnWith.of_le_add, NNReal.coe_mulIndicator, TopologicalSpace.NonemptyCompacts.lipschitz_sup, Complex.nnnorm_exp_ofReal_mul_I, GromovHausdorff.toGHSpace_lipschitz, NNReal.inv_le, 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, NNReal.sqrt_one, Real.lipschitzWith_cos, NNReal.HolderTriple.one_div_add_one_div, holderOnWith_one, ENNReal.one_lt_coe_iff, EMetric.Closeds.lipschitz_sup, IsUltrametricDist.nnnorm_natCast_le_one, AffineIsometryEquiv.lipschitz, NNReal.sqrt_le_one, MeasureTheory.ProbabilityMeasure.testAgainstNN_lipschitz, LinearIsometryEquiv.lipschitz, ContinuousMultilinearMap.nnnorm_ofSubsingleton_id, MeasureTheory.addEquivAddHaarChar_refl, Metric.lipschitz_infDist_set, NNReal.rpow_zero, thickenedIndicator_one, LipschitzOnWith.holderOnWith, unitInterval.toNNReal_symm_add_toNNReal, NNReal.one_rpow, BoundedContinuousFunction.lipschitz_eval_const, Polynomial.cauchyBound_X_add_C, CStarAlgebra.inr_mem_Icc_iff_nnnorm_le, ContinuousLinearMap.nnnorm_id, NNReal.HolderTriple.one_div_pos, NNReal.coe_one, Complex.nnnorm_I, IsUnifLocDoublingMeasure.one_le_scalingConstantOf, NNReal.coe_mulSingle, AffineIsometryEquiv.antilipschitz, Real.toNNReal_eq_one, Polynomial.cauchyBound_X_sub_C, NNReal.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, NNReal.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, NNReal.HolderConjugate.sub_one_mul_conj, NNReal.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, NNReal.holderConjugate_iff, one_le_thickenedIndicator_apply, EMetric.NonemptyCompacts.lipschitz_sup, NNReal.inv_lt_one_iff, HasOuterApproxClosed.apprSeq_apply_le_one, lipschitzWith_min, one_le_nnnorm_one, NNReal.coe_eq_one, UniformOnFun.lipschitzWith_restrict, NNReal.coe_list_prod, LipschitzWith.subtype_val, Metric.lipschitz_infNndist_pt, HasOuterApproxClosed.exAppr, 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, NNReal.tendsto_pow_atTop_nhds_zero_iff, UniformOnFun.lipschitzWith_one_ofFun_toFun', NNReal.HolderTriple.one_div_pos', MeasureTheory.BorelCantelli.process_difference_le, lipschitzWith_one_norm, UniformFun.lipschitzWith_eval, ContinuousMap.exists_mul_le_one_eqOn_ge
|
instPartialOrderNNReal 📖 | CompOp | 589 math, 2 bridgemath: SpectrumRestricts.le_nnreal_iff, MeasureTheory.FiniteMeasure.mass_map_le, NNReal.pow_arith_mean_le_arith_mean_pow, NNReal.orderIsoIccZeroCoe_apply_coe_coe, Matrix.frobenius_nnnorm_mul, Real.toNNReal_lt_natCast', IsometricContinuousFunctionalCalculus.isGreatest_nnnorm_spectrum, NNReal.HolderTriple.one_div_nonneg', eq_zero_or_nnnorm_pos, thickenedIndicator_mono_infEDist, nnnorm_le_insert', nnnorm_le_nnnorm_add_nnnorm_div', nnnorm_cfcₙ_nnreal_le_iff, WithLp.prod_nndist_eq_of_L2, Real.nnnorm_deriv_mulExpNegMulSq_le_one, ENNReal.exists_nnreal_pos_mul_lt, isCompact_setOf_finiteMeasure_le_of_isCompact, NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, AntilipschitzWith.mul_le_nndist, pi_nnnorm_le_iff, setOf_riemmanianEDist_lt_subset_nhds, NumberField.mixedEmbedding.one_le_convexBodyLTFactor, MeasureTheory.addEquivAddHaarChar_pos, nndist_pi_le_iff, Real.toNNReal_le_toNNReal_iff', eventually_enorm_mfderivWithin_symm_extChartAt_lt, Real.tendsto_toNNReal_atTop_iff, nnnorm_cfcₙ_lt_iff, CFC.nnnorm_sqrt, List.nnnorm_prod_le', nnnorm_nsmul_le, NNReal.sqrt_le_iff_le_sq, NNReal.sqrt_mul_lt_half_add_of_ne, IsGreatest.nnnorm_cfcₙ, nnnorm_sum_le, Real.toNNReal_le_ofNat, NNReal.inner_le_Lp_mul_Lq_hasSum, NNReal.rpow_add_rpow_le_add, NNReal.coe_le_one, ENNReal.lt_iff_exists_add_pos_lt, ContinuousLinearMap.opNNNorm_le_iff, NNReal.segment_eq_uIcc, nnnorm_le_add_nnnorm_add, nnnorm_le_mul_nnnorm_add, NNReal.orderIsoRpow_apply, NNReal.agmSequences_zero, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum, ContinuousLinearMap.ebound, MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure, MeasureTheory.exists_upperSemicontinuous_le_lintegral_le, NNReal.agm_lt_max_of_ne, nnnorm_le_nnnorm_add_nnnorm_sub, Real.le_toNNReal_iff_coe_le, NNReal.pi_pos, NNReal.not_summable_iff_tendsto_nat_atTop, IsUltrametricDist.nnnorm_pow_le, NNReal.sqrt_sq, EuclideanSpace.nndist_eq, NNReal.sqrt_pos, ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective, Real.nnnorm_exp_I_mul_ofReal_sub_one_le, NormedField.exists_nnnorm_lt_one, NNReal.le_sqrt_iff_sq_le, NNReal.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, NNReal.half_le_self, MeasureTheory.MemLp.meas_ge_lt_top, NNReal.agm_le_agmSequences_snd, FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius, NNReal.HolderTriple.nonneg', EMetric.exists_continuous_nnreal_forall_closedBall_subset, NNReal.sqrt_zero, WithLp.nndist_fst_le, NonUnitalStarAlgHom.nnnorm_apply_le, NNReal.young_inequality, NNReal.map_coe_atTop, ContinuousAlternatingMap.le_opNNNorm, nndist_add_add_le, Real.toNNReal_lt_toNNReal_iff_of_nonneg, NNReal.HolderTriple.left_pos, Matrix.linfty_opNNNorm_mulVec, ApproximatesLinearOn.norm_fderiv_sub_le, IsGreatest.nnnorm_cfc_nnreal, NNReal.rpow_zero_pos, NNReal.agmSequences_fst_le_agm, ENNReal.coe_mem_upperBounds, NNReal.image_coe_Ico, MeasureTheory.uniformIntegrable_iff, FormalMultilinearSeries.nnnorm_changeOrigin_le, NNReal.instPosSMulStrictMono, eq_one_or_nnnorm_pos, FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum, nnnorm_mul_le, ENNReal.image_coe_Iic, Matrix.frobenius_nnnorm_one, thickenedIndicator_le_one, ENNReal.instSMulPosMonoNNReal, BoxIntegral.Prepartition.distortion_le_of_mem, nnnorm_mul₃_le, NNReal.strictConcaveOn_sqrt, NNReal.arith_mean_le_rpow_mean, MeasureTheory.mulEquivHaarChar_pos, WithZeroMulInt.toNNReal_pos, NNReal.sqrt_le_sqrt, ENNReal.natCast_le_ofNNReal, NNReal.isGreatest_Lp, Real.one_lt_toNNReal, LinearMap.exists_antilipschitzWith, NNReal.isCoboundedUnder_le_toReal, nndist_smul_le, 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, ENNReal.iSup_coe_lt_top, Real.toNNReal_le_one, NNReal.closedBall_zero_eq_Icc, NNReal.lt_iff_exists_rat_btwn, NNReal.instCanonicallyOrderedAdd, Real.toNNReal_monotone, nndist_le_pi_nndist, nnnorm_zpow_le_mul_norm, CompactlySupportedContinuousMap.nnrealPart_add_le_add_nnrealPart, NNReal.comap_coe_atTop, MeasureTheory.ProbabilityMeasure.apply_mono, NNReal.rpow_sum_le_const_mul_sum_rpow, PiLp.nndist_apply_le, BoundedContinuousFunction.nndist_set_exists, BoundedContinuousFunction.Lp_nnnorm_le, dist_le_coe, isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le, antilipschitzWith_iff_le_mul_nndist, FormalMultilinearSeries.compAlongComposition_nnnorm, IsGreatest.nnnorm_cfc, SemilinearMapClass.nnbound_of_continuous, nndist_triangle_right, NNReal.one_le_coe, Real.toNNReal_le_toNNReal_iff, Finset.nnnorm_prod_le', NNReal.sqrt_eq_iff_eq_sq, SpectrumRestricts.nnreal_lt_iff, NNReal.HolderTriple.inv_nonneg, exists_spanning_measurableSet_le, NNReal.addLeftMono, ENNReal.le_coe_iff, ENNReal.coe_lt_coe, nnnorm_multiset_sum_le, IsGreatest.nnnorm_cfcₙ_nnreal, Matrix.l2_opNNNorm_mulVec, PiLp.nnnorm_apply_le, NNReal.map_coe_nhdsGT, MeasureTheory.SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral, Complex.antilipschitz_equivRealProd, AntilipschitzWith.le_mul_nnnorm', NNReal.bddAbove_range_agmSequences_fst, NNReal.image_coe_Iio, NNReal.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, ENNReal.toNNReal_pos, 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, NNReal.instStarOrderedRing, nnnorm_mul_le', nnnorm_pos', IsUltrametricDist.nnnorm_mul_le_max, NNReal.agmSequences_fst_lt_snd_of_ne, FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, MeasureTheory.measureUnivNNReal_pos, indicator_le_thickenedIndicator, SpectrumRestricts.nnreal_le_iff, NNReal.bot_eq_zero, NNReal.sqrt_mul, Real.ofNat_lt_toNNReal, NNReal.rpow_arith_mean_le_arith_mean_rpow, NNReal.le_add_nndist, ENNReal.le_toNNReal_of_coe_le, ContinuousLinearMap.nnnorm_holder_apply_apply_le, NNReal.instIsOrderBornology, ENNReal.toNNReal_strict_mono, tendsto_real_toNNReal_atTop, MeasureTheory.FiniteMeasure.apply_iUnion_le, NNReal.add_rpow_le_rpow_add, NNReal.sqrt_eq_zero, SemilinearMapClass.ebound_of_continuous, Real.comap_toNNReal_atTop, MeasureTheory.FiniteMeasure.apply_mono, MeasureTheory.L1.nnnorm_integral_le, NNReal.coe_lt_one, Module.Basis.exists_opNNNorm_le, MeasureTheory.ProbabilityMeasure.apply_le_one, NNReal.mul_self_sqrt, isCompact_setOf_finiteMeasure_le_of_compactSpace, ENNReal.ofNNReal_le_natCast, Real.toNNReal_pos, NNReal.strictMono_rpow_of_pos, NNReal.lt_rpow_inv_iff, NNReal.agmSequences_fst_monotone, ContinuousLinearMap.isLeast_opNNNorm, IsUltrametricDist.nnnorm_add_one_le_max_nnnorm_one, 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, NNReal.geom_mean_le_arith_mean4_weighted, NNReal.tendsto_rpow_atTop, NNReal.tsum_comp_le_tsum_of_inj, one_le_thickenedIndicator_apply', ENat.floor_coe, ENNReal.coe_le_one_iff, Delone.DeloneSet.packingRadius_pos, NNReal.HolderTriple.lt, Matrix.l2_opNNNorm_mul, nndist_vsub_vsub_le, Pi.sum_nnnorm_apply_le_nnnorm, NNReal.geom_mean_le_arith_mean2_weighted, NNReal.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, Metric.exists_continuous_nnreal_forall_closedEBall_subset, ContinuousMap.nnnorm_lt_iff_of_nonempty, 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, Real.toNNReal_add_le, NNReal.agm_eq_agm_gm_am, MeasureTheory.FiniteMeasure.mass_comap_le, AntilipschitzWith.le_mul_nndist, NNReal.rpow_lt_rpow_iff, NNReal.rpow_inv_le_iff, NNReal.isBoundedUnder_le_toReal, NNReal.continuous_sqrt, ContinuousMultilinearMap.isLeast_opNNNorm, NNReal.HolderTriple.one_div_nonneg, NNReal.image_coe_Ici, NNReal.min_le_agm, uniformity_basis_edist_nnreal_le, nndist_triangle_left, NNReal.isCoboundedUnder_ge_toReal, MeasureTheory.mul_le_addHaar_image_of_lt_det, Real.toNNReal_lt_one, nnnorm_cfcₙ_nnreal_lt_iff, ContinuousLinearMap.nonlinearRightInverseOfSurjective_def, NNReal.exists_pos_sum_of_countable, Pi.sum_nnnorm_apply_le_nnnorm', rieszContentAux_sup_le, NNReal.isOpen_Ico_zero, CStarAlgebra.mem_Icc_algebraMap_iff_nnnorm_le, MeasureTheory.L1.nnnorm_Integral_le_one, Units.nnnorm_pos, NNReal.HolderTriple.pos', ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos, NNReal.le_rpow_inv_iff, edist_lt_coe, Tactic.NormNum.isNNRat_nnrealSqrt_of_isNNRat, enorm_lt_coe, Real.toNNReal_mono, Set.InvOn.one_sub_one_add_inv, NNReal.rpow_add_rpow_le, ENNReal.iSup_coe_eq_top, BoundedContinuousFunction.nndist_coe_le_nndist, nnnorm_inner_le_nnnorm, NNReal.sqrt_eq_one, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnnorm_quasispectrum, IsometricContinuousFunctionalCalculus.nnnorm_spectrum_le, cfc_nnreal_le_iff, 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, ENNReal.toNNReal_mono, Set.OrdConnected.preimage_coe_nnreal_ennreal, WithLp.nnnorm_fst_le, MeasureTheory.nnnorm_indicatorConstLp_le, enorm_le_coe, IsUltrametricDist.nnnorm_nsmul_le, NNReal.agmSequences_monotone_and_antitone, NNReal.rpow_add_le_mul_rpow_add_rpow, rieszContentAux_mono, ENNReal.exists_pos_tsum_mul_lt_of_countable, NNReal.sum_mul_le_sqrt_mul_sqrt, NNReal.lt_inv_iff_mul_lt, Real.one_le_toNNReal, eventually_enorm_mfderiv_extChartAt_lt, MeasureTheory.addHaar_image_le_mul_of_det_lt, Polynomial.one_le_cauchyBound, MeasureTheory.ProbabilityMeasure.apply_iUnion_le, nnnorm_smul_le, NNReal.ball_zero_eq_Ico', thickenedIndicator_subset, ContinuousLinearMap.le_opNNNorm, ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos, NNReal.HolderTriple.right_pos, ENNReal.image_coe_Iio, NNReal.one_le_sqrt, NNReal.Lp_add_le_hasSum, NNReal.convex_iff, NNReal.coe_expect, nnnorm_le_nnnorm_add_nnnorm_div, nnnorm_apply_le_nnnorm_cfc, IsometricContinuousFunctionalCalculus.spectrum_le, nnnorm_pow_le', BoundedContinuousFunction.nnnorm_coe_le_nnnorm, dist_lt_coe, nndist_nnnorm_nnnorm_le', NNReal.half_lt_self, NNReal.inner_le_weight_mul_Lp, NNReal.le_toNNReal_of_coe_le, BoundedContinuousFunction.nnnorm_le, ProbabilityTheory.HasSubgaussianMGF.add, NNReal.iInf_real_pos_eq_iInf_nnreal_pos, MeasureTheory.SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge, edist_le_coe, NNReal.geom_mean_le_arith_mean_weighted, Set.OrdConnected.image_real_toNNReal, NNReal.le_inv_iff_mul_le, AntilipschitzWith.le_mul_nnnorm, nndist_midpoint_midpoint_le, NNReal.image_coe_Iic, MeasureTheory.ProbabilityMeasure.apply_union_le, BoundedContinuousFunction.nnnorm_const_le, nnnorm_tsum_le, NNReal.orderIsoIccZeroCoe_symm_apply_coe, ContinuousAlternatingMap.isLeast_opNNNorm, apply_le_nnnorm_cfc_nnreal, setOf_riemannianEDist_lt_subset_nhds, eventually_riemannianEDist_le_edist_extChartAt, NNReal.coe_mono, WithLp.nnnorm_snd_le, Valuation.RankOne.strictMono', LipschitzWith.nnorm_le_mul', Valued.integer.exists_nnnorm_lt_one, BoxIntegral.Prepartition.distortion_le_iff, NNReal.instOrderTopology, NNReal.agmSequences_fst_le_snd, ContinuousLinearMap.nndist_le_opNNNorm, Real.toNNReal_le_toNNReal_iff_of_pos, Matrix.linfty_opNNNorm_mul, NNReal.instIsOrderedRing, thickenedIndicator_mono_infEdist, NNReal.image_coe_Ioi, NNReal.nhds_zero, Real.natCastle_toNNReal', NNReal.monotone_nnrpow_const, LipschitzWith.nndist_le, ContinuousLinearMap.opNNNorm_comp_le, NNReal.rpow_add_le_add_rpow, PreTilt.valAux_add, MemHolder.nnHolderNorm_add_le, Metric.isBounded_iff_nndist, convex_setOf_holderWith, NNReal.orderIsoRpow_symm_eq, ENNReal.toNNReal_lt_toNNReal, NNReal.Lp_add_le_tsum', MeasureTheory.Measure.exists_positive_of_not_mutuallySingular, NonUnitalIsometricContinuousFunctionalCalculus.quasispectrum_le, NNReal.bddAbove_natCast_image_iff, NNReal.addLeftReflectLT, NNReal.HolderTriple.inv_pos', MeasureTheory.Content.mono', ContinuousMultilinearMap.opNNNorm_le_iff, NNReal.image_coe_Ioo, nnnorm_multiset_prod_le, NNReal.HolderTriple.pos, NNReal.rpow_inv_lt_iff, NNReal.inv_le, ENNReal.orderIsoIicCoe_apply_coe, nnnorm_commutator_sub_one_le, CFC.sqrt_eq_cfc, NNReal.coe_lt_coe, ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le, nnnorm_cfcₙ_le_iff, IsUltrametricDist.nnnorm_intCast_le_one, MeasureTheory.Measure.modularCharacterFun_pos, NNReal.rpow_arith_mean_le_arith_mean2_rpow, NNReal.monotone_rpow_of_nonneg, IsUltrametricDist.nnnorm_tprod_le, ContinuousLinearMap.opNNNorm_le_of_lipschitz, Int.abs_le_floor_nnreal_iff, Metric.boundedSpace_iff_nndist, MeasureTheory.eLpNormEssSup_lt_top_iff_isBoundedUnder, Finset.nnnorm_sum_le_sup_nnnorm, MeasureTheory.UniformIntegrable.spec, HasOuterApproxClosed.indicator_le_apprSeq, NNReal.sqrt_one, NNReal.inner_le_Lp_mul_Lq_tsum', ENNReal.coe_le_iff, NNReal.Lp_add_le, nnnorm_commutator_units_sub_one_le, CFC.sqrt_algebraMap, NNReal.coe_pos, ENNReal.one_lt_coe_iff, NNReal.HolderTriple.inv_pos, 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, NNReal.sqrt_le_one, HolderWith.nnholderNorm_le, ENNReal.image_coe_Ici, NNReal.ball_zero_eq_Ico, ENNReal.coe_strictMono, Real.toNNReal_le_iff_le_coe, ModP.v_p_lt_val, ENNReal.image_coe_Ioi, MeasureTheory.SimpleFunc.exists_upperSemicontinuous_le_lintegral_le, Real.nnreal_trichotomy, IsUltrametricDist.nnnorm_zpow_le, NNReal.instIsStrictOrderedRing, ENNReal.toNNReal_lt_of_lt_coe, nnnorm_le_nnnorm_add_nnnorm_sub', Real.toNNReal_lt_natCast, NNReal.geom_mean_le_arith_mean3_weighted, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, NNReal.HolderTriple.inv_nonneg', NNReal.agmSequences_snd_antitone, spectrum.le_nnnorm_of_mem, NNReal.instMulArchimedean, NNReal.summable_iff_not_tendsto_nat_atTop, NormedField.denselyOrdered_range_nnnorm, NNReal.instArchimedean, ENNReal.natCast_lt_coe, BoxIntegral.TaggedPrepartition.distortion_le_iff, Real.nnabs_pos, MeasureTheory.Measure.addModularCharacterFun_pos, CStarAlgebra.inr_mem_Icc_iff_nnnorm_le, convex_setOf_holderOnWith, NNReal.HolderTriple.one_div_pos, NNReal.sqrt_div, Matrix.nnnorm_le_iff, NNReal.tendsto_coe_atTop, ENNReal.image_coe_Ioo, ContinuousLinearEquiv.nnnorm_symm_pos, Finset.nnnorm_prod_le_sup_nnnorm, pi_nnnorm_const_le, Finset.nnnorm_prod_le, NNReal.instIsStrictOrderedModule, EuclideanSpace.nnnorm_eq, NNReal.nhds_zero_basis, IsUnifLocDoublingMeasure.one_le_scalingConstantOf, HolderOnWith.nndist_le, MeasureTheory.exists_upperSemicontinuous_le_integral_le, ContinuousLinearMap.nnbound, NNReal.agmSequences_succ', uniformity_basis_edist_nnreal, NNReal.one_lt_coe, nndist_nnnorm_nnnorm_le, MeasureTheory.Measure.toSphereBallBound_pos, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id_le, CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_le, NNReal.closedBall_zero_eq_Icc', Real.coe_sqrt, ENNReal.one_le_coe_iff, ContinuousAlternatingMap.opNNNorm_le_iff, Real.tendsto_toNNReal_atTop, NNReal.instDenselyOrdered, NNReal.inner_le_Lp_mul_Lq_tsum, NNReal.instSMulPosStrictMono, nnnorm_prod_le, MeasureTheory.exists_eLpNorm_indicator_le, ENat.ceil_coe, NNReal.sum_sqrt_mul_sqrt_le, NNReal.mulLeftMono, ModP.preVal_add, NNReal.HolderConjugate.sub_one_pos, CompactlySupportedContinuousMap.monotone_of_nnreal, TensorProduct.nndist_tmul_le, lipschitzExtensionConstant_pos, NNReal.sqrt_mul_le_half_add, Real.map_toNNReal_atTop, Real.lt_toNNReal_iff_coe_lt, MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz_estimate, MeasureTheory.Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure, ENNReal.image_coe_Ico, NumberField.mixedEmbedding.one_le_convexBodyLT'Factor, ENNReal.image_coe_Icc, SpectrumRestricts.lt_nnreal_iff, NNReal.rpow_le_rpow_iff, nnnorm_sub_le, NNReal.HolderTriple.nonneg, ContinuousMultilinearMap.le_opNNNorm, ENNReal.coe_lt_one_iff, MeasureTheory.distribHaarChar_pos, Real.ofNat_le_toNNReal, NNReal.image_coe_Icc, BoxIntegral.IntegrationParams.MemBaseSet.exists_common_compl, LinearMap.injective_iff_antilipschitz, ENNReal.instPosSMulStrictMonoNNReal, apply_le_nnnorm_cfcₙ_nnreal, ENNReal.tendsto_coe_nhds_top, NNReal.HolderTriple.inv_lt_inv, nndist_vadd_vadd_le, nnnorm_add_le, NNReal.coe_le_coe, NNReal.holderConjugate_iff, ENNReal.toNNReal_pos_iff, NNReal.sqrt_mul_self, NNReal.strictConcaveOn_rpow, one_le_thickenedIndicator_apply, nnnorm_le_add_nnnorm_add', NNReal.Lp_add_le_tsum, NNReal.inv_lt_one_iff, HasOuterApproxClosed.apprSeq_apply_le_one, NNReal.sqrt_inv, one_le_nnnorm_one, MeasureTheory.FiniteMeasure.apply_union_le, IsometricContinuousFunctionalCalculus.isGreatest_spectrum, NNReal.dist_gm_am_le, coe_le_enorm, IsUltrametricDist.nnnorm_add_le_max, HasOuterApproxClosed.exAppr, CStarAlgebra.nnnorm_le_natCast_iff_of_nonneg, NNReal.agm_lt_agmSequences_snd_of_ne, EMetric.exists_pos_forall_lt_edist, NNReal.bddAbove_coe, nnnorm_pos, NormedField.exists_lt_nnnorm, Real.toNNReal_lt_toNNReal_iff', HolderWith.nndist_le, NNReal.agmSequences_succ, nnnorm_zsmul_le, NNReal.young_inequality_real, Tactic.NormNum.isNat_nnrealSqrt, BoundedContinuousFunction.apply_le_nndist_zero, BoundedContinuousFunction.nndist_le_two_nnnorm, BoundedContinuousFunction.NNReal.upper_bound, CStarAlgebra.le_nnnorm_of_mem_quasispectrum, NNReal.map_coe_nhdsGE, NNReal.sqrt_lt_sqrt, PiLp.nndist_eq_of_L2, IsUltrametricDist.nnnorm_zsmul_le, NNReal.inner_le_Lp_mul_Lq, NonUnitalIsometricContinuousFunctionalCalculus.nnnorm_quasispectrum_le, Polynomial.card_mahlerMeasure_le_prod, Real.natCast_le_toNNReal, Metric.exists_pos_forall_lt_edist, WithLp.nndist_snd_le, Polynomial.IsRoot.norm_lt_cauchyBound, nnnorm_le_pi_nnnorm', NNReal.bddAbove_range_natCast_iff, nnnorm_div_le, NNReal.sq_sqrt, NNReal.tendsto_pow_atTop_nhds_zero_iff, IsUltrametricDist.nnnorm_tsum_le, MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite, NNReal.agm_le_max, NNReal.HolderTriple.one_div_pos', MeasureTheory.Content.sup_le', LipschitzWith.nnorm_le_mul, NNReal.Icc_subset_segment, Real.natCast_lt_toNNReal, NNReal.holderTriple_iff, FormalMultilinearSeries.comp_summable_nnreal, NNReal.concaveOn_rpow, Delone.DeloneSet.coveringRadius_pos, ENNReal.image_coe_Ioc, thickenedIndicator_mono, NNReal.instOrderedSub, IsCoercive.antilipschitz
bridge: BoxIntegral.IntegrationParams.MemBaseSet.exists_compl, BoxIntegral.IntegrationParams.MemBaseSet.distortion_le
|
instReprNNReal 📖 | CompOp | — |
instSemilatticeInfNNReal 📖 | CompOp | — |
instSemilatticeSupNNReal 📖 | CompOp | 24 mathmath: Seminorm.finset_sup_apply, Pi.norm_def', BoxIntegral.Prepartition.distortion_biUnionTagged, NNReal.mul_finset_sup, Pi.nnnorm_def', NumberField.canonicalEmbedding.nnnorm_eq, ENNReal.coe_finset_sup, Pi.norm_def, 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, NNReal.finset_sup_mul, Finset.nnnorm_prod_le_sup_nnnorm, Matrix.linfty_opNNNorm_def, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, Matrix.linfty_opNorm_def, NumberField.house_eq_sup', Matrix.norm_eq_sup_sup_nnnorm, NNReal.finset_sup_div
|
instSemiringNNReal 📖 | CompOp | 679 mathmath: Delone.DeloneSet.mapBilipschitz_coveringRadius, NNReal.HolderConjugate.mul_eq_add, PiLp.lipschitzWith_toLp, Seminorm.isBounded_const, PiLp.norm_toLp_const', NNReal.summable_coe, PiLp.nndist_eq_sum, Matrix.frobenius_nnnorm_mul, NNReal.rpow_sub_intCast, ProbabilityTheory.gaussianReal_map_const_mul, List.nnnorm_prod, Real.toNNReal_lt_natCast', ENNReal.toNNReal_pow, NNReal.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', NNReal.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, NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, AntilipschitzWith.mul_le_nndist, Real.toNNReal_mul, NNReal.pow_antitone_exp, setIntegral_withDensity_eq_setIntegral_smul₀, MeasureTheory.addHaarScalarFactor_smul_inv_eq_distribHaarChar, NNReal.coe_toRealHom, PiLp.norm_toLp_one, HolderWith.of_le, HasSum.toNNReal, ENNReal.ofNNReal_natCast_sub, Complex.nndist_self_conj, List.nnnorm_prod_le', nnnorm_nsmul_le, NNReal.sqrt_le_iff_le_sq, HolderOnWith.comp, NumberField.FinitePlace.norm_def', ENNReal.coe_finset_sum, ProbabilityTheory.HasSubgaussianMGF.sum_of_iIndepFun, NNReal.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, ENNReal.summable_toNNReal_of_tsum_ne_top, ENNReal.smul_def, CFC.abs_nnrpow_two, instStarModuleNNRealOfReal, NNReal.rpow_add_rpow_le_add, FormalMultilinearSeries.changeOriginSeries_summable_aux₃, ContinuousLinearMap.opNNNorm_le_iff, MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar_inv, NNReal.segment_eq_uIcc, NNReal.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, NNReal.summable_sigma, WithLp.prod_nnnorm_eq_add, nndist_smul₀, NNReal.agmSequences_zero, NNReal.rpow_natCast, nnnorm_le_nnnorm_add_nnnorm_sub, NNReal.coe_add, Real.toNNReal_pow, NNReal.not_summable_iff_tendsto_nat_atTop, NNReal.sqrt_sq, EuclideanSpace.nndist_eq, HolderWith.add, NNReal.summable_geometric, ProbabilityTheory.HasSubgaussianMGF.const_mul, NumberField.mixedEmbedding.convexBodyLT_volume, instStarModuleNNRealReal, NNReal.le_sqrt_iff_sq_le, nnnorm_le_insert, PiLp.nnnorm_eq_of_L2, NNReal.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, 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, NNReal.tsum_mul_right, Dilation.ratio_mul, MeasureTheory.FiniteMeasure.testAgainstNN_eq_mass_mul, ProbabilityTheory.Kernel.HasSubgaussianMGF.add_comp, NNReal.natCast_iInf, HolderOnWith.nndist_le_of_le, NNReal.rpow_add_intCast', FormalMultilinearSeries.nnnorm_changeOrigin_le, NNReal.instPosSMulStrictMono, NNReal.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, NNReal.isSquare, MeasureTheory.FiniteMeasure.mass_prod, PiLp.nnnorm_toLp_one, MeasureTheory.FiniteMeasure.testAgainstNN_const, MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto, nnnorm_mul₃_le, rieszContentAux_image_nonempty, MeasureTheory.FiniteMeasure.normalize_eq_of_nonzero, LipschitzWith.mul_end, Real.toNNReal_sum_of_nonneg, NNReal.strictConcaveOn_sqrt, WithZeroMulInt.toNNReal_pos, ContinuousMap.toNNReal_algebraMap, InnerProductSpace.nnnorm_rankOne, ENNReal.natCast_le_ofNNReal, MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar, Seminorm.ball_smul, NNReal.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₀, NNReal.natCast_natAbs, nnnorm_smul, List.nnnorm_prod_le, CompactlySupportedContinuousMap.coe_toRealLinearMap, nnnorm_le_mul_nnnorm_add', NNReal.HolderConjugate.inv_add_inv_eq_one, ENNReal.toNNReal_add, BoxIntegral.Box.nndist_le_distortion_mul, NNReal.rpow_sub_natCast, Hamming.nnnorm_eq_hammingNorm, StarAlgHom.realContinuousMapOfNNReal_apply, NNReal.hasLipschitzAdd, MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalize, MeasureTheory.FiniteMeasure.self_eq_mass_mul_normalize, NNReal.instCanonicallyOrderedAdd, Real.toNNReal_ofNat, Real.nnabs_of_nonneg, WithZeroMulInt.toNNReal_lt_one_iff, Dilation.nndist_eq, nnnorm_zpow_le_mul_norm, LipschitzWith.pow_end, CompactlySupportedContinuousMap.nnrealPart_add_le_add_nnrealPart, NNReal.rpow_sum_le_const_mul_sum_rpow, PseudoMetricSpace.dist_ofPreNNDist, MeasureTheory.distribHaarChar_apply, MeasureTheory.Content.sup_disjoint', BoundedContinuousFunction.Lp_nnnorm_le, NNReal.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', selfAdjoint.nnnorm_pow_two_pow, ModP.preVal_mul, SemilinearMapClass.nnbound_of_continuous, NNReal.rpow_add_natCast', Metric.IsCover.image_lipschitz_of_surjective, setIntegral_withDensity_eq_setIntegral_smul₀', nndist_triangle_right, Dilation.ratioHom_apply, NNReal.sqrt_eq_iff_eq_sq, exists_spanning_measurableSet_le, NNReal.addLeftMono, LipschitzWith.list_prod, ProbabilityTheory.gaussianReal_map_linearMap, nnnorm_multiset_sum_le, Seminorm.comp_smul, CompactlySupportedContinuousMap.toRealLinearMap_apply, Matrix.l2_opNNNorm_mulVec, LipschitzWith.comp_lipschitzOnWith, Complex.antilipschitz_equivRealProd, TensorProduct.nnnorm_tmul, AntilipschitzWith.le_mul_nnnorm', NNReal.smulCommClass_left, CFC.posPart_smul, FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le, nnnorm_algebraMap, nnnorm_pow, Real.coe_nnabs, NNReal.agm_mul_distrib, MeasureTheory.integrable_withDensity_iff_integrable_smul₀, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le, Seminorm.bound_of_continuous, nnnorm_pow_le, Real.toNNReal_le_natCast, WithZeroMulInt.toNNReal_neg_apply, CompactlySupportedContinuousMap.toRealPositiveLinear_apply, NNReal.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, NNReal.lipschitzWith_sub, NNReal.instIsTopologicalSemiring, CFC.sqrt_eq_nnrpow, lipschitzWith_circleMap, IsSelfAdjoint.nnnorm_mul_self, FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal, NNReal.rpow_ofNat, NNReal.sqrt_mul, MeasureTheory.Measure.modularCharacterFun_map_mul, MeasureTheory.Measure.toSignedMeasure_smul, NNReal.HolderConjugate.two_two, CFC.abs_nnrpow_two_mul, NNReal.iSup_pow_of_ne_zero, NNReal.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, NNReal.add_rpow_le_rpow_add, NNReal.rpow_two, WithZeroMulInt.toNNReal_le_one_iff, nndist_midpoint_left, MeasureTheory.FiniteMeasure.instContinuousSMulNNReal, Module.Basis.exists_opNNNorm_le, PreTilt.valAux_mul, NNReal.mul_self_sqrt, 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', NNReal.rpow_natCast_mul, NNReal.exists_pow_lt_of_lt_one, NNReal.mul_finset_sup, ProbabilityTheory.gaussianReal_mul_const, Dilation.ratio_pow, nndist_center_homothety, LipschitzWith.vadd, ENat.floor_coe, Real.toNNReal_eq_natCast, NNReal.summable_nat_add_iff, NNReal.rpow_add_natCast, Matrix.l2_opNNNorm_mul, nndist_vsub_vsub_le, NNReal.coe_natCast, Pi.sum_nnnorm_apply_le_nnnorm, NNReal.coe_tsum_of_nonneg, NNReal.mul_sup, MeasureTheory.Measure.addModularCharacterFun_map_add, WithLp.prod_nndist_eq_add, NNReal.coe_sum, Real.nnnorm_mul_toNNReal, ENNReal.coe_two, nnnorm_prod_le_of_le, NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, ValuativeRel.RankLeOneStruct.strictMono, CompactlySupportedContinuousMap.integralLinearMap_apply, nndist_mul_mul_le, nndist_triangle, Real.toNNReal_add_le, NNReal.agm_eq_agm_gm_am, AntilipschitzWith.le_mul_nndist, NNReal.tendsto_sum_nat_add, ENNReal.toNNReal_natCast, MeasureTheory.memL1_smul_of_L1_withDensity, NNReal.list_prod_map_rpow', NNReal.le_gm_and_am_le, Real.nnnorm_two, Real.toNNReal_mul_nnnorm, LipschitzWith.uncurry, Mathlib.Meta.NormNum.IsNat.nnreal_rpow_eq_nnreal_pow, CFC.nnrpow_sqrt, nndist_lineMap_right, WithLp.prod_lipschitzWith_toLp, nndist_triangle_left, NNReal.rpow_add', MeasureTheory.FiniteMeasure.smul_testAgainstNN_apply, NNReal.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, NNReal.rpow_add, NNReal.hasSum_geometric, Valued.norm_def, Seminorm.closedBall_smul, ENNReal.smulCommClass_left, NumberField.FinitePlace.norm_def_int, NNReal.coe_two, NNReal.coe_nsmul, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply, MeasureTheory.mulEquivHaarChar_trans, Set.InvOn.one_sub_one_add_inv, NNReal.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, NNReal.natCast_iSup, ContinuousMap.toNNReal_mul_add_neg_mul_add_mul_neg_eq, ENNReal.coe_mul, LipschitzWith.sub, NNReal.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, NNReal.smul_def, MeasureTheory.nnnorm_indicatorConstLp_le, ProbabilityTheory.HasSubgaussianMGF.sub_of_indepFun, NNReal.rpow_add_le_mul_rpow_add_rpow, NNReal.sum_mul_le_sqrt_mul_sqrt, NNReal.smulCommClass_right, NNReal.lt_inv_iff_mul_lt, NNReal.rpow_add_intCast, LipschitzOnWith.add, CFC.nnrpow_nnrpow, MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN, NNRealRMK.le_rieszMeasure_of_isCompact_tsupport_subset, nnnorm_smul_le, Real.nndist_eq, CompactlySupportedContinuousMap.toReal_add, NumberField.mixedEmbedding.convexBodyLT'_volume, NNReal.tsum_eq_toNNReal_tsum, ContinuousLinearMap.le_opNNNorm, Metric.coveringNumber_subset_le, ENNReal.ofNNReal_sub_natCast, NNReal.convex_iff, ProbabilityTheory.gaussianPDFReal_inv_mul, NNReal.coe_expect, nnnorm_le_nnnorm_add_nnnorm_div, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul, NNReal.rpow_add_one, setIntegral_withDensity_eq_setIntegral_smul, NNReal.HolderTriple.inv_add_inv_eq_inv, nnnorm_pow_le', ContinuousMapZero.toNNReal_add_add_neg_add_neg_eq, NNReal.half_lt_self, FormalMultilinearSeries.changeOriginSeries_summable_aux₁, NNReal.inner_le_weight_mul_Lp, NNReal.rpow_add_one', ProbabilityTheory.HasSubgaussianMGF.add, ProbabilityTheory.measure_sum_ge_le_of_hasCondSubgaussianMGF, MeasureTheory.Measure.mul_addHaarScalarFactor_smul, CompactlySupportedContinuousMap.toNNRealLinear_apply, NNReal.le_inv_iff_mul_le, AntilipschitzWith.le_mul_nnnorm, nndist_midpoint_midpoint_le, Delone.DeloneSet.mapBilipschitz_trans, MeasureTheory.ProbabilityMeasure.apply_union_le, MemHolder.nnHolderNorm_nsmul, PiLp.norm_toLp_const, nnnorm_fderiv_norm_rpow_le, HasStrictFDerivAt.approximates_deriv_on_open_nhds, TrivSqZeroExt.nnnorm_def, similar_iff_exists_pairwise_nndist_eq, NNReal.mul_eq_mul_left, ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm, NNReal.HolderTriple.one_div_eq, NNReal.segment_eq_Icc, Valuation.RankOne.strictMono', NNReal.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, NNReal.instIsOrderedRing, Real.toNNReal_add_toNNReal, AntilipschitzWith.comp, Real.nnabs_coe, MemHolder.nnHolderNorm_smul, CFC.nnrpow_three, LipschitzWith.mul, MeasureTheory.JordanDecomposition.toSignedMeasure_smul, StarAlgHom.realContinuousMapOfNNReal_injective, Real.natCastle_toNNReal', SeminormedAddCommGroup.lipschitzWith_sub, RCLike.nnnorm_two, NNReal.summable_one_div_rpow, LipschitzWith.nndist_le, WithZeroMulInt.toNNReal_eq_one_iff, ContinuousLinearMap.opNNNorm_comp_le, NNReal.rpow_add_le_add_rpow, FormalMultilinearSeries.changeOriginSeries_summable_aux₂, MemHolder.nnHolderNorm_add_le, NNReal.mul_lt_of_lt_div, convex_setOf_holderWith, NNReal.coe_pow, Dilation.ratio_comp, exists_lt_rieszContentAux_add_pos, ProbabilityTheory.HasSubgaussianMGF.add_of_hasCondSubgaussianMGF, MeasureTheory.FiniteMeasure.normalize_testAgainstNN, NNReal.rpow_sub_natCast', HolderOnWith.comp_holderWith, Real.toNNReal_abs, ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun, PiLp.nnnorm_eq_of_L1, MeasureTheory.withDensitySMulLI_apply, MeasureTheory.Measure.addHaar_nnreal_smul, NNReal.bddAbove_natCast_image_iff, NNReal.addLeftReflectLT, NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one, ContinuousLinearMap.nnnorm_smulRight_apply, ContinuousMultilinearMap.opNNNorm_le_iff, MeasureTheory.FiniteMeasure.map_smul, nnnorm_multiset_prod_le, NNReal.inv_le, Seminorm.finset_sup_smul, LipschitzWith.comp, nnnorm_commutator_sub_one_le, Seminorm.isBounded_sup, ENNReal.coe_pow, NNReal.sup_mul, NNReal.summable_rpow_inv, WithZeroMulInt.toNNReal_strictMono, instTrivialStarNNReal, CompactlySupportedContinuousMap.toReal_smul, norm_cfcₙ_one_sub_one_add_inv_lt_one, MeasureTheory.FiniteMeasure.prod_prod, MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous, FormalMultilinearSeries.summable_nnnorm_mul_pow, Int.abs_le_floor_nnreal_iff, nnnormHom_apply, MeasureTheory.distribHaarChar_eq_div, nndist_lineMap_lineMap, CFC.sqrt_nnrpow_two, Real.toNNReal_coe_nat, Int.nnnorm_natCast, NNReal.coe_multiset_sum, NNReal.mul_iSup, NNReal.Lp_add_le, CFC.sqrt_nnrpow, Metric.lipschitz_infDist, nnnorm_commutator_units_sub_one_le, Dilation.ratio_comp', NNReal.rpow_one_add', MeasureTheory.distribHaarChar_mul, NNReal.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, HolderOnWith.of_le, NumberField.toNNReal_valued_eq_adicAbv, MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous, nnnorm_sum_le_of_le, nnnorm_sub_mul_le, WithZeroMulInt.toNNReal_pos_apply, NNReal.mk_natCast, NNReal.finset_sup_mul, NNReal.mul_iInf, NNReal.instIsStrictOrderedRing, NNReal.coe_mul, NNReal.summable_schlomilch_iff, ENNReal.toNNReal_mul, CompactlySupportedContinuousMap.nnrealPart_smul_pos, nnnorm_le_nnnorm_add_nnnorm_sub', NNReal.iInf_mul, Real.toNNReal_lt_natCast, Int.toNat_add_toNat_neg_eq_nnnorm, NNReal.summable_iff_not_tendsto_nat_atTop, signedDist_eq_dist_iff_vsub_mem_span, NNReal.instArchimedean, NNReal.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, LinearMap.mem_span_iff_bound, ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero, ENNReal.coe_nsmul, NNReal.tsum_mul_left, ENNReal.toNNReal_sum, NNReal.instIsStrictOrderedModule, EuclideanSpace.nnnorm_eq, RCLike.nnnorm_natCast, MeasureTheory.Measure.mul_haarScalarFactor_smul, ContinuousMapZero.toNNReal_neg_smul, HolderOnWith.nndist_le, LipschitzOnWith.comp, CStarRing.nnnorm_self_mul_star, ContinuousLinearMap.nnbound, Polynomial.cauchyBound_X_sub_C, NNReal.rpow_mul_natCast, NNReal.agmSequences_succ', Module.Basis.opNNNorm_le, NNReal.hasSum_coe, NNReal.hasSum_nat_add_iff, ContinuousAlternatingMap.opNNNorm_le_iff, ContinuousMultilinearMap.nnnorm_smulRight, ENNReal.hasSum_coe, MeasureTheory.addEquivAddHaarChar_trans, NNReal.instSMulPosStrictMono, AEMeasurable.nnreal_tsum, nnnorm_prod_le, NNReal.tendsto_tsum_compl_atTop_zero, NNReal.summable_condensed_iff, NNReal.rpow_inv_natCast_pow, ENat.ceil_coe, NNReal.sum_sqrt_mul_sqrt_le, NNReal.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, NNReal.coe_tsum, NNReal.coe_list_sum, NNReal.sqrt_mul_le_half_add, NNReal.rpow_add_of_nonneg, Unitization.lipschitzWith_addEquiv, MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz_estimate, RCLike.nnnorm_nsmul, ProbabilityTheory.HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF, NNReal.rpow_of_add_eq, Matrix.linfty_opNNNorm_replicateRow, MeasureTheory.Measure.haarScalarFactor_eq_mul, Valuation.RankOne.hom_eq_zero_iff, integral_withDensity_eq_integral_smul₀, NNReal.HolderConjugate.sub_one_mul_conj, NNReal.list_prod_map_rpow, HolderWith.smul, MeasureTheory.FiniteMeasure.map_snd_prod, nndist_right_midpoint, PiLp.nnnorm_toLp_const, exists_continuous_add_one_of_isCompact_nnreal, 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, Real.nndist_eq', nnnorm_mul_le_of_le, NNReal.iSup_mul, MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN, nndist_vadd_vadd_le, nnnorm_add_le, NNReal.holderConjugate_iff, NNReal.sqrt_mul_self, LipschitzOnWith.div, NNReal.strictConcaveOn_rpow, WithLp.unitization_nnnorm_def, nnnorm_le_add_nnnorm_add', ProbabilityTheory.Kernel.integral_withDensity, NNReal.instNoZeroDivisors, NNReal.iSup_pow, ENNReal.ofNNReal_natCast_add, nndist_self_homothety, MeasureTheory.FiniteMeasure.apply_union_le, Metric.IsCover.image_lipschitz, NNReal.dist_gm_am_le, Matrix.linfty_opNNNorm_def, NNReal.coe_list_prod, CStarRing.nnnorm_star_mul_self, CStarAlgebra.nnnorm_le_natCast_iff_of_nonneg, tsum_geometric_nnreal, HolderWith.nndist_le, NNReal.agmSequences_succ, Measurable.nnreal_tsum, LipschitzWith.div, nnnorm_zsmul_le, nndist_homothety_self, NNReal.young_inequality_real, LipschitzOnWith.mul, 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, NNReal.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, NNReal.instIsScalarTowerOfReal, MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto, Similar.exists_pairwise_nndist_eq, NNReal.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, NNReal.bddAbove_range_natCast_iff, nnnorm_div_le, ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc, nndist_lineMap_left, NNReal.sq_sqrt, NNReal.tendsto_pow_atTop_nhds_zero_iff, NNReal.summable_rpow, IsSelfAdjoint.nnnorm_pow_two_pow, CFC.nnrpow_two, ContinuousAlternatingMap.le_of_opNNNorm_le, MeasureTheory.Content.sup_le', LipschitzWith.nnorm_le_mul, NNReal.Icc_subset_segment, Real.natCast_lt_toNNReal, NNReal.holderTriple_iff, PiLp.nndist_eq_of_L1, FormalMultilinearSeries.comp_summable_nnreal, LipschitzWith.dist, NNReal.concaveOn_rpow, WithLp.prod_antilipschitzWith_ofLp, rieszContentAux_le, HolderWith.nndist_le_of_le, NNReal.instOrderedSub, ContinuousMap.exists_mul_le_one_eqOn_ge, CFC.nnrpow_add, NNReal.instContinuousStar
|
instZeroNNReal 📖 | CompOp | 276 mathmath: NNReal.HolderTriple.one_div_nonneg', eq_zero_or_nnnorm_pos, Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure, ENNReal.toNNReal_top_mul, ENNReal.toNNReal_eq_zero_iff, ENNReal.toNNReal_top, ENNReal.exists_nnreal_pos_mul_lt, NNReal.coe_indicator, NNReal.iSup_of_not_bddAbove, isCompact_setOf_finiteMeasure_le_of_isCompact, MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply, nndist_self, NNReal.zero_rpow, setOf_riemmanianEDist_lt_subset_nhds, 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, NNReal.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, NNReal.tendsto_atTop_zero_of_summable, ProbabilityTheory.gaussianReal_zero_var, NNReal.pi_pos, NNReal.sqrt_pos, ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective, NormedField.exists_nnnorm_lt_one, Metric.exists_continuous_nnreal_forall_closedBall_subset, NNReal.isBoundedSMul, ENNReal.toNNReal_mul_top, FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius, NNReal.HolderTriple.nonneg', EMetric.exists_continuous_nnreal_forall_closedBall_subset, NNReal.sqrt_zero, MeasureTheory.Lp.nnnorm_eq_zero_iff, NNReal.HolderTriple.left_pos, NNReal.rpow_zero_pos, NNReal.iSup_eq_zero, NNReal.instPosSMulStrictMono, NNRealRMK.lintegral_rieszMeasure, thickenedIndicator_zero, MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN, HolderWith.holderWith_zero_of_bounded, eq_one_or_nnnorm_pos, HasOuterApproxClosed.tendsto_apprSeq, CompactlySupportedContinuousMap.toRealLinearMap_apply_apply, ENNReal.zero_eq_coe, MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto, rieszContentAux_image_nonempty, NNReal.coe_eq_zero, MeasureTheory.mulEquivHaarChar_pos, WithZeroMulInt.toNNReal_pos, LinearMap.exists_antilipschitzWith, CompactlySupportedContinuousMap.coe_toRealLinearMap, MeasureTheory.condExpIndSMul_empty, unitInterval.toNNReal_zero, NNReal.closedBall_zero_eq_Icc, indiscreteTopology_iff_forall_nnnorm_eq_zero, CompactlySupportedContinuousMap.nnrealPart_add_le_add_nnrealPart, holderWith_zero_iff, SemilinearMapClass.nnbound_of_continuous, NNReal.HolderTriple.inv_nonneg, NNReal.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, NNReal.sSup_of_not_bddAbove, nnnorm_pos', nnHolderNorm_const, CompactlySupportedContinuousMap.toReal_apply, MeasureTheory.measureUnivNNReal_pos, indicator_le_thickenedIndicator, NNReal.tsum_eq_add_tsum_ite, NNReal.bot_eq_zero, NNReal.sqrt_eq_zero, SemilinearMapClass.ebound_of_continuous, ProbabilityTheory.HasCondSubgaussianMGF.zero, Module.Basis.exists_opNNNorm_le, Real.toNNReal_pos, Probability.cauchyPDF_scale_zero, ENNReal.coe_eq_zero, nnnorm_eq_zero', MeasureTheory.FiniteMeasure.restrict_eq_zero_iff, Probability.cauchyPDFReal_scale_zero, Delone.DeloneSet.packingRadius_pos, NNReal.instContinuousInv₀, Metric.exists_continuous_nnreal_forall_closedEBall_subset, Dilation.ratio_pos, CompactlySupportedContinuousMap.integralLinearMap_apply, NNReal.tendsto_sum_nat_add, nnnorm_indicator_eq_indicator_nnnorm, ProbabilityTheory.gaussianPDF_zero_var, CFC.nnrpow_zero, NNReal.HolderTriple.one_div_nonneg, MeasureTheory.FiniteMeasure.testAgainstNN_zero, thickenedIndicator_tendsto_indicator_closure, NNReal.rpow_eq_zero, uniformity_basis_edist_nnreal_le, MeasureTheory.mul_le_addHaar_image_of_lt_det, ContinuousLinearMap.nonlinearRightInverseOfSurjective_def, NNReal.exists_pos_sum_of_countable, HolderOnWith.holderOnWith_zero_of_bounded, Real.toNNReal_eq_zero, NNReal.isOpen_Ico_zero, Probability.cauchyMeasure_zero_scale, Units.nnnorm_pos, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply, NNReal.HolderTriple.pos', ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_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, MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply, ENNReal.exists_pos_tsum_mul_lt_of_countable, MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN, CompletelyRegularSpace.exists_BCNN, eventually_enorm_mfderiv_extChartAt_lt, MeasureTheory.addHaar_image_le_mul_of_det_lt, Real.toNNReal_of_nonpos, CompactlySupportedContinuousMap.toReal_add, NNReal.ball_zero_eq_Ico', ProbabilityTheory.Kernel.HasSubgaussianMGF.zero, ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos, NNReal.HolderTriple.right_pos, hasConstantSpeedOnWith_zero_iff, ContinuousMapZero.toNNReal_add_add_neg_add_neg_eq, nnnorm_eq_zero, NNReal.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, MeasureTheory.FiniteMeasure.zero_mass, NNReal.nhds_zero, LipschitzOnWith.zero_iff, ModP.preVal_zero, MeasureTheory.tendstoInMeasure_iff_tendsto_toNNReal, ProbabilityTheory.HasCondSubgaussianMGF.fun_zero, nnnorm_one', NNReal.limsSup_of_not_isBounded, MeasureTheory.Measure.exists_positive_of_not_mutuallySingular, NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one, NNReal.HolderTriple.inv_pos', NNReal.indicator_summable, NNReal.HolderTriple.pos, NNReal.rpow_eq_zero_iff, Real.toNNReal_zero, MeasureTheory.Measure.modularCharacterFun_pos, MeasureTheory.measureUnivNNReal_zero, NNReal.limsup_of_not_isBoundedUnder, CompactlySupportedContinuousMap.toReal_smul, zero_eq_nndist, MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous, NNReal.iSup_empty, HasOuterApproxClosed.indicator_le_apprSeq, NNReal.coe_pos, NNReal.HolderTriple.inv_pos, CompactlySupportedContinuousMap.nnrealPart_apply, PMF.mem_support_bernoulli_iff, NNReal.liminf_of_not_isCoboundedUnder, ContinuousLinearMap.opNNNorm_subsingleton, CompactlySupportedContinuousMap.eq_toRealPositiveLinear_toReal, NNReal.continuousOn_rpow_const_compl_zero, Mathlib.Meta.Positivity.nnabs_pos_of_pos, MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous, NNReal.ball_zero_eq_Ico, NNReal.coeNNRealReal_zero, WithZeroMulInt.toNNReal_pos_apply, NNReal.sInf_empty, Real.nnreal_trichotomy, Inseparable.nndist_eq_zero, Metric.inseparable_iff_nndist, CompactlySupportedContinuousMap.nnrealPart_smul_pos, NNReal.HolderTriple.inv_nonneg', ContinuousMap.toNNReal_neg_one, IndiscreteTopology.nnnorm_eq_zero', Metric.packingNumber_zero, NNReal.iInf_empty, Real.nnabs_pos, MeasureTheory.Measure.addModularCharacterFun_pos, MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN, PreTilt.map_eq_zero, NNReal.HolderTriple.one_div_pos, MeasureTheory.FiniteMeasure.testAgainstNN_smul, MeasureTheory.FiniteMeasure.mass_zero_iff, MemHolder.nnHolderNorm_eq_zero, ContinuousLinearEquiv.nnnorm_symm_pos, NNReal.instIsStrictOrderedModule, NNReal.nhds_zero_basis, ContinuousMapZero.toNNReal_neg_smul, ContinuousLinearMap.nnbound, uniformity_basis_edist_nnreal, MeasureTheory.Measure.toSphereBallBound_pos, ProbabilityTheory.HasSubgaussianMGF.zero, NNReal.closedBall_zero_eq_Icc', NNReal.nndist_zero_eq_val', LipschitzWith.const, NNReal.tendsto_tsum_compl_atTop_zero, MeasureTheory.exists_eLpNorm_indicator_le, NNRealRMK.integral_rieszMeasure, NNReal.HolderConjugate.sub_one_pos, IndiscreteTopology.nnnorm_eq_zero, CompactlySupportedContinuousMap.monotone_of_nnreal, ContinuousMapZero.toNNReal_smul, lipschitzExtensionConstant_pos, NNReal.agm_zero_left, NNReal.coe_list_sum, ModP.preVal_eq_zero, NNReal.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, NNReal.HolderTriple.nonneg, Metric.isCover_zero, MeasureTheory.distribHaarChar_pos, LinearMap.injective_iff_antilipschitz, ENNReal.instPosSMulStrictMonoNNReal, ContinuousMapZero.continuous_toNNReal, MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN, continuousOn_cfcₙ_nnreal_setProd, ENNReal.toNNReal_pos_iff, NNReal.instNoZeroDivisors, NNReal.tendsto_cofinite_zero_of_summable, HasOuterApproxClosed.exAppr, EMetric.exists_pos_forall_lt_edist, NNReal.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, NNReal.coe_single, CompactlySupportedContinuousMap.exists_add_nnrealPart_add_eq, ENNReal.coe_indicator, MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto, Metric.exists_pos_forall_lt_edist, MeasureTheory.Lp.nnnorm_zero, NNReal.iInf_const_zero, MeasureTheory.SimpleFunc.map_coe_ennreal_restrict, BoundedContinuousFunction.lintegral_le_edist_mul, NNReal.tendsto_pow_atTop_nhds_zero_iff, MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite, NNReal.HolderTriple.one_div_pos', NNReal.holderTriple_iff, FormalMultilinearSeries.comp_summable_nnreal, ENNReal.toNNReal_zero, Delone.DeloneSet.coveringRadius_pos, ProbabilityTheory.Kernel.HasSubgaussianMGF.fun_zero, IsCoercive.antilipschitz, MeasureTheory.FiniteMeasure.null_iff_toMeasure_null
|