| Name | Category | Theorems |
|---|
MemLp 📖 | MathDef | 95 mathmath: ProbabilityTheory.IsGaussian.memLp_id, ProbabilityTheory.IdentDistrib.memLp_iff, memLp_top_of_bound, memLp_congr_ae, ContinuousLinearMap.comp_memLp, AEStronglyMeasurable.memLp_truncation, LipschitzWith.memLp_lineDeriv, mem_L1_toReal_of_lintegral_ne_top, AntitoneOn.memLp_isCompact, Lp.memLp, memLp_indicator_const, LipschitzWith.memLp_comp_iff_of_antilipschitz, MemLp.zero, ProbabilityTheory.evariance_lt_top_iff_memLp, SimpleFunc.memLp_zero, UniformIntegrable.memLp_of_tendstoInMeasure, memLp_two_iff_integrable_sq_norm, integrable_norm_rpow_iff, UniformIntegrable.memLp_of_ae_tendsto, ProbabilityTheory.Kernel.HasSubgaussianMGF.memLp_exp_mul, SchwartzMap.memLp, SimpleFunc.memLp_iff_integrable, ProbabilityTheory.IsGaussian.memLp_two_id, memLp_const_iff, memLp_measure_zero, memLp_haarAddCircle_iff, MeasurableEmbedding.memLp_map_measure_iff, MemLp.of_discrete, MonotoneOn.memLp_of_measure_ne_top, ProbabilityTheory.memLp_of_mem_interior_integrableExpSet, HasCompactSupport.memLp_of_bound, SimpleFunc.memLp_iff_finMeasSupp, memLp_two_iff_integrable_sq, AntitoneOn.memLp_top, BoundedContinuousFunction.memLp_top, memLp_prod_iff, SimpleFunc.memLp_of_finite_measure_preimage, SimpleFunc.memLp_iff, memLp_const_iff_enorm, ProbabilityTheory.evariance_eq_top_iff, ProbabilityTheory.Kernel.memL1_limitProcess_densityProcess, ProbabilityTheory.memLp_id_gaussianReal', memLp_congr_norm, L1.SimpleFunc.toLp_one_eq_toL1, ProbabilityTheory.HasSubgaussianMGF.memLp_exp_mul, Continuous.memLp_of_hasCompactSupport, MeasurableEquiv.memLp_map_measure_iff, SimpleFunc.memLp_top, memL1_smul_of_L1_withDensity, integrable_enorm_rpow_iff, ProbabilityTheory.IsGaussian.memLp_dual, Lp.simpleFunc.memLp, memLp_top_const_enorm, AntitoneOn.memLp_of_measure_ne_top, Lp.mem_Lp_iff_memLp, memLp_pi_iff, memLp_indicator_iff_restrict, ProbabilityTheory.HasCondSubgaussianMGF.memLp_exp_mul, memLp_piLp_iff, memLp_top_of_bound_enorm, memLp_const_enorm, MemLp.zero', Filtration.memLp_limitProcess_of_eLpNorm_bdd, memLp_add_of_disjoint, ProbabilityTheory.memLp_id_gaussianReal, memLp_norm_rpow_iff, Continuous.memLp_top_of_hasCompactSupport, MemLp.of_bound, memLp_enorm_iff, SimpleFunc.memLp_of_isFiniteMeasure, UniformIntegrable.memLp, ProbabilityTheory.memLp_tilted_mul, memLp_prodLp_iff, SchwartzMap.memLp_top, ProbabilityTheory.HasSubgaussianMGF.memLp, memLp_neg_iff, MonotoneOn.memLp_isCompact, memLp_enorm_rpow_iff, MemLp.of_enorm_bound, MonotoneOn.memLp_top, ProbabilityTheory.IsGaussian.memLp_two_fun_id, memLp_of_bounded, Submartingale.memLp_limitProcess, memLp_congr_enorm, memLp_zero_iff_aestronglyMeasurable, memLp_norm_iff, memLp_one_iff_integrable, ProbabilityTheory.HasGaussianLaw.memLp, memLp_trim_of_mem_lpMeasSubgroup, ProbabilityTheory.HasGaussianLaw.memLp_two, memLp_re_im_iff, memLp_map_measure_iff, memLp_top_const, memLp_const, exists_continuous_eLpNorm_sub_le_of_closed
|
eLpNorm 📖 | CompOp | 190 mathmath: MemLp.eLpNorm_indicator_le_of_meas, tendsto_Lp_of_tendsto_ae, Lp.tendsto_Lp_iff_tendsto_eLpNorm'', eLpNorm_condExp_le, eLpNorm_le_mul_eLpNorm_of_ae_le_mul'', eLpNorm_smul_le_mul_eLpNorm, unifTight_iff_real, eLpNorm_eq_zero_of_ae_zero, MemLp.exists_simpleFunc_eLpNorm_sub_lt, MemLp.toLp_val, Lp.cauchySeq_Lp_iff_cauchySeq_eLpNorm, eLpNorm_mono_nnnorm_ae, Lp.edist_def, tendsto_Lp_of_tendstoInMeasure, Lp.dist_def, eLpNorm_const_lt_top_iff_enorm, le_eLpNorm_of_bddBelow, Lp.nnnorm_def, eLpNorm_le_mul_eLpNorm_of_ae_le_mul', Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top, eLpNorm_exponent_top, eLpNorm_of_isEmpty, eLpNorm_smul_measure_of_ne_top', eLpNorm_top_piecewise, eLpNorm_add_lt_top, eLpNorm_le_eLpNorm_mul_eLpNorm_top, eLpNorm_le_of_ae_nnnorm_bound, eLpNorm_mono_real, mul_meas_ge_le_pow_eLpNorm', Lp.enorm_toLp, ProbabilityTheory.IdentDistrib.eLpNorm_eq, eLpNorm_sub_le, MemLp.exist_eLpNorm_sub_le, SchwartzMap.eLpNorm_lt_top, eLpNorm_norm, uniformIntegrable_iff, eLpNorm_congr_enorm_ae, eLpNorm_exponent_zero, tendstoInMeasure_iff_tendsto_Lp, eLpNorm_mono_ae, Lp.edist_toLp_toLp, eLpNorm_ofReal, Integrable.tendsto_eLpNorm_condExp, eLpNorm_indicator_sub_le_of_dist_bdd, eLpNorm_restrict_eq_of_support_subset, Lp.edist_toLp_zero, eLpNorm_eq_zero_iff, eLpNorm_one_eq_lintegral_enorm, eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul', Lp.norm_toLp, eLpNorm_zero, eLpNorm_one_le_of_le', eLpNorm_one_smul_measure, eLpNorm_le_eLpNorm_top_mul_eLpNorm, Submartingale.eLpNorm_stoppedAbove_le, eLpNorm_enorm, toReal_eLpNorm, eLpNorm_le_eLpNorm_fderiv_of_eq_inner, eLpNorm_sub_comm, UniformIntegrable.spec', Lp.nnnorm_toLp, eLpNorm_smul_measure_of_ne_top, eLpNorm_eq_eLpNorm', eLpNorm_star, eLpNorm_zero', eLpNorm_le_add_measure_left, eLpNorm_le_mul_eLpNorm_of_ae_le_mul, SchwartzMap.norm_toLp, eLpNorm_le_add_measure_right, Lp.eLpNorm_lim_le_liminf_eLpNorm, Submartingale.eLpNorm_stoppedAbove_le', eLpNorm_trim, eLpNorm_le_eLpNorm_fderiv_one, eLpNorm_nnreal_eq_eLpNorm', eLpNorm_trim_ae, eLpNorm_indicator_eq_eLpNorm_restrict, MemLp.eLpNorm_eq_integral_rpow_norm, eLpNorm_const_smul_le', eLpNorm_indicator_const_le, eLpNorm_sub_le', eLpNorm_le_eLpNorm_fderiv_of_le, eLpNorm_le_of_ae_enorm_bound, eLpNorm_const', eLpNorm_indicator_le_of_bound, eLpNorm_neg, MemLp.exists_hasCompactSupport_eLpNorm_sub_le, Lp.simpleFunc.norm_toSimpleFunc, L2.eLpNorm_inner_lt_top, MeasurableEmbedding.eLpNorm_map_measure, Submartingale.stoppedValue_leastGE_eLpNorm_le, eLpNorm_indicator_sub_indicator, unifTight_iff_ennreal, eLpNorm_nnreal_eq_lintegral, eLpNorm_congr_nnnorm_ae, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess, SchwartzMap.eLpNorm_le_seminorm, eLpNorm_const_smul_le, StrongDual.norm_toLpₗ_le, eLpNorm_lt_top_of_finite, tendsto_eLpNorm_condExp, eLpNorm_one_condExp_le_eLpNorm, eLpNorm_mono_ae_real, eLpNorm_congr_norm_ae, eLpNorm_const_smul, eLpNorm_mono_enorm, eLpNorm_norm_rpow, exists_Lp_half, eLpNorm_indicator_le, Submartingale.tendsto_eLpNorm_one_limitProcess, eLpNorm_one_le_of_le, ProbabilityTheory.strong_law_Lp, eLpNorm_mono, eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm, meas_ge_le_mul_pow_eLpNorm_enorm, Lp.mem_Lp_iff_eLpNorm_lt_top, MemLp.eLpNorm_indicator_le, eLpNorm_mono_enorm_ae, eLpNorm_le_eLpNorm_fderiv_of_eq, UnifTight.exists_measurableSet_indicator, Lp.eLpNorm_lt_top, eLpNorm_eq_lintegral_rpow_enorm_toReal, MemLp.exists_boundedContinuous_eLpNorm_sub_le, eLpNorm_indicator_const', MemLp.eLpNorm_indicator_norm_ge_pos_le, ProbabilityTheory.Kernel.eLpNorm_densityProcess_le, UniformIntegrable.spec, pow_mul_meas_ge_le_eLpNorm, eLpNorm_const, eLpNorm_add_le, ProbabilityTheory.Kernel.eLpNorm_density_le, Measure.HasTemperateGrowth.exists_eLpNorm_lt_top, Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf, Lp.enorm_def, eLpNorm_le_eLpNorm_mul_rpow_measure_univ, Lp.tendsto_Lp_iff_tendsto_eLpNorm', eLpNorm_eq_lintegral_rpow_enorm, eLpNorm_indicator_const₀, eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg, MemLp.eLpNorm_lt_top, eLpNorm_mono_ae', eLpNorm_const_lt_top_iff, tendsto_Lp_finite_of_tendstoInMeasure, eLpNorm_mono_measure, eLpNorm_map_measure, eLpNorm_add_le', HasCompactSupport.exist_eLpNorm_sub_le_of_continuous, ofReal_lpNorm, eLpNorm_condExpL2_le, eLpNorm_le_eLpNorm_of_exponent_le, eLpNorm_sub_le_of_dist_bdd, eLpNorm_one_add_measure, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_restrict_densityProcess_limitProcess, exists_eLpNorm_indicator_le, eLpNorm_enorm_rpow, eLpNorm_smul_measure_of_ne_zero, eLpNorm_nnreal_pow_eq_lintegral, AEEqFun.eLpNorm_compMeasurePreserving, eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm, eLpNorm_aeeqFun, eLpNorm_le_eLpNorm_fderiv, eLpNorm_smul_measure_of_ne_zero', eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top, AEEqFun.eLpNorm_star, MemLp.eLpNorm_indicator_le', eLpNorm_congr_ae, mul_meas_ge_le_pow_eLpNorm, eLpNorm_comp_measurePreserving, eLpNorm_restrict_le, eLpNorm_measure_zero, eLpNorm_sum_le, tendstoInMeasure_iff_tendsto_Lp_finite, eLpNorm_mono_nnnorm, eLpNorm_conj, Lp.tendsto_Lp_iff_tendsto_eLpNorm, tendsto_Lp_finite_of_tendsto_ae_of_meas, L2.eLpNorm_rpow_two_norm_lt_top, eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul, eLpNorm_le_of_ae_bound, eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm, Submartingale.stoppedValue_leastGE_eLpNorm_le', eLpNorm_indicator_const, MemLp.eLpNorm_indicator_norm_ge_le, MemLp.eLpNorm_mk_lt_top, MemLp.exists_eLpNorm_indicator_compl_lt, Lp.simpleFunc.norm_toLp, tendsto_Lp_finite_of_tendsto_ae, eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top, Lp.norm_def, eLpNorm_nsmul, exists_continuous_eLpNorm_sub_le_of_closed
|
eLpNorm' 📖 | CompOp | 50 mathmath: eLpNorm'_norm, eLpNorm'_sum_le, eLpNorm'_const', eLpNorm'_zero', eLpNorm'_mono_enorm_ae, eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul, eLpNorm'_mono_nnnorm_ae, eLpNorm'_trim, eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul, eLpNorm'_measure_zero_of_pos, eLpNorm'_congr_norm_ae, eLpNorm'_enorm, eLpNorm'_neg, eLpNorm'_eq_zero_of_ae_eq_zero, eLpNorm'_le_eLpNormEssSup, eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul', eLpNorm'_smul_le_mul_eLpNorm', eLpNorm'_smul_measure, eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ, eLpNorm'_congr_enorm_ae, eLpNorm_eq_eLpNorm', lintegral_rpow_enorm_eq_rpow_eLpNorm', eLpNorm'_mono_measure, eLpNorm'_mono_ae, eLpNorm'_zero, eLpNorm_nnreal_eq_eLpNorm', eLpNorm'_eq_zero_of_ae_zero, eLpNorm'_congr_nnnorm_ae, eLpNorm'_le_eLpNorm'_of_exponent_le, Lp.eLpNorm'_lim_eq_lintegral_liminf, eLpNorm'_congr_ae, eLpNorm'_le_eLpNorm'_mul_eLpNorm', eLpNorm'_const_smul, eLpNorm'_eq_zero_of_ae_zero', eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ, eLpNorm'_add_le_of_le_one, SimpleFunc.eLpNorm'_eq, eLpNorm'_measure_zero_of_neg, eLpNorm'_eq_zero_iff, eLpNorm'_const_smul_le, eLpNorm'_add_le, eLpNorm'_const_smul_le', eLpNorm'_measure_zero_of_exponent_zero, eLpNorm'_eq_lintegral_enorm, eLpNorm'_const_of_isProbabilityMeasure, eLpNorm'_norm_rpow, eLpNorm'_const, eLpNorm'_enorm_rpow, eLpNorm'_exponent_zero, Lp.eLpNorm'_lim_le_liminf_eLpNorm'
|
eLpNormEssSup 📖 | CompOp | 41 mathmath: eLpNormEssSup_le_of_ae_enorm_bound, eLpNormEssSup_const_smul_le, eLpNormEssSup_const_smul, eLpNorm_exponent_top, eLpNormEssSup_mono_enorm_ae, eLpNormEssSup_zero, enorm_ae_le_eLpNormEssSup, meas_eLpNormEssSup_lt, eLpNormEssSup_mono_measure, eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul', eLpNormEssSup_lt_top_of_ae_enorm_bound, eLpNormEssSup_eq_iSup, eLpNorm'_le_eLpNormEssSup, MemLp.eLpNormEssSup_indicator_norm_ge_eq_zero, eLpNormEssSup_const, eLpNormEssSup_piecewise, eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul, eLpNormEssSup_mono_nnnorm_ae, eLpNormEssSup_le_of_ae_bound, eLpNormEssSup_smul_measure, ae_le_eLpNormEssSup, eLpNormEssSup_eq_essSup_enorm, eLpNormEssSup_trim, eLpNormEssSup_map_measure, eLpNormEssSup_add_le, eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ, eLpNormEssSup_count, eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict, eLpNormEssSup_lt_top_iff_isBoundedUnder, eLpNormEssSup_lt_top_of_ae_bound, eLpNormEssSup_indicator_const_le, eLpNormEssSup_lt_top_of_ae_nnnorm_bound, eLpNormEssSup_indicator_le, eLpNormEssSup_congr_ae, eLpNormEssSup_eq_zero_iff, MeasurableEmbedding.eLpNormEssSup_map_measure, eLpNormEssSup_measure_zero, eLpNormEssSup_ennreal_smul_measure, eLpNormEssSup_indicator_const_eq, eLpNormEssSup_le_of_ae_nnnorm_bound, eLpNormEssSup_const_smul_le'
|
lpNorm 📖 | CompOp | 47 mathmath: lpNorm_conj, lpNorm_fun_div_natCast, lpNorm_neg, lpNorm_add_le', lpNorm_nonneg, lpNorm_fun_zero, lpNorm_fun_neg, lpNorm_add_le, lpNorm_mul_natCast, lpNorm_smul_measure_of_ne_zero, lpNorm_one_eq_integral_norm, lpNorm_measure_zero, lpNorm_le_add_lpNorm_add, lpNorm_sub_comm, toReal_eLpNorm, lpNorm_fun_mul_natCast, lpNorm_sub_le, lpNorm_fun_natCast_mul, lpNorm_le_lpNorm_add_lpNorm_sub', lpNorm_sub_le_lpNorm_sub_add_lpNorm_sub, lpNorm_abs, lpNorm_nnreal_eq_integral_norm_rpow, ae_le_lpNorm_exponent_top, lpNorm_norm, lpNorm_nsmul, lpNorm_le_lpNorm_add_lpNorm_sub, lpNorm_zero, lpNorm_const_smul, lpNorm_one, lpNorm_div_natCast, lpNorm_of_isEmpty, lpNorm_sum_le, lpNorm_mono_real, lpNorm_of_not_aestronglyMeasurable, lpNorm_natCast_mul, lpNorm_expect_le, lpNorm_eq_integral_norm_rpow_toReal, ofReal_lpNorm, lpNorm_smul_measure_of_ne_top, lpNorm_one', lpNorm_const, lpNorm_eq_zero, lpNorm_exponent_top_eq_essSup, lpNorm_of_not_memLp, lpNorm_exponent_zero, lpNorm_const', lpNorm_fun_abs
|