| Name | Category | Theorems |
|---|
instConditionallyCompleteLinearOrder 📖 | CompOp | 49 mathmath: ProbabilityTheory.cdf_measure_stieltjesFunction, limsup_of_not_isBoundedUnder, volume_val, ENNReal.liminf_toReal_eq, isBigO_norm_Icc_restrict_atTop, liminf_of_not_isBoundedUnder, ProbabilityTheory.IsMeasurableRatCDF.instIsProbabilityMeasure_stieltjesFunction, volume_eq_stieltjes_id, limsSup_of_not_isCobounded, continuousMap_mem_polynomialFunctions_closure, ENNReal.ofReal_limsup, ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_univ, Monotone.ae_hasDerivAt, StieltjesFunction.measurable_measure, le_limsup_mul, limsup_of_not_isCoboundedUnder, liminf_of_not_isCoboundedUnder, exists_polynomial_near_continuousMap, MeasureTheory.integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure, ProbabilityTheory.measurable_measure_stieltjesOfMeasurableRat, ENNReal.toReal_limsup, ProbabilityTheory.instIsProbabilityMeasureCondCDF, ProbabilityTheory.measure_cdf, ENNReal.ofReal_essSup, ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_Iic, limsInf_of_not_isBounded, ProbabilityTheory.measure_stieltjesOfMeasurableRat_univ, liminf_mul_le, ENNReal.toReal_essSup, ProbabilityTheory.measure_stieltjesOfMeasurableRat_Iic, isBigO_norm_Icc_restrict_atBot, limsInf_of_not_isCobounded, StieltjesFunction.ae_hasDerivAt, ProbabilityTheory.measure_condCDF_Iic, ProbabilityTheory.measurable_measure_condCDF, ProbabilityTheory.instIsProbabilityMeasure_stieltjesOfMeasurableRat, NNReal.toReal_limsup, le_liminf_mul, ProbabilityTheory.IsMeasurableRatCDF.measurable_measure_stieltjesFunction, ProbabilityTheory.measure_condCDF_univ, polynomialFunctions_closure_eq_top', NNReal.toReal_liminf, limsSup_of_not_isBounded, polynomialFunctions_closure_eq_top, ENNReal.limsup_toReal_eq, MeasureTheory.lpNorm_exponent_top_eq_essSup, limsup_mul_le, ProbabilityTheory.IsCondKernelCDF.toKernel_apply, ProbabilityTheory.instIsProbabilityMeasurecdf
|
instFloorRing 📖 | CompOp | 93 mathmath: Chebyshev.theta_eq_theta_coe_floor, ZLattice.covolume_eq_det_inv, natFloor_logb_natCast, nat_floor_real_sqrt_eq_nat_sqrt, round_exp_one_eq_three, CircleDeg1Lift.map_lt_add_floor_translationNumber_add_one, Chebyshev.psi_eq_psi_coe_floor, GaussianInt.toComplex_div_re, Chebyshev.psi_eq_sum_theta, Chebyshev.psi_sub_theta_eq_sum_not_prime, CircleDeg1Lift.floor_sub_le_translationNumber, Function.Periodic.sInf_add_zsmul_le_integral_of_pos, CircleDeg1Lift.map_le_of_map_zero, CircleDeg1Lift.le_map_of_map_zero, Nat.closedBall_eq_Icc, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, SimpleGraph.triangleRemovalBound_mul_cube_lt, Polynomial.card_eq_of_natDegree_le_of_coeff_le, Complex.arg_cos_add_sin_mul_I_sub, sum_mul_eq_sub_integral_mul', LSeries_eq_mul_integral_of_nonneg, Chebyshev.sum_PrimePow_eq_sum_sum, CircleDeg1Lift.le_floor_map_map_zero, Int.ball_eq_Ioo, Chebyshev.primeCounting_eq_theta_div_log_add_integral, sum_div_nat_floor_pow_sq_le_div_sq, natCeil_logb_natCast, convergent_succ, GaussianInt.toComplex_im_div, exists_nat_abs_mul_sub_round_le, unitInterval.fract_mem, Chebyshev.primeCounting_sub_theta_div_log_isBigO, Behrend.exp_neg_two_mul_le, floor_real_sqrt_eq_nat_sqrt, convergent_zero, sum_mul_eq_sub_integral_mul₀', CircleDeg1Lift.le_map_map_zero, Chebyshev.theta_eq_log_primorial, ProbabilityTheory.strong_law_aux6, CircleDeg1Lift.translationNumber_le_ceil_sub, harmonic_floor_le_one_add_log, Behrend.ceil_lt_mul, GaussianInt.toComplex_re_div, sum_mul_eq_sub_integral_mul₁, Chebyshev.psi_eq_theta_add_sum_theta, ceil_exp_one_eq_three, LSeries_eq_mul_integral, exists_convs_eq_rat, CircleDeg1Lift.le_ceil_map_map_zero, ceil_pi_eq_four, BoxIntegral.unitPartition.index_apply, ZLattice.volume_image_eq_volume_div_covolume, Chebyshev.theta_eq_sum_Icc, log_le_harmonic_floor, UnitAddCircle.norm_eq, convs_eq_convergent, ceil_logb_natCast, locallyIntegrableOn_mul_sum_Icc, ZLattice.volume_image_eq_volume_div_covolume', Int.closedBall_eq_Icc, ProbabilityTheory.strong_law_aux4, SimpleGraph.triangleRemovalBound_le, floor_logb_natCast, floor_pi_eq_three, CircleDeg1Lift.ceil_map_map_zero_le, ZLattice.isAddFundamentalDomain, Chebyshev.psi_eq_sum_Icc, integrableOn_mul_sum_Icc, ProbabilityTheory.strong_law_aux1, ProbabilityTheory.strong_law_aux2, AddCircle.norm_eq, Behrend.div_lt_floor, Function.Periodic.integral_le_sSup_add_zsmul_of_pos, sum_mul_eq_sub_sub_integral_mul', CircleDeg1Lift.map_fract_sub_fract_eq, floor_exp_one_eq_two, sum_mul_eq_sub_integral_mul, CircleDeg1Lift.floor_map_map_zero_le, AddCircle.norm_eq', Complex.Gamma_def, Complex.arg_mul_cos_add_sin_mul_I_sub, sum_mul_eq_sub_integral_mul₀, CircleDeg1Lift.map_map_zero_le, CircleDeg1Lift.mul_floor_map_zero_le_floor_iterate_zero, NumberField.Units.basisOfIsMaxRank_fundSystem, sum_mul_eq_sub_sub_integral_mul, Chebyshev.eventually_primeCounting_le, round_pi_eq_three, LSeries_eq_mul_integral', mul_pow_le_nat_floor_pow, ofDigits_digits_sum_eq, GaussianInt.toComplex_div_im, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne
|
instInfSet 📖 | CompOp | 84 mathmath: iInf_Ioi_eq_iInf_rat_gt, iInf_nonpos', iInf_of_isEmpty, sSup_smul_of_nonpos, gauge_def', ProbabilityTheory.IsMeasurableRatCDF.iInf_rat_gt_eq, norm_eq_iInf_iff_real_inner_le_zero, iInf_nonneg, iInf_of_not_bddBelow, ediam_eq, ENNReal.ofReal_iInf, iInf_mul_of_nonneg, ContinuousAlternatingMap.norm_def, sInf_of_not_bddBelow, sInf_le_sSup, sInf_smul_of_nonneg, PiTensorProduct.projectiveSeminorm_apply, Function.Periodic.sInf_add_zsmul_le_integral_of_pos, ContinuousLinearMap.iInf_rayleigh_eq_iInf_rayleigh_sphere, Submodule.norm_eq_iInf_iff_inner_eq_zero, BoundedContinuousFunction.dist_eq, StieltjesFunction.iInf_rat_gt_eq, Set.Nontrivial.infsep_eq_iInf, iSup_mul_of_nonpos, iInf_const_zero, ArchimedeanClass.stdPart_eq_sInf, BoundedContinuousFunction.norm_eq, Set.infsep_eq_iInf, Submodule.norm_eq_iInf_iff_real_inner_eq_zero, GroupSeminorm.inf_apply, le_sInf, mul_iInf_of_nonneg, sInf_neg, smul_iInf_of_nonpos, ContinuousLinearMap.norm_def, iInf_mul_of_nonpos, ContinuousOn.isBigOWith_rev_principal, diam_eq, gauge_def, sInf_nonpos, sInf_nonneg, quotient_norm_mk_eq, Seminorm.inf_apply, sInf_empty, sInf_univ, NormedAddGroupHom.IsQuotient.norm, LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional, ConvexOn.hasDerivWithinAt_sInf_slope_of_mem_interior, ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt, ENNReal.toReal_iInf, IsSelfAdjoint.hasEigenvector_of_isMinOn, NNReal.coe_iInf, sInf_le_iff, sInf_smul_of_nonpos, BoundedContinuousFunction.norm_eq_of_nonempty, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt, exists_norm_eq_iInf_of_complete_convex, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def, StieltjesFunction.iInf_Ioi_eq, sInf_nonpos', Submodule.starProjection_minimal, SchwartzMap.seminorm_apply, le_iInf, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def', smul_iSup_of_nonpos, ProbabilityTheory.iInf_rat_gt_defaultRatCDF, mul_iSup_of_nonpos, Metric.infDist_eq_iInf, ContinuousMultilinearMap.norm_def, NormedAddGroupHom.norm_def, isGLB_sInf, mul_iInf_of_nonpos, sSup_neg, Submodule.exists_norm_eq_iInf_of_complete_subspace, sInf_def, AddGroupSeminorm.inf_apply, iInf_nonpos, ConvexOn.rightDeriv_eq_sInf_slope_of_mem_interior, tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici, lt_sInf_add_pos, smul_iInf_of_nonneg, ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq, NNReal.coe_sInf, ENNReal.toReal_sInf
|
instSupSet 📖 | CompOp | 106 mathmath: HasCompactSupport.convolution_integrand_bound_left, sSup_smul_of_nonpos, BoundedContinuousFunction.dist_eq_iSup, ContinuousLinearMap.sSup_unit_ball_eq_norm, NonarchAddGroupSeminorm.coe_iSup_apply, sSup_empty, GroupSeminorm.coe_iSup_apply, ContinuousLinearMap.iSup_rayleigh_eq_iSup_rayleigh_sphere, iSup_nonneg', NNReal.coe_sSup, ediam_eq, add_neg_lt_sSup, ConvexOn.univ_sSup_of_countable_affine_eq, NNReal.coe_iSup, iSup_nonpos, IsUltrametricDist.invariantExtension_apply, sInf_le_sSup, tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici, IsUltrametricDist.norm_tsum_le, sSup_smul_of_nonneg, IsUltrametricDist.norm_tprod_le, sSup_nonpos, ContinuousMap.norm_eq_iSup_norm, NumberField.mulHeight_eq, spectralNorm_eq_iSup_of_finiteDimensional_normal, LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional, Hyperreal.isSt_sSup, iSup_mul_of_nonpos, sSup_nonneg, IsSelfAdjoint.hasEigenvector_of_isMaxOn, ConvexOn.sSup_of_countable_affine_eq, iSup_pow, PiLp.dist_eq_iSup, ConvexOn.real_univ_sSup_of_countable_affine_eq, WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup, ConvexOn.sSup_of_nat_affine_eq, Seminorm.iSup_apply, sInf_neg, AddGroupSeminorm.coe_iSup_apply, smul_iInf_of_nonpos, iSup_const_zero, ContinuousLinearMap.sSup_sphere_eq_norm, iInf_mul_of_nonpos, diam_eq, Height.mulHeight_eq, PiTensorProduct.injectiveSeminorm_apply, iSup_of_isEmpty, PiLp.norm_eq_ciSup, Seminorm.coe_sSup_eq', ContinuousOn.isBigOWith_principal, iSup_pow_of_ne_zero, AddGroupSeminorm.coe_sSup_apply, sSup_le, ConvexOn.real_univ_sSup_affine_eq, AddGroupSeminorm.coe_sSup_apply', sSup_univ, ConvexOn.hasDerivWithinAt_sSup_slope_of_mem_interior, CStarModule.norm_eq_csSup, Seminorm.continuous_iSup, Seminorm.coe_sSup_eq, iSup_mul_of_nonneg, GroupSeminorm.coe_sSup_apply', iSup_of_not_bddAbove, ConvexOn.univ_sSup_affine_eq, ConvexOn.real_univ_sSup_of_nat_affine_eq, ConvexOn.leftDeriv_eq_sSup_slope_of_mem_interior, ConvexOn.real_sSup_of_countable_affine_eq, ENNReal.toReal_sSup, iSup_le, OrthonormalBasis.norm_le_card_mul_iSup_norm_inner, sInf_smul_of_nonpos, max_norm_root_eq_spectralValue, sSup_def, smul_iSup_of_nonneg, smul_iSup_of_nonpos, Function.Periodic.integral_le_sSup_add_zsmul_of_pos, le_sSup_iff, lp.norm_eq_ciSup, Polynomial.supNorm_eq_iSup, ContinuousLinearMap.sSup_unitClosedBall_eq_norm, Seminorm.coe_iSup_eq, mul_iSup_of_nonpos, sSup_of_not_bddAbove, GroupSeminorm.coe_sSup_apply, isLUB_sSup, NonarchAddGroupSeminorm.coe_sSup_apply', ConvexOn.real_sSup_of_nat_affine_eq, BoundedContinuousFunction.norm_eq_iSup_norm, Hyperreal.st_eq_sSup, UniformFun.dist_def, mul_iInf_of_nonpos, sSup_neg, ConvexOn.sSup_affine_eq, sInf_def, NonarchAddGroupSeminorm.coe_sSup_apply, HasCompactSupport.convolution_integrand_bound_right, ConvexOn.real_sSup_affine_eq, iSup_nonneg, HasCompactSupport.convolution_integrand_bound_right_of_subset, ConvexOn.univ_sSup_of_nat_affine_eq, Seminorm.sSup_apply, ENNReal.toReal_iSup, ContinuousMap.dist_eq_iSup, ArchimedeanClass.stdPart_eq_sSup, mul_iSup_of_nonneg, sSup_nonneg'
|