Documentation Verification Report

Measurable

📁 Source: Mathlib/Analysis/Calculus/LineDeriv/Measurable.lean

Statistics

MetricCount
DefinitionsMeasurable
1
Theoremsaemeasurable_lineDeriv, aemeasurable_lineDeriv_uncurry, aestronglyMeasurable_lineDeriv, aestronglyMeasurable_lineDeriv_uncurry, measurableSet_lineDifferentiableAt, measurableSet_lineDifferentiableAt_uncurry, measurable_lineDeriv, measurable_lineDeriv_uncurry, stronglyMeasurable_lineDeriv, stronglyMeasurable_lineDeriv_uncurry
10
Total11

(root)

Definitions

NameCategoryTheorems
Measurable 📖MathDef
402 mathmath: ProbabilityTheory.Kernel.measurable_rnDerivAux, MeasureTheory.IsPredictable.measurable_add_one, measurable_inl, MeasurableSet.mem, RCLike.measurable_ofReal, measurable_sigmaUncurry, measurable_from_top, Preorder.measurable_restrictLe, measurable_add_op, MeasurableSpace.measurable_invariants_dom, WithLp.measurable_ofLp, measurable_lineDeriv, MeasurableSup.measurable_const_sup, NumberField.mixedEmbedding.measurable_polarCoordReal_symm, measurable_subtype_coe, measurable_of_Iio, Real.measurable_sinh, measurable_deriv_with_param, measurable_to_nat, AEMeasurable.exists_ae_eq_range_subset, ProbabilityTheory.IsKolmogorovProcess.measurable, measurable_div_const', MeasurableAdd₂.measurable_add, MeasureTheory.measurable_restrict_cylinderEvents, measurable_ereal_toENNReal, measurable_norm, Complex.measurable_arg, EReal.measurable_exp, measurable_of_Ici, MeasureTheory.NullMeasurable.measurable', MeasureTheory.Measure.measurable_measure, measurable_of_Iic, measurable_update', ContinuousLinearMap.measurable, IsClosedEmbedding.measurable, measurable_pi_iff, MeasureTheory.Adapted.measurable, MeasurableDiv.measurable_div_const, HasCompactSupport.measurable_of_prod, measurable_ereal_toReal, Nat.measurable_floor, MeasureTheory.measurable_update_cylinderEvents, measurable_down, measurable_from_nat, measurable_neg_iff, MeasureTheory.measurable_uniqueElim_cylinderEvents, WithTop.measurable_coe, measurableSet_setOf, Probability.measurable_cauchyPDFReal, MeasureTheory.Measure.measurable_coe, UpperSemicontinuous.measurable, measurable_mul_op, measurable_fun_prod, MeasurableMul₂.measurable_mul, Finset.measurable_restrict, MeasureTheory.measurable_measure_add_right, Meromorphic.measurable, measurable_uncurry, Finset.measurable_restrict₂, ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux, ProbabilityTheory.Kernel.measurable_singularPart_fun_right, measurable_edist_right, MeasureTheory.ProbabilityMeasure.measurable_fun_prod, aemeasurable_iff_measurable, measurable_lt, Measurable.of_discrete, MeasurableAdd.measurable_const_add, ProbabilityTheory.IsRatCondKernelCDFAux.measurable, ProbabilityTheory.exists_hasLaw_indepFun, measurable_id, measurable_tProd_elim', ENNReal.measurable_toNNReal, measurable_mem, InformationTheory.measurable_klFun, ProbabilityTheory.measurable_condDistrib, MeasureTheory.measurable_measure_mul_right, WithLp.measurable_toLp, MeasureTheory.measurable_update_cylinderEvents_left, measurable_infEDist, MeasurableSup₂.measurable_sup, measurable_circleMap, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.Measure.singularPart_def, Measurable.of_le_map, ENat.measurable_iff, measurable_inr, MeasureTheory.StronglyMeasurable.enorm, Real.measurable_sinc, ContinuousLinearMap.measurable_apply₂, ENNReal.measurable_toReal, MeromorphicOn.measurable, Antitone.measurable, Complex.measurable_re, MeasureTheory.NullMeasurable.measurable_of_complete, ProbabilityTheory.Kernel.measurable_density, measurable_oneLePart, Real.measurable_cos, MeasurableNeg.measurable_neg, aeSeq.measurable, MeasureTheory.SimpleFunc.measurable, measurable_deriv, MeasurableMul.measurable_const_mul, measurable_tProd_elim, MeasurablePow.measurable_pow, measurable_eq_mp, Meromorphic.MeromorphicOn.measurable, Real.measurable_arctan, measurable_fract, measurableVAdd_iterateAddAct, MeasurableDiv₂.measurable_div, Nat.measurable_ceil, ProbabilityTheory.exists_iid, ProbabilityTheory.measurable_gaussianPDF, MeasurableConstVAdd.measurable_const_vadd, measurable_sigmaCurry, measurable_real_toNNReal, MeasurableSMul.measurable_smul_const, Measurable.of_comap_le, MeasurableEmbedding.measurable_rangeSplitting, ProbabilityTheory.Kernel.measurable_densityProcess, MeasurableSub₂.measurable_sub, unitInterval.measurable_symm, MeasurableEquiv.measurable_toFun, MeasurableVAdd₂.measurable_vadd, ProbabilityTheory.measurable_paretoPDFReal, MeasureTheory.measurable_pdf, MeasureTheory.exists_measurable_le_forall_setLIntegral_eq, Preorder.measurable_frestrictLe₂, measurable_const_vadd_iff, ProbabilityTheory.Kernel.measurable_rnDeriv, measurable_infEdist, RCLike.measurable_re, measurable_pi_apply, MeasurableInf.measurable_inf_const, measurableSMul₂_iterateMulAct, ProbabilityTheory.Kernel.measurable_densityProcess_left, ProbabilityTheory.measurable_countablePartitionSet_subtype, QuotientAddGroup.measurable_from_quotient, MeasurableSub.measurable_sub_const, ProbabilityTheory.measurable_gammaPDFReal, measurable_prodMk_right, MeasureTheory.StronglyAdapted.measurable_upcrossings, ProbabilityTheory.IsKolmogorovProcess.measurable_edist, measurable_update_left, WithTop.measurable_untopA, ProbabilityTheory.Kernel.measurable_countableFiltration_densityProcess, MeasureTheory.IsStoppingTime.measurable, MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral, stronglyMeasurable_iff_measurable_separable, MeasurableInf₂.measurable_inf, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left', Preorder.measurable_restrictLe₂, measurable_encard, ProbabilityTheory.measurable_preCDF, MeasurableSet.exists_measurable_proj, ProbabilityTheory.Kernel.measurable_trajFun, MeasurableInv.measurable_inv, ProbabilityTheory.Kernel.measurable_lintegral_indicator_const, measurable_indicator_const_iff, MeasureTheory.measurable_update_cylinderEvents', measurable_setOf, MeasureTheory.measurable_cylinderEvents_iff, MeasurableEquiv.measurable_invFun, measurable_intCast, Int.measurable_floor, Real.measurable_cosh, MeasureTheory.finStronglyMeasurable_iff_measurable, MeasurableSup.measurable_sup_const, Complex.measurable_cos, measurable_iff_comap_le, ProbabilityTheory.Kernel.measurable_singularPart_fun, measurable_measure_prodMk_left_finite, MeasureTheory.Measure.HaveLebesgueDecomposition.lebesgue_decomposition, Continuous.borel_measurable, VitaliFamily.limRatioMeas_measurable, measurable_updateFinset, Set.measurable_restrict₂, MeasureTheory.Adapted.measurable_le, ProbabilityTheory.measurable_preCDF', ProbabilityTheory.measurable_poissonPMFReal, measurable_const', MeasurableConstSMul.measurable_const_smul, measurable_up, ProbabilityTheory.Kernel.measurable_rnDeriv_right, measurable_IicProdIoc, measurable_tProd_mk, measurable_set_iff, ProbabilityTheory.IsCondKernelCDF.measurable, Complex.measurable_im, measurable_fderiv_apply_const, measurable_generateFrom, Complex.measurable_exp, measurable_coe_ennreal_ereal, Real.measurable_arccos, measurable_updateFinset_left, ProbabilityTheory.measurable_geometricPMFReal, ProbabilityTheory.measurable_countablePartitionSet, MeasureTheory.SignedMeasure.measurable_rnDeriv, MeasureTheory.measurable_cylinderEvent_apply, QuotientAddGroup.measurable_coe, measurable_of_isClosed, measurable_of_Ioi, measurableSMul_iterateMulAct, measurable_to_countable, MeasureTheory.IsStoppingTime.measurable', measurable_leOnePart, ContinuousLinearMap.measurable_apply, measurable_comap_iff, MeasurableVAdd.measurable_vadd_const, MeasurableInf.measurable_const_inf, MeasureTheory.Measure.rnDeriv_def, ProbabilityTheory.Kernel.measurable_densityProcess_aux, ProbabilityTheory.IsKolmogorovProcess.measurablePair, measurable_one, Real.measurable_arcsin, measurable_edist_left, MeasureTheory.Measure.measurable_dirac, measurable_swap, measurable_lineDeriv_uncurry, measurable_equivCurry_symm, measurable_to_prop, measurable_le, measurable_updateFinset', MeasureTheory.StronglyAdapted.measurable_upcrossingsBefore, measurable_measure_prodMk_left, measurable_of_isOpen, LowerSemicontinuous.measurable, comap_measurable, measurable_id'', ProbabilityTheory.IsMeasurableRatCDF.measurable_stieltjesFunction, MeasureTheory.AEEqFun.measurable, measurable_quot_mk, MeasureTheory.L1.measurable_coeFn, ProbabilityTheory.measurable_condExpKernel, measurable_inv_iff, measurable_zero, Complex.measurable_sinh, Set.measurable_restrict, MeasurableSMul₂.measurable_smul, measurable_from_quotient, measurable_snd, measurable_uniqueElim, measurable_of_countable, Real.measurable_exp, MeasurableMul.measurable_mul_const, ENNReal.measurable_log, ContinuousLinearMap.measurable_coe, measurable_enorm, MeasureTheory.FinStronglyMeasurable.measurable, measurable_set_mem, ProbabilityTheory.IsRatCondKernelCDFAux.measurable_right, RCLike.measurable_im, MeasureTheory.measurable_condLExp', MeasureTheory.measurable_condLExp, MeasurableEquiv.measurable_comp_iff, measurable_measure_prodMk_right, ENNReal.measurable_ofReal, measurable_of_finite, measurable_derivWithin_Ioi, measurable_coe_nnreal_real, MeasureTheory.MeasurePreserving.measurable, measurable_compl, measurable_coe_real_ereal, ProbabilityTheory.measurable_exponentialPDFReal, ProbabilityTheory.measurable_gaussianPDFReal, NumberField.mixedEmbedding.measurable_polarCoord_symm, Continuous.measurable, measurable_set_notMem, Complex.measurable_sin, measurable_negPart, ProbabilityTheory.Kernel.measurable_density_left, QuotientGroup.measurable_coe, measurable_smul_const, measurable_to_countable', measurable_of_isClosed', measurable_findGreatest, MeasureTheory.isPredictable_iff_measurable_add_one, MeasureTheory.measurable_llr, measurable_quotient_mk', MeasurableDiv.measurable_const_div, Measurable.map_prodMk_right, Preorder.measurable_frestrictLe, Int.measurable_ceil, Complex.measurable_log, AddCircle.measurable_mk', measurable_iff_le_map, measurable_fderiv_with_param, AEMeasurable.exists_measurable_nonneg, ProbabilityTheory.Kernel.measurable, measurable_id', BoundedContinuousFunction.measurable_coe_ennreal_comp, ProbabilityTheory.Kernel.measurable_coe, measurable_findGreatest', Real.measurable_sin, Complex.measurable_cosh, measurable_of_subsingleton_codomain, measurable_const, measurable_piEquivPiSubtypeProd_symm, measurable_natCast, QuotientGroup.measurable_from_quotient, Monotone.measurable, measurable_piCurry_symm, Real.measurable_log, ProbabilityTheory.measurable_measure_condCDF, ContinuousLinearMap.measurable_apply', stronglyMeasurable_iff_measurable, ProbabilityTheory.IsRatCondKernelCDF.measurable, MeasureTheory.Lp.simpleFunc.measurable, ProbabilityTheory.measurable_memPartitionSet_subtype, ProbabilityTheory.IsMeasurableRatCDF.measurable, measurable_nndist, MeasureTheory.exists_measurable_le_lintegral_eq, MeasurableEquiv.measurable, measurable_fderiv, MeasureTheory.condLExp_def, measurable_of_continuousOn_compl_singleton, measurable_infNndist, ProbabilityTheory.IsMeasurableRatCDF.measurable_measure_stieltjesFunction, IsUnit.measurable_const_smul_iff, MeasurableSpace.measurable_mapNatBool, ProbabilityTheory.Kernel.measurable_singularPart, MeasurableEmbedding.measurable_comp_iff, ProbabilityTheory.Kernel.measurable_densityProcess_right, measurable_limit_of_tendsto_metrizable_ae, measurable_of_empty_codomain, measurable_IocProdIoc, ProbabilityTheory.measurable_condCDF, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left_of_finite, ProbabilityTheory.Kernel.measurable', ContinuousOn.measurable_piecewise, ProbabilityTheory.measurable_betaPDFReal, Homeomorph.measurable, MeasurableEmbedding.measurable, ProbabilityTheory.measurable_partitionFiltration_memPartitionSet, measurable_add_unop, Complex.measurable_ofReal, measurable_mabs, MeasureTheory.exists_measurable_le_setLIntegral_eq_of_integrable, measurable_piCurry, measurable_edist, measurable_swap_iff, ContinuousMap.measurable, WithTop.measurable_untopD, MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated, ProbabilityTheory.Kernel.measurable_kernel_prodMk_right, MeasureTheory.Measure.measurable_rnDeriv, Measure.exists_hasLaw, MeasureTheory.FiniteMeasure.measurable_fun_prod, measurable_infDist, MeasureTheory.Measure.QuasiMeasurePreserving.measurable, measurable_derivWithin_Ici, IsAddUnit.measurable_const_vadd_iff, Measurable.map_prodMk_left, measurableSMul₂_iterateAddAct, MeasureTheory.IsStoppingTime.measurable_of_le, MeasureTheory.exists_measurable_le_withDensity_eq, measurable_equivCurry, MeasureTheory.measurable_charFun, measurable_of_empty, MeasurableEmbedding.measurable_invFun, Probability.measurable_cauchyPDF, measurable_coe_nnreal_ennreal, Subsingleton.measurable, measurable_find, measurable_fderiv_apply_const_with_param, ProbabilityTheory.Kernel.measurable_density_right, MeasurableAdd.measurable_add_const, ProbabilityTheory.Kernel.measurable_rnDerivAux_right, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left, measurable_fst, measurable_curry, MeasureTheory.measurable_stoppedValue, measurable_const_smul_iff₀, ProbabilityTheory.measurable_countableFiltration_countablePartitionSet, MeasureTheory.Measure.haveLebesgueDecomposition_spec, measurable_sub_const', NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm, measurable_prodMk_left, measurable_abs, MeasureTheory.AEStronglyMeasurable.measurable_mk, measurable_unit, ProbabilityTheory.measurable_memPartitionSet, measurable_piCongrLeft, measurable_to_bool, MeasureTheory.measurable_embeddingReal, measurable_quotient_mk'', measurable_coe_nnreal_real_iff, measurable_coe_nnreal_ennreal_iff, measurable_const_smul_iff, measurable_posPart, MeasureTheory.Measure.measurable_join, measurable_mul_unop, MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite, AEMeasurable.measurable_mk, measurable_inclusion, measurable_piEquivPiSubtypeProd, measurable_update, measurable_nnnorm, MeasureTheory.measurableSet_spanningSetsIndex, MeasurableSub.measurable_const_sub, measurable_ncard, measurable_dist

