| Metric | Count |
|---|
DefinitionstoAEEqFun, toAEEqFunAddHom, toAEEqFunLinearMap, toAEEqFunMulHom, LiftPred, LiftRel, cast, comp, compMeasurable, compMeasurePreserving, compQuasiMeasurePreserving, comp₂, comp₂Measurable, const, instAdd, instAddCommGroup, instAddCommMonoid, instAddGroup, instAddMonoid, instCoeFun, instCommGroup, instCommMonoid, instDistribMulAction, instDiv, instGroup, instInf, instInhabited, instInv, instInvolutiveStarOfContinuousStar, instLattice, instModule, instMonoid, instMul, instMulAction, instNeg, instOne, instPartialOrder, instPowInt, instPowNat, instPreorder, instSMul, instStarOfContinuousStar, instSub, instSup, instZero, lintegral, mk, pair, posPart, toGerm, toGermAddMonoidHom, toGermMonoidHom, aeEqSetoid, «term_→ₘ[_]_» | 54 |
TheoremscoeFn_toAEEqFun, add_toGerm, aemeasurable, aestronglyMeasurable, coeFn_abs, coeFn_add, coeFn_comp, coeFn_compMeasurable, coeFn_compMeasurePreserving, coeFn_compQuasiMeasurePreserving, coeFn_comp₂, coeFn_comp₂Measurable, coeFn_const, coeFn_const_eq, coeFn_div, coeFn_inf, coeFn_inv, coeFn_le, coeFn_mk, coeFn_mul, coeFn_neg, coeFn_one, coeFn_one_eq, coeFn_pair, coeFn_posPart, coeFn_pow, coeFn_smul, coeFn_star, coeFn_sub, coeFn_sup, coeFn_zero, coeFn_zero_eq, coeFn_zpow, compMeasurable_eq_mk, compMeasurable_mk, compMeasurable_toGerm, compMeasurePreserving_eq_mk, compMeasurePreserving_mk, compMeasurePreserving_toGerm, compQuasiMeasurePreserving_eq_mk, compQuasiMeasurePreserving_mk, compQuasiMeasurePreserving_toGerm, comp_comp, comp_compQuasiMeasurePreserving, comp_eq_mk, comp_id, comp_mk, comp_toGerm, comp₂Measurable_eq_mk, comp₂Measurable_eq_pair, comp₂Measurable_mk_mk, comp₂Measurable_toGerm, comp₂_eq_mk, comp₂_eq_pair, comp₂_mk_mk, comp₂_toGerm, div_toGerm, ext, ext_iff, induction_on, induction_on₂, induction_on₃, inf_le_left, inf_le_right, instIsCentralScalar, instIsScalarTower, instSMulCommClass, instTrivialStar, inv_mk, inv_toGerm, le_inf, le_sup_left, le_sup_right, liftRel_iff_coeFn, liftRel_mk_mk, lintegral_add, lintegral_coeFn, lintegral_eq_zero_iff, lintegral_mk, lintegral_mono, lintegral_zero, measurable, mk_add_mk, mk_coeFn, mk_div, mk_eq_mk, mk_le_mk, mk_mul_mk, mk_pow, mk_sub, mk_toGerm, mk_zpow, mul_toGerm, neg_mk, neg_toGerm, one_def, one_toGerm, pair_eq_mk, pair_mk_mk, posPart_mk, pow_toGerm, quot_mk_eq_mk, smul_mk, smul_toGerm, stronglyMeasurable, sub_toGerm, sup_le, tendsto_ae_unique, toGermAddMonoidHom_apply, toGermMonoidHom_apply, toGerm_eq, toGerm_injective, zero_def, zero_toGerm, zpow_toGerm | 115 |
| Total | 169 |
| Name | Category | Theorems |
|---|
LiftPred 📖 | MathDef | — |
LiftRel 📖 | MathDef | 2 mathmath: liftRel_mk_mk, liftRel_iff_coeFn
|
cast 📖 | CompOp | 232 mathmath: MeasureTheory.integrable_indicatorConstLp, coeFn_smul, MeasureTheory.LpToLpRestrictCLM_coeFn, MeasureTheory.Lp.mul_meas_ge_le_pow_enorm', MeasureTheory.aestronglyMeasurable_condExpInd, MeasureTheory.mem_lpMeasSubgroup_iff_aestronglyMeasurable, ContinuousLinearMap.integral_compLp, MeasureTheory.condExpInd_ae_eq_condExpIndSMul, MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral, ContinuousMap.coeFn_toAEEqFun, MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_eLpNorm, ContinuousLinearMap.continuous_integral_comp_L1, MeasureTheory.Lp.edist_def, MeasureTheory.Lp.coeFn_add, ContinuousLinearMap.comp_memLp, MeasureTheory.Lp.eq_zero_iff_ae_eq_zero, MeasureTheory.Lp.ext_iff, MeasureTheory.Lp.coeFn_const, MeasureTheory.norm_setToFun_le_mul_norm', coeFn_inf, MeasureTheory.L1.ofReal_norm_eq_lintegral, coeFn_mul, MeasureTheory.Lp.dist_def, MeasureTheory.Lp.aestronglyMeasurable, compQuasiMeasurePreserving_eq_mk, coeFn_comp₂, MeasureTheory.Lp.memLp, MeasureTheory.Lp.nnnorm_def, MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq, MeasureTheory.L2.inner_def, MeasureTheory.MemLp.condExpL2_ae_eq_condExp, pair_eq_mk, MeasureTheory.Lp.finStronglyMeasurable, MeasureTheory.aestronglyMeasurable_condExpL2, MeasureTheory.condExpL1_of_aestronglyMeasurable', coeFn_neg, MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.L1.integrable_coeFn, MeasureTheory.condExpL2_indicator_ae_eq_smul, coeFn_sub, UnitAddTorus.mFourierCoeff_toLp, coeFn_le, lintegral_coeFn, MeasureTheory.continuous_setToFun, MeasureTheory.L1.dist_eq_integral_dist, MeasureTheory.L1.norm_def, MeasureTheory.integral_condExpL2_eq, coeFn_comp, toGerm_eq, MeasureTheory.setIntegral_condExpL2_indicator, coeFn_const, ContinuousLinearMap.setIntegral_compLp, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, MeasureTheory.setIntegral_condExpInd, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable, MeasureTheory.aestronglyMeasurable_condExpL1, hasSum_fourier_series_L2, MeasureTheory.integral_indicatorConstLp, MeasureTheory.Lp.coeFn_compMeasurePreserving, MeasureTheory.lintegral_nnnorm_condExpL2_le, integrable_coeFn, MeasureTheory.L1.setToFun_eq_setToL1, coeFn_abs, MeasureTheory.Lp.coeFn_smul, coeFn_compQuasiMeasurePreserving, MeasureTheory.integrableOn_Lp_of_measure_ne_top, MeasureTheory.Lp.coeFn_le, UnitAddTorus.coeFn_mFourierLp, MeasureTheory.setIntegral_condExpIndSMul, ext_iff, MeasureTheory.Lp.coeFn_negPart_eq_max, MeasureTheory.L2.integral_inner_eq_sq_eLpNorm, MeasureTheory.L2.inner_indicatorConstLp_one, DomMulAct.smul_aeeqFun_aeeq, SchwartzMap.coeFn_toLp, coeFn_mk, comp₂_eq_mk, MeasureTheory.isClosed_aestronglyMeasurable, MeasureTheory.Lp.coeFn_sup, liftRel_iff_coeFn, MeasureTheory.Lp_toLp_restrict_add, MeasureTheory.setIntegral_condExpL1, compMeasurePreserving_eq_mk, MeasureTheory.continuous_integral_integral, fourierCoeff_toLp, coeFn_sup, comp_eq_mk, ProbabilityTheory.Kernel.continuous_integral_integral, coeFn_comp₂Measurable, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, MeasureTheory.memL1_smul_of_L1_withDensity, MeasureTheory.condExp_ae_eq_condExpL1, DomAddAct.vadd_aeeqFun_aeeq, DomAddAct.vadd_Lp_ae_eq, MeasureTheory.setIntegral_condExpL1CLM_of_measure_ne_top, MeasureTheory.condExp_ae_eq_condExpL1CLM, BoundedContinuousFunction.coeFn_toLp, MeasureTheory.mem_lpMeasSubgroup_toLp_of_trim, UnitAddTorus.hasSum_mFourier_series_L2, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, ContinuousLinearMap.lpPairing_eq_integral, MeasureTheory.L2.eLpNorm_inner_lt_top, MeasureTheory.Lp.mem_Lp_iff_memLp, coeFn_compMeasurable, MeasureTheory.Lp.simpleFunc.coeFn_le, MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner, MeasureTheory.Lp.coeFn_nonneg, MeasureTheory.Lp.coeFn_lpSMul, MeasureTheory.Lp.simpleFunc.coeFn_zero, MeasureTheory.condExpIndSMul_nonneg, MeasureTheory.L1.dist_def, coeFn_add, ContinuousLinearMap.coeFn_compLpL, comp₂Measurable_eq_mk, MeasureTheory.setIntegral_indicatorConstLp, ProbabilityTheory.Kernel.continuous_integral_integral_comp, MeasureTheory.L1.aemeasurable_coeFn, MeasureTheory.integrable_condExpL2_of_isFiniteMeasure, measurable, ContinuousLinearMap.integral_comp_L1_comm, MeasureTheory.L1.measurable_coeFn, MeasureTheory.aestronglyMeasurable_condExpL1CLM, MeasureTheory.continuous_integral, MeasureTheory.integrable_condExpL2_indicator, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', MeasureTheory.Lp.smul_def, MeasureTheory.L1.stronglyMeasurable_coeFn, ContinuousMap.coeFn_toLp, coeFn_star, MeasureTheory.Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq, coeFn_zero, MeasureTheory.tendstoInMeasure_of_tendsto_Lp, ProbabilityTheory.condVar_of_sigmaFinite, MeasureTheory.lpTrimToLpMeas_ae_eq, coeFn_compMeasurePreserving, mk_coeFn, MeasureTheory.isComplete_aestronglyMeasurable, MeasureTheory.L1.integral_of_fun_eq_integral, MeasureTheory.setLIntegral_nnnorm_condExpIndSMul_le, coeFn_inv, MeasureTheory.withDensitySMulLI_apply, UnitAddTorus.hasSum_prod_mFourierCoeff, DomMulAct.smul_Lp_ae_eq, MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top, MeasureTheory.aestronglyMeasurable_condExpIndSMul, MeasureTheory.L2.mem_L1_inner, MeasureTheory.L1.integral_eq_integral, MeasureTheory.Integrable.coeFn_toL1, MeasureTheory.L1.aestronglyMeasurable_coeFn, MeasureTheory.Lp.eLpNorm_lt_top, MeasureTheory.L2.integrable_inner, MeasureTheory.Lp.coeFn_negPart, MeasureTheory.L1.integral_of_fun_eq_integral', MeasureTheory.condExp_of_sigmaFinite, MeasureTheory.norm_setToFun_le_mul_norm, coeFn_posPart, MeasureTheory.MemLp.coeFn_toLp, coeFn_const_eq, MeasureTheory.setToFun_mono_left, MeasureTheory.Lp.coeFn_zero, MeasureTheory.norm_Lp_toLp_restrict_le, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, hasSum_sq_fourierCoeff, MeasureTheory.Lp.enorm_def, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm', UnitAddTorus.mFourierBasis_repr, MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul, LipschitzWith.coeFn_compLp, fourierBasis_repr, MeasureTheory.condExpL1_mono, MeasureTheory.Lp.coeFn_neg, MeasureTheory.Lp.coeFn_abs, MeasureTheory.Lp.coeFn_sub, coeFn_zpow, MeasureTheory.Lp.meas_ge_le_mul_pow_enorm, UnitAddTorus.hasSum_sq_mFourierCoeff, aemeasurable, ContinuousLinearMap.coeFn_compLp, MeasureTheory.lintegral_nnnorm_condExpIndSMul_le, aestronglyMeasurable, MeasureTheory.integrable_condExpIndSMul, MeasureTheory.Lp.toTemperedDistribution_apply, MeasureTheory.Lp.coeFn_posPart, coeFn_pow, MeasureTheory.L1.norm_sub_eq_lintegral, MeasureTheory.integrable_condExpL1, stronglyMeasurable, MeasureTheory.setIntegral_condExpL1CLM, MeasureTheory.L1.hasFiniteIntegral_coeFn, tsum_sq_fourierCoeff, MeasureTheory.lpMeasToLpTrim_ae_eq, MeasureTheory.eLpNorm_condExpL2_le, coeFn_zero_eq, MeasureTheory.condExpIndSMul_ae_eq_smul, MeasureTheory.Lp.dense_hasCompactSupport_contDiff, eLpNorm_compMeasurePreserving, MeasureTheory.lpMeas.ae_fin_strongly_measurable', MeasureTheory.eLpNorm_aeeqFun, MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq, MeasureTheory.L1.ofReal_norm_sub_eq_lintegral, MeasureTheory.Lp.coeFn_inf, coeFn_div, eLpNorm_star, MeasureTheory.L1.edist_def, MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun, MeasureTheory.continuous_setIntegral, MeasureTheory.Lp.pow_mul_meas_ge_le_enorm, MeasureTheory.indicatorConstLp_coeFn, compMeasurable_eq_mk, MeasureTheory.Lp.simpleFunc.coeFn_nonneg, MeasureTheory.memLp_trim_of_mem_lpMeasSubgroup, MeasureTheory.continuous_L1_toL1, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm, coeFn_one_eq, MeasureTheory.condExpL2_comp_continuousLinearMap, MeasureTheory.Lp.coeFn_star, MeasureTheory.L2.eLpNorm_rpow_two_norm_lt_top, MeasureTheory.condExpL2_const_inner, coeFn_fourierLp, MeasureTheory.Lp_toLp_restrict_smul, ContinuousLinearMap.coeFn_holder, MeasureTheory.setToFun_toL1, MeasureTheory.condExpL2_indicator_nonneg, MeasureTheory.MemLp.eLpNorm_mk_lt_top, MeasureTheory.Lp.mul_meas_ge_le_pow_enorm, coeFn_pair, MeasureTheory.Lp.norm_def, coeFn_one, ContinuousLinearMap.coeFn_compLp', MeasureTheory.lpMeas.aestronglyMeasurable, MeasureTheory.L1.norm_eq_integral_norm
|
comp 📖 | CompOp | 8 mathmath: coeFn_comp, comp_eq_mk, comp_comp, comp_mk, comp_id, comp_compQuasiMeasurePreserving, comp₂_eq_pair, comp_toGerm
|
compMeasurable 📖 | CompOp | 5 mathmath: compMeasurable_mk, compMeasurable_toGerm, coeFn_compMeasurable, comp₂Measurable_eq_pair, compMeasurable_eq_mk
|
compMeasurePreserving 📖 | CompOp | 8 mathmath: compMeasurePreserving_mem_Lp, MeasureTheory.Lp.compMeasurePreservingₗᵢ_apply_coe, compMeasurePreserving_mk, compMeasurePreserving_eq_mk, coeFn_compMeasurePreserving, eLpNorm_compMeasurePreserving, compMeasurePreserving_toGerm, MeasureTheory.Lp.compMeasurePreserving_val
|
compQuasiMeasurePreserving 📖 | CompOp | 5 mathmath: compQuasiMeasurePreserving_eq_mk, coeFn_compQuasiMeasurePreserving, compQuasiMeasurePreserving_toGerm, comp_compQuasiMeasurePreserving, compQuasiMeasurePreserving_mk
|
comp₂ 📖 | CompOp | 5 mathmath: coeFn_comp₂, comp₂_mk_mk, comp₂_eq_mk, comp₂_toGerm, comp₂_eq_pair
|
comp₂Measurable 📖 | CompOp | 5 mathmath: comp₂Measurable_toGerm, coeFn_comp₂Measurable, comp₂Measurable_eq_mk, comp₂Measurable_eq_pair, comp₂Measurable_mk_mk
|
const 📖 | CompOp | 8 mathmath: QuasiErgodic.eq_const_of_compQuasiMeasurePreserving_eq, coeFn_const, Ergodic.eq_const_of_compMeasurePreserving_eq, DomAddAct.vadd_aeeqFun_const, MeasureTheory.Lp.const_mem_Lp, coeFn_const_eq, DomMulAct.smul_aeeqFun_const, MeasureTheory.Lp.const_val
|
instAdd 📖 | CompOp | 5 mathmath: lintegral_add, coeFn_add, mk_add_mk, Integrable.add, add_toGerm
|
instAddCommGroup 📖 | CompOp | 68 mathmath: MeasureTheory.Lp.instIsScalarTower, DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_1, MeasureTheory.norm_condExpL2_le, MeasureTheory.Lp.instIsOrderedAddMonoid, MeasureTheory.inner_condExpL2_left_eq_right, MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero, ContinuousMap.range_toLp, ContinuousLinearMap.smul_compLp, MeasureTheory.Lp.compMeasurePreservingₗ_apply, MeasureTheory.MemLp.condExpL2_ae_eq_condExp, MeasureTheory.aestronglyMeasurable_condExpL2, MeasureTheory.condExpL2_indicator_ae_eq_smul, ContinuousLinearMap.holderₗ_apply_apply, MeasureTheory.integral_condExpL2_eq, MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc, MeasureTheory.setIntegral_condExpL2_indicator, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, MeasureTheory.norm_condExpL2_coe_le, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable, MeasureTheory.mem_lpMeas_indicatorConstLp, MeasureTheory.lintegral_nnnorm_condExpL2_le, ContinuousLinearMap.holder_smul_left, MeasureTheory.Lp.coeFn_smul, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, MeasureTheory.Lp.constₗ_apply, DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_2, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, MeasureTheory.condExpL2_indicator_of_measurable, MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, ContinuousLinearMap.lpPairing_eq_integral, ContinuousLinearMap.holder_smul_right, MeasureTheory.condExpL1CLM_lpMeas, StrongDual.toLpₗ_apply, StrongDual.norm_toLpₗ_le, MeasureTheory.Lp.instIsCentralScalar, StrongDual.toLpₗ_of_not_memLp, MeasureTheory.integrable_condExpL2_of_isFiniteMeasure, MeasureTheory.integrable_condExpL2_indicator, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', MeasureTheory.Lp.simpleFunc.coe_smul, MeasureTheory.Lp.instSMulCommClass, MeasureTheory.lpTrimToLpMeas_ae_eq, MeasureTheory.Lp.smul_comm, MeasureTheory.Lp.simpleFunc.toLp_smul, MeasureTheory.inner_condExpL2_eq_inner_fun, MeasureTheory.mem_lpMeas_self, MeasureTheory.Lp.coe_LpSubmodule, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, MeasureTheory.Lp.smul_assoc, MeasureTheory.lpMeasToLpTrim_ae_eq, MeasureTheory.eLpNorm_condExpL2_le, MeasureTheory.lpMeasToLpTrim_smul, MeasureTheory.condExpIndSMul_ae_eq_smul, ContinuousLinearMap.norm_holderL_le, MeasureTheory.lpMeas.ae_fin_strongly_measurable', ContinuousLinearMap.holderL_apply_apply, BoundedContinuousFunction.range_toLp, MeasureTheory.lpMeasToLpTrimLie_symm_toLp, MeasureTheory.MemLp.toLp_const_smul, MeasureTheory.norm_condExpL2_le_one, MeasureTheory.condExpL2_comp_continuousLinearMap, MeasureTheory.condExpL2_const_inner, MeasureTheory.Lp_toLp_restrict_smul, MeasureTheory.condExpL2_indicator_nonneg, MeasureTheory.lpMeas.aestronglyMeasurable
|
instAddCommMonoid 📖 | CompOp | — |
instAddGroup 📖 | CompOp | 556 mathmath: SchwartzMap.norm_toLp_le_seminorm, MeasureTheory.L1.setToL1_eq_setToL1', MeasureTheory.Lp.instHasSolidNorm, MeasureTheory.integrable_indicatorConstLp, ContinuousMap.toLp_inj, MeasureTheory.Lp.toTemperedDistributionCLM_apply, MeasureTheory.LpToLpRestrictCLM_coeFn, MeasureTheory.L1.SimpleFunc.norm_Integral_le_one, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm'', MeasureTheory.condExpInd_of_measurable, MeasureTheory.Lp.mul_meas_ge_le_pow_enorm', MeasureTheory.condExpL1_smul, MeasureTheory.Lp.instIsScalarTower, DomAddAct.mk_vadd_indicatorConstLp, MeasureTheory.aestronglyMeasurable_condExpInd, MeasureTheory.mem_lpMeasSubgroup_iff_aestronglyMeasurable, ContinuousLinearMap.integral_compLp, MeasureTheory.norm_indicatorConstLp_le, MeasureTheory.condExpInd_ae_eq_condExpIndSMul, MeasureTheory.L1.setToL1_indicatorConstLp, MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left, DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_1, UnitAddTorus.coe_mFourierBasis, SchwartzMap.inner_fourier_toL2_eq, SchwartzMap.toLp_fourierTransformInv_eq, MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral, MeasureTheory.Lp.mem_Lp_of_ae_bound, MeasureTheory.tendsto_condExpL1_of_dominated_convergence, MeasureTheory.Lp.const_smul_mem_Lp, MeasureTheory.norm_condExpL2_le, MeasureTheory.Lp.instIsOrderedAddMonoid, MeasureTheory.MemLp.toLp_val, MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_eLpNorm, ContinuousLinearMap.continuous_integral_comp_L1, MeasureTheory.Lp.edist_def, MeasureTheory.L1.norm_setToL1_le, MeasureTheory.inner_condExpL2_left_eq_right, ContinuousMap.toLp_denseRange, MeasureTheory.Lp.coeFn_add, ContinuousLinearMap.comp_memLp, MeasureTheory.Lp.eq_zero_iff_ae_eq_zero, MeasureTheory.Lp.ext_iff, ContinuousLinearMap.norm_compLp_le, MeasureTheory.Lp.indicatorConstLp_compMeasurePreserving, MeasureTheory.Lp.coeFn_const, MeasureTheory.norm_setToFun_le_mul_norm', LipschitzWith.lipschitzWith_compLp, MeasureTheory.norm_indicatorConstLp, ContinuousMap.range_toLp, MeasureTheory.L1.ofReal_norm_eq_lintegral, MeasureTheory.condExpIndL1Fin_smul, MeasureTheory.Lp.dist_def, MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.L1.SimpleFunc.setToL1SCLM_const, MeasureTheory.lpMeasSubgroupToLpTrim_neg, MeasureTheory.Lp.simpleFunc.uniformContinuous, MeasureTheory.Lp.memLp, MeasureTheory.Lp.nnnorm_def, MeasureTheory.Integrable.toL1_zero, MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq, MeasureTheory.condExpIndL1_add, MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM, MeasureTheory.norm_indicatorConstLp_top, MeasureTheory.L1.integral_smul, MeasureTheory.Lp.instFourierInvSMul, ContinuousLinearMap.smul_compLp, MeasureTheory.L2.inner_def, MeasureTheory.Lp.enorm_toLp, SchwartzMap.toLpCLM_apply, MeasureTheory.condExpIndL1Fin_add, MeasureTheory.Lp.compMeasurePreservingₗ_apply, ContinuousMap.toLp_norm_le, MeasureTheory.condExpL1_measure_zero, SchwartzMap.inner_toL2_toL2_eq, integrable_iff_mem_L1, MeasureTheory.Lp.simpleFunc.isDenseEmbedding, MeasureTheory.L1.SimpleFunc.norm_setToL1S_le, MeasureTheory.MemLp.condExpL2_ae_eq_condExp, DomMulAct.smul_Lp_sub, MeasureTheory.L1.SimpleFunc.setToL1S_neg, SchwartzMap.toLp_fourierInv_eq, MeasureTheory.continuous_condExpIndL1, MeasureTheory.Lp.nnnorm_eq_zero_iff, MeasureTheory.dominatedFinMeasAdditive_condExpInd, MeasureTheory.L1.SimpleFunc.integral_add, MeasureTheory.Integrable.edist_toL1_zero, MeasureTheory.Lp.finStronglyMeasurable, MeasureTheory.aestronglyMeasurable_condExpL2, MeasureTheory.L1.setToL1_smul_left, MeasureTheory.L1.setToL1_zero_left, MeasureTheory.condExpInd_nonneg, MeasureTheory.condExpL1_of_aestronglyMeasurable', MeasureTheory.L1.continuous_integral, MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.L1.integrable_coeFn, SchwartzMap.injective_toLp, MeasureTheory.condExpL2_indicator_ae_eq_smul, UnitAddTorus.mFourierCoeff_toLp, MeasureTheory.Lp.dist_edist, ContinuousLinearMap.holderₗ_apply_apply, MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left', MeasureTheory.Lp.coeFn_mk, MeasureTheory.Lp.norm_zero, MeasureTheory.Lp.mem_Lp_of_ae_nnnorm_bound, MeasureTheory.continuous_setToFun, MeasureTheory.Lp.simpleFunc.sub_toSimpleFunc, MeasureTheory.L1.dist_eq_integral_dist, MeasureTheory.L1.norm_def, MeasureTheory.integral_condExpL2_eq, DomAddAct.instIsIsometricVAddSubtypeAEEqFunMemAddAddSubgroupLp, MeasureTheory.Lp.edist_toLp_toLp, orthonormal_fourier, MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc, MeasureTheory.setIntegral_condExpL2_indicator, MeasureTheory.L1.SimpleFunc.integral_eq_norm_posPart_sub, MeasureTheory.Integrable.norm_toL1, ContinuousLinearMap.setIntegral_compLp, MeasureTheory.Lp.edist_toLp_zero, MeasureTheory.L1.setToL1_mono_left', DomAddAct.vadd_Lp_add, MeasureTheory.Integrable.toL1_eq_mk, MeasureTheory.condExpIndSMul_empty, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, MeasureTheory.setIntegral_condExpInd, MeasureTheory.edist_indicatorConstLp_eq_enorm, MeasureTheory.L1.setToL1_eq_setToL1SCLM, MeasureTheory.norm_condExpL2_coe_le, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable, MeasureTheory.aestronglyMeasurable_condExpL1, SchwartzMap.norm_fourier_toL2_eq, MeasureTheory.Lp.boundedContinuousFunction_topologicalClosure, MeasureTheory.Lp.SecondCountableTopology, MeasureTheory.Lp.instCompleteSpace, MeasureTheory.Lp.norm_toLp, MeasureTheory.Lp.instFourierPair, MeasureTheory.L1.integral_def, BoundedContinuousFunction.Lp_nnnorm_le, DomMulAct.edist_smul_Lp, hasSum_fourier_series_L2, MeasureTheory.L1.SimpleFunc.setToL1S_smul_real, BoundedContinuousFunction.range_toLpHom, BoundedContinuousFunction.toLp_inj, MeasureTheory.mem_lpMeas_indicatorConstLp, BoundedContinuousFunction.toLp_injective, MeasureTheory.integral_indicatorConstLp, MeasureTheory.Lp.coeFn_compMeasurePreserving, MeasureTheory.condExpIndSMul_smul, MeasureTheory.lintegral_nnnorm_condExpL2_le, StrongDual.toLp_of_not_memLp, MeasureTheory.Lp.compMeasurePreservingₗᵢ_apply_coe, MeasureTheory.L1.setToFun_eq_setToL1, SchwartzMap.norm_fourierTransformCLM_toL2_eq, MeasureTheory.enorm_indicatorConstLp_le, MeasureTheory.Lp.norm_neg, coeFn_abs, MeasureTheory.L1.integral_eq_setToL1, MeasureTheory.Integrable.toL1_smul, MeasureTheory.Lp.nnnorm_neg, ContinuousLinearMap.holder_smul_left, MeasureTheory.Lp.coeFn_smul, DomMulAct.mk_smul_toLp, MeasureTheory.condExpL1CLM_indicatorConstLp, MeasureTheory.L1.setToL1_add_left', MeasureTheory.L1.SimpleFunc.coe_negPart, MeasureTheory.integrableOn_Lp_of_measure_ne_top, MeasureTheory.L1.setToL1_mono_left, MeasureTheory.Lp.dist_eq_norm, MeasureTheory.condExpInd_disjoint_union, MeasureTheory.Lp.coeFn_le, MeasureTheory.Lp.simpleFunc.add_toSimpleFunc, UnitAddTorus.coeFn_mFourierLp, MeasureTheory.setIntegral_condExpIndSMul, MeasureTheory.indicatorConstLp_univ, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, MeasureTheory.norm_setToFun_le', MeasureTheory.Lp.norm_const_le, MeasureTheory.Lp.coeFn_negPart_eq_max, MeasureTheory.condExpL1_undef, MeasureTheory.Lp.nnnorm_toLp, MeasureTheory.Measure.MeasureDense.indicatorConstLp_subset_closure, MeasureTheory.L1.SimpleFunc.setToL1S_sub, ContinuousMap.toLp_def, MeasureTheory.L2.integral_inner_eq_sq_eLpNorm, MeasureTheory.L2.inner_indicatorConstLp_one, MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp, MeasureTheory.L1.setToL1_smul_left', MeasureTheory.Lp.boundedContinuousFunction_dense, MeasureTheory.Lp.constₗ_apply, MeasureTheory.Lp.coe_nnnorm, MeasureTheory.L1.SimpleFunc.toLp_one_eq_toL1, MeasureTheory.Lp.mem_boundedContinuousFunction_iff, DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_2, MeasureTheory.condExpIndSMul_add, MeasureTheory.Lp.norm_fourier_eq, SchwartzMap.coeFn_toLp, MeasureTheory.Lp.instFourierSMul, MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left, MeasureTheory.Lp.simpleFunc.toLp_eq_toLp, MeasureTheory.Lp.norm_const', MeasureTheory.norm_condExpIndL1_le, SchwartzMap.norm_toLp, MeasureTheory.condExpL1_add, MeasureTheory.Lp.smul_zero, MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul, DomMulAct.mk_smul_indicatorConstLp, MeasureTheory.norm_condExpInd_apply_le, ContinuousLinearMap.nnnorm_holder_apply_apply_le, DomAddAct.norm_vadd_Lp, MeasureTheory.condExpL1_neg, MeasureTheory.Lp.instTrivialStarSubtypeAEEqFunMemAddSubgroup, MeasureTheory.L1.nnnorm_integral_le, MeasureTheory.Lp.norm_smul_le, MeasureTheory.isClosed_aestronglyMeasurable, MeasureTheory.Lp.coeFn_sup, MeasureTheory.Lp_toLp_restrict_add, MeasureTheory.setIntegral_condExpL1, MeasureTheory.condExpIndL1_smul, UnitAddTorus.orthonormal_mFourier, ContinuousMap.toLp_norm_eq_toLp_norm_coe, MeasureTheory.Integrable.enorm_toL1, MeasureTheory.continuous_integral_integral, fourierCoeff_toLp, coe_fourierBasis, MeasureTheory.lpMeasSubgroupToLpTrim_sub, MeasureTheory.Integrable.toL1_sub, MeasureTheory.MemLp.toLp_neg, ProbabilityTheory.Kernel.continuous_integral_integral, DomMulAct.smul_Lp_neg, MeasureTheory.L2.real_inner_indicatorConstLp_one_indicatorConstLp_one, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, MeasureTheory.Lp.simpleFunc.denseRange, MeasureTheory.memL1_smul_of_L1_withDensity, MeasureTheory.condExp_ae_eq_condExpL1, MeasureTheory.condExpIndL1_smul', BoundedContinuousFunction.mem_Lp, MeasureTheory.lpMeasSubgroupToLpTrim_right_inv, BoundedContinuousFunction.Lp_norm_le, DomAddAct.vadd_Lp_ae_eq, MeasureTheory.Lp.norm_constL_le, MeasureTheory.Lp.simpleFunc.neg_toSimpleFunc, DomMulAct.norm_smul_Lp, MeasureTheory.condExpL2_indicator_of_measurable, MeasureTheory.Lp.add_smul, MeasureTheory.setIntegral_condExpL1CLM_of_measure_ne_top, MeasureTheory.condExp_ae_eq_condExpL1CLM, DomAddAct.vadd_Lp_sub, BoundedContinuousFunction.coeFn_toLp, MeasureTheory.Integrable.toL1_smul', UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, MeasureTheory.Lp.instContinuousVAddDomAddAct, MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le', MeasureTheory.condExpL1CLM_indicatorConst, MeasureTheory.mem_lpMeasSubgroup_toLp_of_trim, MeasureTheory.L1.nnnorm_Integral_le_one, MeasureTheory.lpMeasSubgroupToLpTrim_add, MeasureTheory.L1.integral_eq_norm_posPart_sub, MeasureTheory.Lp.instContinuousFourierInv, UnitAddTorus.hasSum_mFourier_series_L2, MeasureTheory.Lp.norm_const, MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace, MeasureTheory.lpMeasSubgroupToLpTrim_left_inv, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, MeasureTheory.Lp.instAddLeftMono, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left, ContinuousLinearMap.lpPairing_eq_integral, MeasureTheory.Lp.simpleFunc.norm_toSimpleFunc, ContinuousLinearMap.holder_smul_right, MeasureTheory.L2.eLpNorm_inner_lt_top, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left', MeasureTheory.condExpL1CLM_lpMeas, MeasureTheory.Lp.mem_Lp_iff_memLp, StrongDual.toLpₗ_apply, MeasureTheory.L1.setToL1_apply_coeToLp, MeasureTheory.Lp.const_mem_Lp, MeasureTheory.indicatorConstLp_add, MeasureTheory.L1.setToL1_congr_left', DomAddAct.vadd_Lp_neg, MeasureTheory.Lp.simpleFunc.coeFn_le, MeasureTheory.Lp.instFourierPairInv, MeasureTheory.Lp.simpleFunc.toLp_zero, MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner, MeasureTheory.L1.SimpleFunc.integralCLM'_L1_eq_integral, MeasureTheory.Lp.coeFn_nonneg, MeasureTheory.nnnorm_indicatorConstLp_le, DomMulAct.dist_smul_Lp, MeasureTheory.Lp.instFourierInvAdd, MeasureTheory.L1.setToL1_congr_left, MeasureTheory.L1.setToL1_smul, MeasureTheory.Lp.coeFn_lpSMul, MeasureTheory.Lp.simpleFunc.coeFn_zero, MeasureTheory.condExpIndSMul_nonneg, MeasureTheory.L1.dist_def, ContinuousLinearMap.coeFn_compLpL, StrongDual.norm_toLpₗ_le, MeasureTheory.Lp.coe_mk, MeasureTheory.Lp.instIsCentralScalar, MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left', MeasureTheory.L1.norm_integral_le, MeasureTheory.setIntegral_indicatorConstLp, ProbabilityTheory.Kernel.continuous_integral_integral_comp, ContinuousMap.toLp_injective, StrongDual.toLpₗ_of_not_memLp, MeasureTheory.indicatorConstLp_sub, DomAddAct.edist_vadd_Lp, MeasureTheory.L1.aemeasurable_coeFn, MeasureTheory.integrable_condExpL2_of_isFiniteMeasure, MeasureTheory.condExpIndL1Fin_disjoint_union, MeasureTheory.Lp.instIsBoundedSMul, ContinuousMap.coe_toLp, DomMulAct.instIsIsometricSMulSubtypeAEEqFunMemAddSubgroupLp, MeasureTheory.Lp.antitone, ContinuousLinearMap.integral_comp_L1_comm, span_fourierLp_closure_eq_top, MeasureTheory.L1.measurable_coeFn, MeasureTheory.aestronglyMeasurable_condExpL1CLM, SchwartzMap.inner_fourierTransformCLM_toL2_eq, MeasureTheory.continuous_integral, MeasureTheory.Lp.simpleFunc.isBoundedSMul, MeasureTheory.Lp.coe_posPart, MeasureTheory.integrable_condExpL2_indicator, MeasureTheory.Lp.zero_smul, DomMulAct.smul_Lp_zero, DomAddAct.mk_vadd_toLp, MeasureTheory.lpMeasSubgroupToLpTrim_norm_map, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', MeasureTheory.Lp.completeSpace_lp_of_cauchy_complete_eLpNorm, MeasureTheory.Lp.simpleFunc.toLp_sub, MeasureTheory.Lp.simpleFunc.coe_smul, MeasureTheory.Lp.smul_def, MeasureTheory.Lp.norm_exponent_zero, MeasureTheory.Lp.smul_neg, MeasureTheory.L1.stronglyMeasurable_coeFn, ContinuousMap.coeFn_toLp, MeasureTheory.L1.norm_setToL1_le_mul_norm', ProbabilityTheory.condVar_of_sigmaFinite, MeasureTheory.Lp.instSMulCommClass, MeasureTheory.Lp.simpleFunc.toLp_neg, MeasureTheory.L1.SimpleFunc.integral_smul, MeasureTheory.L2.inner_indicatorConstLp_one_indicatorConstLp_one, MeasureTheory.lpTrimToLpMeas_ae_eq, DomAddAct.vadd_Lp_const, MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le, ContinuousMap.toLp_comp_toContinuousMap, MeasureTheory.Lp.smul_comm, SchwartzMap.continuous_toLp, MeasureTheory.isComplete_aestronglyMeasurable, MeasureTheory.Lp.simpleFunc.isUniformEmbedding, MeasureTheory.L1.integral_of_fun_eq_integral, MeasureTheory.L1.integral_zero, SchwartzMap.toLp_fourierTransform_eq, MeasureTheory.setLIntegral_nnnorm_condExpIndSMul_le, MeasureTheory.continuous_indicatorConstLp_set, MeasureTheory.condExpIndL1_of_not_measurableSet, MeasureTheory.Lp.smul_add, MeasureTheory.L1.norm_setToL1_le', MeasureTheory.withDensitySMulLI_apply, MeasureTheory.Lp.fourierInv_toTemperedDistribution_eq, UnitAddTorus.hasSum_prod_mFourierCoeff, DomMulAct.smul_Lp_ae_eq, MeasureTheory.Lp.simpleFunc.isUniformInducing, MeasureTheory.L1.norm_of_fun_eq_integral_norm, MeasureTheory.L1.integral_add, MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top, MeasureTheory.aestronglyMeasurable_condExpIndSMul, MeasureTheory.Lp.constL_apply, MeasureTheory.L2.mem_L1_inner, MeasureTheory.L1.integral_eq_integral, DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp, MeasureTheory.Integrable.coeFn_toL1, MeasureTheory.Lp.simpleFunc.coe_indicatorConst, MeasureTheory.condExpIndL1_disjoint_union, ContinuousLinearMap.add_compLp, MeasureTheory.Lp.inner_fourier_eq, MeasureTheory.Integrable.norm_toL1_eq_lintegral_norm, MeasureTheory.L1.aestronglyMeasurable_coeFn, MeasureTheory.condExpInd_smul', MeasureTheory.L1.setToL1_add_left, MeasureTheory.Lp.eLpNorm_lt_top, MeasureTheory.L2.integrable_inner, BoundedContinuousFunction.toLp_norm_le, MeasureTheory.Lp.continuous_negPart, MeasureTheory.Lp.coeFn_negPart, MeasureTheory.condExp_of_sigmaFinite, MeasureTheory.norm_setToFun_le_mul_norm, MeasureTheory.L1.SimpleFunc.norm_eq_integral, MeasureTheory.condExpIndL1_of_measure_eq_top, MeasureTheory.L1.SimpleFunc.norm_integral_le_norm, MeasureTheory.Lp.simpleFunc.toLp_smul, MeasureTheory.L1.norm_setToL1_le_mul_norm, MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left', MeasureTheory.Lp.neg_smul, MeasureTheory.Lp.instOrderClosedTopologySubtypeAEEqFunMemAddSubgroupOfClosedIciTopology, MeasureTheory.norm_condExpInd_le, MeasureTheory.setToFun_mono_left, MeasureTheory.MemLp.toLp_add, StrongDual.toLp_apply, MeasureTheory.Lp.coeFn_zero, MeasureTheory.mem_lpMeas_self, MeasureTheory.norm_Lp_toLp_restrict_le, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, hasSum_sq_fourierCoeff, ContinuousLinearMap.holder_add_right, MeasureTheory.Lp.enorm_def, MeasureTheory.condExpInd_disjoint_union_apply, ContinuousLinearMap.add_compLpL, MeasureTheory.L1.setToL1_simpleFunc_indicatorConst, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm', MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left, UnitAddTorus.mFourierBasis_repr, MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul, MeasureTheory.Lp.norm_measure_zero, MeasureTheory.tendsto_indicatorConstLp_set, LipschitzWith.coeFn_compLp, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, fourierBasis_repr, MeasureTheory.L1.setToL1_zero_left', MeasureTheory.BoundedContinuousFunction.inner_toLp, MeasureTheory.condExpL1_mono, MeasureTheory.Lp.coeFn_neg, MeasureTheory.L1.norm_Integral_le_one, MeasureTheory.Lp.toLp_compMeasurePreserving, MeasureTheory.Lp.coeFn_abs, MeasureTheory.Lp.norm_eq_zero_iff, MeasureTheory.Lp.coeFn_sub, MeasureTheory.Lp.meas_ge_le_mul_pow_enorm, UnitAddTorus.hasSum_sq_mFourierCoeff, ContinuousLinearMap.coeFn_compLp, DomMulAct.nnnorm_smul_Lp, MeasureTheory.lintegral_nnnorm_condExpIndSMul_le, LipschitzWith.continuous_compLp, MeasureTheory.Lp.smul_assoc, MeasureTheory.integrable_condExpIndSMul, MeasureTheory.Lp.toTemperedDistribution_apply, LipschitzWith.compLp_zero, MeasureTheory.condExpL1_zero, MeasureTheory.Lp.compMeasurePreserving_continuous, MeasureTheory.Lp.coeFn_posPart, MeasureTheory.L1.SimpleFunc.setToL1S_add, MeasureTheory.L1.norm_sub_eq_lintegral, MeasureTheory.norm_indicatorConstLp', MeasureTheory.Lp.neg_smul_neg, MeasureTheory.isometry_lpMeasSubgroupToLpTrim, MeasureTheory.integrable_condExpL1, ContinuousLinearMap.smul_compLpL, MeasureTheory.Integrable.toL1_add, ContinuousLinearMap.norm_compLpL_le, DomMulAct.smul_Lp_const, MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left, MeasureTheory.setIntegral_condExpL1CLM, MeasureTheory.L1.hasFiniteIntegral_coeFn, tsum_sq_fourierCoeff, MeasureTheory.lpMeasToLpTrim_ae_eq, MeasureTheory.eLpNorm_condExpL2_le, MeasureTheory.L1.integral_eq', MeasureTheory.lpMeasToLpTrim_smul, MeasureTheory.Lp.simpleFunc.denseRange_coeSimpleFuncNonnegToLpNonneg, MeasureTheory.condExpIndSMul_ae_eq_smul, MeasureTheory.Lp.simpleFunc.isDenseInducing, MeasureTheory.Lp.dense_hasCompactSupport_contDiff, ContinuousLinearMap.norm_holderL_le, MeasureTheory.lpMeas.ae_fin_strongly_measurable', MeasureTheory.L1.setToL1'_eq_setToL1SCLM, MeasureTheory.condExpIndSMul_smul', MeasureTheory.condExpL1_sub, MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace, MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq, MeasureTheory.L1.integral_sub, MeasureTheory.L1.ofReal_norm_sub_eq_lintegral, MeasureTheory.Lp.coeFn_inf, MeasureTheory.ContinuousMap.inner_toLp, MeasureTheory.L1.SimpleFunc.integral_L1_eq_integral, MeasureTheory.Lp.simpleFunc.toLp_eq_mk, DomAddAct.dist_vadd_Lp, ContinuousLinearMap.holderL_apply_apply, MeasureTheory.Lp.instContinuousFourier, DomAddAct.vadd_Lp_zero, MeasureTheory.condExpInd_empty, MeasureTheory.condExpL1CLM_smul, LipschitzWith.norm_compLp_le, MeasureTheory.L1.edist_def, MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun, MeasureTheory.continuous_setIntegral, MeasureTheory.MemLp.toLp_zero, UnitAddTorus.span_mFourierLp_closure_eq_top, MeasureTheory.Lp.pow_mul_meas_ge_le_enorm, MeasureTheory.condExpIndL1Fin_smul', ContinuousLinearMap.norm_holder_apply_apply_le, MeasureTheory.Lp.edist_dist, BoundedContinuousFunction.range_toLp, MeasureTheory.indicatorConstLp_disjoint_union, MeasureTheory.L1.integral_eq, MeasureTheory.indicatorConstLp_coeFn, MeasureTheory.Lp.fourier_toTemperedDistribution_eq, MeasureTheory.Lp.const_val, MeasureTheory.Lp.simpleFunc.coeFn_nonneg, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp, MeasureTheory.L1.setToL1'_apply_coeToLp, SchwartzMap.denseRange_toLpCLM, SchwartzMap.toLp_fourier_eq, DomMulAct.smul_Lp_val, DomAddAct.nnnorm_vadd_Lp, MeasureTheory.L1.setToL1_const, MeasureTheory.norm_condExpIndL1Fin_le, MeasureTheory.lpMeasToLpTrimLie_symm_toLp, MeasureTheory.continuous_L1_toL1, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm, MeasureTheory.indicatorConstLp_empty, MeasureTheory.Integrable.edist_toL1_toL1, MeasureTheory.MemLp.toLp_const_smul, MeasureTheory.L1.setToL1_lipschitz, MeasureTheory.Integrable.toL1_neg, MeasureTheory.norm_condExpL2_le_one, MeasureTheory.setToFun_eq, MeasureTheory.condExpL2_comp_continuousLinearMap, MeasureTheory.Lp.coeFn_star, MeasureTheory.L2.eLpNorm_rpow_two_norm_lt_top, ContinuousLinearMap.holder_add_left, MeasureTheory.dist_indicatorConstLp_eq_norm, LipschitzWith.norm_compLp_sub_le, MeasureTheory.Lp.simpleFunc.toLp_add, BoundedContinuousFunction.toLp_denseRange, MeasureTheory.condExpL2_const_inner, MeasureTheory.Lp.isometry_compMeasurePreserving, coeFn_fourierLp, MeasureTheory.Lp.simpleFunc.dense, MeasureTheory.Lp.instFourierAdd, MeasureTheory.Lp.simpleFunc.zero_toSimpleFunc, MeasureTheory.norm_setToFun_le, MeasureTheory.Lp.toTemperedDistribution_smul_eq, MeasureTheory.Lp_toLp_restrict_smul, MeasureTheory.condExpL1_eq, DomAddAct.vadd_Lp_val, MeasureTheory.L1.SimpleFunc.coe_posPart, MeasureTheory.Lp.compMeasurePreserving_val, ContinuousLinearMap.coeFn_holder, MeasureTheory.Lp.instContinuousSMulDomMulAct, MeasureTheory.Lp.norm_compMeasurePreserving, MeasureTheory.Lp.nnnorm_zero, MeasureTheory.setToFun_toL1, MeasureTheory.condExpL2_indicator_nonneg, MeasureTheory.L1.integral_neg, MeasureTheory.MemLp.toLp_sub, MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left', MeasureTheory.Lp.mul_meas_ge_le_pow_enorm, MeasureTheory.Lp.simpleFunc.norm_toLp, DomMulAct.smul_Lp_add, MeasureTheory.Lp.continuous_posPart, MeasureTheory.Lp.norm_def, ContinuousLinearMap.coeFn_compLp', MeasureTheory.MemLp.toLp_const, MeasureTheory.lpMeas.aestronglyMeasurable, MeasureTheory.L1.SimpleFunc.setToL1S_smul, MeasureTheory.L1.norm_eq_integral_norm
|
instAddMonoid 📖 | CompOp | 1 mathmath: toGermAddMonoidHom_apply
|
instCoeFun 📖 | CompOp | — |
instCommGroup 📖 | CompOp | — |
instCommMonoid 📖 | CompOp | — |
instDistribMulAction 📖 | CompOp | — |
instDiv 📖 | CompOp | 3 mathmath: div_toGerm, mk_div, coeFn_div
|
instGroup 📖 | CompOp | — |
instInf 📖 | CompOp | 4 mathmath: coeFn_inf, inf_le_left, inf_le_right, le_inf
|
instInhabited 📖 | CompOp | — |
instInv 📖 | CompOp | 3 mathmath: inv_mk, coeFn_inv, inv_toGerm
|
instInvolutiveStarOfContinuousStar 📖 | CompOp | — |
instLattice 📖 | CompOp | 1 mathmath: coeFn_abs
|
instModule 📖 | CompOp | 1 mathmath: MeasureTheory.Lp.coe_LpSubmodule
|
instMonoid 📖 | CompOp | 1 mathmath: toGermMonoidHom_apply
|
instMul 📖 | CompOp | 3 mathmath: coeFn_mul, mul_toGerm, mk_mul_mk
|
instMulAction 📖 | CompOp | — |
instNeg 📖 | CompOp | 4 mathmath: neg_toGerm, coeFn_neg, neg_mk, Integrable.neg
|
instOne 📖 | CompOp | 4 mathmath: one_toGerm, one_def, coeFn_one_eq, coeFn_one
|
instPartialOrder 📖 | CompOp | 1 mathmath: MeasureTheory.Lp.instIsOrderedAddMonoid
|
instPowInt 📖 | CompOp | 3 mathmath: mk_zpow, zpow_toGerm, coeFn_zpow
|
instPowNat 📖 | CompOp | 3 mathmath: pow_toGerm, coeFn_pow, mk_pow
|
instPreorder 📖 | CompOp | 14 mathmath: mk_le_mk, MeasureTheory.condExpInd_nonneg, coeFn_le, inf_le_left, inf_le_right, MeasureTheory.Lp.coeFn_le, MeasureTheory.Lp.instAddLeftMono, MeasureTheory.Lp.simpleFunc.coeFn_le, MeasureTheory.Lp.coeFn_nonneg, le_sup_right, MeasureTheory.Lp.instOrderClosedTopologySubtypeAEEqFunMemAddSubgroupOfClosedIciTopology, le_sup_left, MeasureTheory.Lp.simpleFunc.denseRange_coeSimpleFuncNonnegToLpNonneg, MeasureTheory.Lp.simpleFunc.coeFn_nonneg
|
instSMul 📖 | CompOp | 10 mathmath: coeFn_smul, MeasureTheory.Lp.const_smul_mem_Lp, instSMulCommClass, instIsCentralScalar, smul_toGerm, Integrable.smul, smul_mk, DomMulAct.instSMulCommClassAEEqFun_1, instIsScalarTower, DomMulAct.instSMulCommClassAEEqFun
|
instStarOfContinuousStar 📖 | CompOp | 3 mathmath: coeFn_star, eLpNorm_star, instTrivialStar
|
instSub 📖 | CompOp | 4 mathmath: coeFn_sub, Integrable.sub, mk_sub, sub_toGerm
|
instSup 📖 | CompOp | 4 mathmath: sup_le, coeFn_sup, le_sup_right, le_sup_left
|
instZero 📖 | CompOp | 7 mathmath: lintegral_eq_zero_iff, lintegral_zero, coeFn_zero, zero_toGerm, coeFn_zero_eq, zero_def, integrable_zero
|
lintegral 📖 | CompOp | 6 mathmath: lintegral_mk, lintegral_coeFn, lintegral_add, lintegral_eq_zero_iff, lintegral_zero, lintegral_mono
|
mk 📖 | CompOp | — |
pair 📖 | CompOp | 5 mathmath: pair_eq_mk, comp₂_eq_pair, pair_mk_mk, comp₂Measurable_eq_pair, coeFn_pair
|
posPart 📖 | CompOp | 3 mathmath: MeasureTheory.Lp.coe_posPart, coeFn_posPart, posPart_mk
|
toGerm 📖 | CompOp | 22 mathmath: comp₂Measurable_toGerm, toGerm_injective, neg_toGerm, toGerm_eq, compMeasurable_toGerm, smul_toGerm, pow_toGerm, toGermMonoidHom_apply, one_toGerm, compQuasiMeasurePreserving_toGerm, comp₂_toGerm, sub_toGerm, toGermAddMonoidHom_apply, div_toGerm, mk_toGerm, mul_toGerm, zpow_toGerm, comp_toGerm, zero_toGerm, compMeasurePreserving_toGerm, inv_toGerm, add_toGerm
|
toGermAddMonoidHom 📖 | CompOp | 1 mathmath: toGermAddMonoidHom_apply
|
toGermMonoidHom 📖 | CompOp | 1 mathmath: toGermMonoidHom_apply
|