Theorems

NameKindAssumesProvesValidatesDepends On
aemeasurable_lineDeriv 📖mathematicalContinuous
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
NormedAddCommGroup.toSeminormedAddCommGroup
AEMeasurable
lineDeriv
NormedAddCommGroup.toAddCommGroup
NormedSpace.toModule
NontriviallyNormedField.toNormedField
—Measurable.aemeasurable
measurable_lineDeriv
aemeasurable_lineDeriv_uncurry 📖mathematicalContinuous
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
NormedAddCommGroup.toSeminormedAddCommGroup
AEMeasurable
Prod.instMeasurableSpace
lineDeriv
NormedAddCommGroup.toAddCommGroup
NormedSpace.toModule
NontriviallyNormedField.toNormedField
—Measurable.aemeasurable
measurable_lineDeriv_uncurry
aestronglyMeasurable_lineDeriv 📖mathematicalContinuous
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
NormedAddCommGroup.toSeminormedAddCommGroup
MeasureTheory.AEStronglyMeasurable
lineDeriv
NormedAddCommGroup.toAddCommGroup
NormedSpace.toModule
NontriviallyNormedField.toNormedField
—MeasureTheory.StronglyMeasurable.aestronglyMeasurable
stronglyMeasurable_lineDeriv
aestronglyMeasurable_lineDeriv_uncurry 📖mathematicalContinuous
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
NormedAddCommGroup.toSeminormedAddCommGroup
MeasureTheory.AEStronglyMeasurable
Prod.instMeasurableSpace
lineDeriv
NormedAddCommGroup.toAddCommGroup
NormedSpace.toModule
NontriviallyNormedField.toNormedField
—MeasureTheory.StronglyMeasurable.aestronglyMeasurable
stronglyMeasurable_lineDeriv_uncurry
measurableSet_lineDifferentiableAt 📖mathematicalContinuous
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
NormedAddCommGroup.toSeminormedAddCommGroup
MeasurableSet
setOf
LineDifferentiableAt
NormedAddCommGroup.toAddCommGroup
NormedSpace.toModule
NontriviallyNormedField.toNormedField
—Continuous.comp'
Continuous.fun_add
IsTopologicalAddGroup.toContinuousAdd
SeminormedAddCommGroup.toIsTopologicalAddGroup
Continuous.fst
continuous_id'
Continuous.smul
IsBoundedSMul.continuousSMul
NormedSpace.toIsBoundedSMul
Continuous.snd
continuous_const
measurable_prodMk_right
measurableSet_of_differentiableAt_with_param
BorelSpace.opensMeasurable
measurableSet_lineDifferentiableAt_uncurry 📖mathematicalContinuous
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
NormedAddCommGroup.toSeminormedAddCommGroup
MeasurableSet
Prod.instMeasurableSpace
setOf
LineDifferentiableAt
NormedAddCommGroup.toAddCommGroup
NormedSpace.toModule
NontriviallyNormedField.toNormedField
—Continuous.comp
Continuous.add
IsTopologicalAddGroup.toContinuousAdd
SeminormedAddCommGroup.toIsTopologicalAddGroup
continuous_fst
Continuous.smul
IsBoundedSMul.continuousSMul
NormedSpace.toIsBoundedSMul
continuous_snd
measurableSet_of_differentiableAt_with_param
Prod.opensMeasurableSpace
secondCountableTopologyEither_of_right
BorelSpace.opensMeasurable
measurable_prodMk_right
measurable_lineDeriv 📖mathematicalContinuous
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
NormedAddCommGroup.toSeminormedAddCommGroup
Measurable
lineDeriv
NormedAddCommGroup.toAddCommGroup
NormedSpace.toModule
NontriviallyNormedField.toNormedField
—Continuous.comp'
Continuous.fun_add
IsTopologicalAddGroup.toContinuousAdd
SeminormedAddCommGroup.toIsTopologicalAddGroup
Continuous.fst
continuous_id'
Continuous.smul
IsBoundedSMul.continuousSMul
NormedSpace.toIsBoundedSMul
Continuous.snd
continuous_const
Measurable.comp
measurable_deriv_with_param
BorelSpace.opensMeasurable
measurable_prodMk_right
measurable_lineDeriv_uncurry 📖mathematicalContinuous
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
NormedAddCommGroup.toSeminormedAddCommGroup
Measurable
Prod.instMeasurableSpace
lineDeriv
NormedAddCommGroup.toAddCommGroup
NormedSpace.toModule
NontriviallyNormedField.toNormedField
—Continuous.comp
Continuous.add
IsTopologicalAddGroup.toContinuousAdd
SeminormedAddCommGroup.toIsTopologicalAddGroup
continuous_fst
Continuous.smul
IsBoundedSMul.continuousSMul
NormedSpace.toIsBoundedSMul
continuous_snd
Measurable.comp
measurable_deriv_with_param
Prod.opensMeasurableSpace
secondCountableTopologyEither_of_right
BorelSpace.opensMeasurable
measurable_prodMk_right
stronglyMeasurable_lineDeriv 📖mathematicalContinuous
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
NormedAddCommGroup.toSeminormedAddCommGroup
MeasureTheory.StronglyMeasurable
lineDeriv
NormedAddCommGroup.toAddCommGroup
NormedSpace.toModule
NontriviallyNormedField.toNormedField
—Continuous.comp'
Continuous.fun_add
IsTopologicalAddGroup.toContinuousAdd
SeminormedAddCommGroup.toIsTopologicalAddGroup
Continuous.fst
continuous_id'
Continuous.smul
IsBoundedSMul.continuousSMul
NormedSpace.toIsBoundedSMul
Continuous.snd
continuous_const
MeasureTheory.StronglyMeasurable.comp_measurable
stronglyMeasurable_deriv_with_param
BorelSpace.opensMeasurable
measurable_prodMk_right
stronglyMeasurable_lineDeriv_uncurry 📖mathematicalContinuous
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
NormedAddCommGroup.toSeminormedAddCommGroup
MeasureTheory.StronglyMeasurable
Prod.instMeasurableSpace
lineDeriv
NormedAddCommGroup.toAddCommGroup
NormedSpace.toModule
NontriviallyNormedField.toNormedField
—Continuous.comp
Continuous.add
IsTopologicalAddGroup.toContinuousAdd
SeminormedAddCommGroup.toIsTopologicalAddGroup
continuous_fst
Continuous.smul
IsBoundedSMul.continuousSMul
NormedSpace.toIsBoundedSMul
continuous_snd
MeasureTheory.StronglyMeasurable.comp_measurable
stronglyMeasurable_deriv_with_param
Prod.opensMeasurableSpace
secondCountableTopologyEither_of_right
BorelSpace.opensMeasurable
secondCountableTopologyEither_of_left
TopologicalSpace.instSecondCountableTopologyProd
measurable_prodMk_right

---

← Back to Index