Blueprint Summary🔗

Overview

Total entries307completed: 168; deps incomplete: 5; sorries: 0; no proof: 80

Ready now8Entries whose next formalization step is currently unblocked.

Fully closed168Local code and prerequisite closure are both complete.

Actionable priorities5Entries ready now and already unlocking downstream work.

Current blockers34Missing external or incomplete Lean declarations.

Missing informal coverage12Entries with Lean code but missing an informal statement or proof block.

Ready next (5)

«def:jordan-one-dimensional-interval»(Definition)

Ready for statement work.

stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 18
«def:ring-of-sets»(Definition)

Ready for statement work.

stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 2
«ex:continuous-riemann-integrable»(Proposition)

Ready for proof work.

tag: notreadytag: examplestage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: ready to formalize
Associated lean decls (1)
- NoteKsk.Chapter01.riemannIntegrable_of_continuousOn
«thm:riemann-darboux-equivalence»(Theorem)

Ready for proof work.

tag: notreadystage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: ready to formalize
Associated lean decls (2)
- NoteKsk.Chapter01.riemann_integrable_iff_darboux_integrable
- NoteKsk.Chapter01.riemannIntegral_eq_darbouxIntegral
«thm:riemann-sums-tendsto-integral»(Theorem)

Ready for proof work.

tag: notreadystage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: ready to formalize
Associated lean decls (1)
- NoteKsk.Chapter01.riemann_sums_tendsto_integral

Current blockers (34)

«lem:jordan-outer-finite-subadditive»(Lemma)

Missing external Lean declaration: NoteKsk.Chapter02.jordanOuterMeasure_finite_subadditive [missing declaration]
«thm:jordan-measurable-criterion»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter02.jordanMeasurable_iff_indicator_riemannIntegrable [missing declaration]
«thm:jordan-measurable-criterion»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter02.jordanMeasurable_iff_boundary_null [missing declaration]
«ex:unbounded-not-riemann-integrable»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter01.not_riemannIntegrable_of_unboundedOn [missing declaration]
«ex:elementary-set-jordan-measurable»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter02.jordanMeasure_elementarySet [missing declaration]
«ex:elementary-set-jordan-measurable»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter02.elementarySet_jordanMeasurable [missing declaration]
«cor:riemann-integral-indicator-jordan-measure»(Corollary)

Missing external Lean declaration: NoteKsk.Chapter02.riemannIntegral_indicator_eq_jordanMeasure [missing declaration]
«ex:piecewise-constant-riemann-integrable»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter01.riemannIntegrable_piecewiseConstant [missing declaration]
«ex:continuous-riemann-integrable»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter01.riemannIntegrable_of_continuousOn [missing declaration]
«thm:jordan-measurable-set-operations»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter02.jordanMeasurable_compl_in_box [missing declaration]
«thm:jordan-measurable-set-operations»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter02.jordanMeasurable_inter [missing declaration]
«thm:jordan-measurable-set-operations»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter02.jordanMeasurable_union [missing declaration]
«ex:dirichlet-not-riemann-integrable»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter01.not_riemannIntegrable_dirichlet [missing declaration]
«ex:dirichlet-not-riemann-integrable»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter01.dirichlet [missing declaration]
«ex:piecewise-continuous-riemann-integrable»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter01.riemannIntegrable_piecewiseContinuous [missing declaration]
«thm:riemann-darboux-equivalence»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter01.riemannIntegral_eq_darbouxIntegral [missing declaration]
«thm:riemann-darboux-equivalence»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter01.riemann_integrable_iff_darboux_integrable [missing declaration]
«ex:riemann-integral-identity»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter01.riemannIntegral_id [missing declaration]
«ex:riemann-integral-identity»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter01.riemannIntegrable_id [missing declaration]
«ex:riemann-integral-constant»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter01.riemannIntegral_const [missing declaration]
«ex:riemann-integral-constant»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter01.riemannIntegrable_const [missing declaration]
«ex:finite-set-jordan-null»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter02.jordanNullSet_finite [missing declaration]
«prop:jordan-null-set-measurable»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter02.jordanNullSet_jordanMeasurable [missing declaration]
«lem:jordan-grid-subdivision»(Lemma)

Missing external Lean declaration: NoteKsk.Chapter02.elementaryVolume_eq_sum_boxVolume [missing declaration]
«lem:jordan-grid-subdivision»(Lemma)

Missing external Lean declaration: NoteKsk.Chapter02.elementarySet_finite_union_leftHalfOpenBoxes [missing declaration]
«thm:riemann-sums-tendsto-integral»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter01.riemann_sums_tendsto_integral [missing declaration]
«thm:riemann-ftc»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter01.fundamental_theorem_of_calculus_for_riemann [missing declaration]
«thm:jordan-elementary-volume-properties»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter02.elementaryVolume_translate [missing declaration]
«thm:jordan-elementary-volume-properties»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter02.elementaryVolume_union_of_disjoint [missing declaration]
«ex:singleton-jordan-null»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter02.jordanNullSet_singleton [missing declaration]
«thm:jordan-measure-properties»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter02.jordanMeasure_union_of_disjoint [missing declaration]
«thm:jordan-measure-properties»(Theorem)

Missing external Lean declaration: NoteKsk.Chapter02.jordanMeasure_union [missing declaration]
«prop:jordan-inner-le-outer»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter02.jordanInnerMeasure_le_jordanOuterMeasure [missing declaration]
«ex:boundary-elementary-jordan-null»(Proposition)

Missing external Lean declaration: NoteKsk.Chapter02.jordanNullSet_boundary_elementary [missing declaration]

Missing informal coverage (12)

«ex:discrete-semirings»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter06.powerset_isSetSemiring
«cor:iterated-integral-exchange»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter11.integral_integral_swap
«thm:riemann-darboux-equivalence»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter01.riemann_integrable_iff_darboux_integrable
- NoteKsk.Chapter01.riemannIntegral_eq_darbouxIntegral
«ex:counting-measure»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter06.countingMeasure_apply
«ex:lebesgue-measure-from-caratheodory-hahn»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter06.lambdaStar_eq_inducedOuterMeasureFromBoxes
«cor:volume-under-affine-map»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
«thm:change-of-variables-diffeomorphism»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
- NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
«cor:affine-change-of-variables»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
- NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
«ex:product-function-tonelli»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter11.lintegral_prod_mul
«ex:dirac-measure»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter06.diracMeasure_apply
«prop:lebesgue-global-local»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasurableSet_windows
«ex:left-half-open-semiring»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter06.leftHalfOpenBox_isSetSemiring

Entry index (307)

Definitions78completed: 42; deps incomplete: 5; sorries: 0; no proof: 0

Propositions114completed: 49; deps incomplete: 0; sorries: 0; no proof: 52

Lemmas17completed: 13; deps incomplete: 0; sorries: 0; no proof: 2

Theorems72completed: 45; deps incomplete: 0; sorries: 0; no proof: 20

Corollaries26completed: 19; deps incomplete: 0; sorries: 0; no proof: 6

Informal-only entries111

Definition Index (78)

«06caratheodory02-definition-auto-2113b228f0»(Definition)
«12banach-definition-auto-4a6ca6d5ba»(Definition)
«14linear-opr-definition-auto-fe652db767»(Definition)
«def:borel-sigma-algebra»(Definition)
Associated lean decls (1)
- NoteKsk.Chapter06.borelSigmaAlgebra
«def:premeasure-on-semiring»(Definition)
Associated lean decls (2)
- MeasureTheory.AddContent
- NoteKsk.IsPremeasureOnSemiring
«def:jordan-one-dimensional-interval»(Definition)
«12banach-definition-auto-7bd2c77569»(Definition)
«def:jordan-outer-inner-measure»(Definition)
Associated lean decls (2)
- NoteKsk.jordanOuterMeasure
- NoteKsk.jordanInnerMeasure
«12banach-definition-auto-5dcf314007»(Definition)
«12banach-definition-auto-de1b622eef»(Definition)
«13hilbert-definition-auto-32a874c6ce»(Definition)
«02jordan02-definition-auto-09fd3f3928»(Definition)
«def:lebesgue-inner-measure»(Definition)
Associated lean decls (1)
- NoteKsk.Chapter04.lambdaInner
«14linear-opr-definition-auto-5c90b2f36a»(Definition)
«def:outer-measure-generated-by-premeasure»(Definition)
Associated lean decls (1)
- NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure
«def:nonnegative-simple-function»(Definition)
Associated lean decls (2)
- NoteKsk.SimpleNNFun
- NoteKsk.Chapter08.simpleNNFun_measurable
«def:caratheodory-condition»(Definition)
Associated lean decls (3)
«13hilbert-definition-auto-5d4ee5bb89»(Definition)
«def:ae-convergence»(Definition)
Associated lean decls (1)
- NoteKsk.AEConvergesOn
«def:integral-over-subset»(Definition)
Associated lean decls (2)
- NoteKsk.setLintegralNN
- NoteKsk.Chapter08.setLintegralNN_eq_indicator
«def:riemann-sum»(Definition)
Associated lean decls (2)
- NoteKsk.Chapter01.IntervalPartition.IsTagged
- NoteKsk.Chapter01.riemannSum
«def:completion»(Definition)
Associated lean decls (3)
«02jordan02-definition-auto-11f0199ce8»(Definition)
«def:riemann-integrable»(Definition)
Associated lean decls (3)
«05lebesgue03-definition-auto-ab11a0a94e»(Definition)
«def:measurable-space»(Definition)
Associated lean decls (2)
- MeasurableSpace
- NoteKsk.SigmaAlgebra
«def:jordan-null-set»(Definition)
Associated lean decls (2)
- NoteKsk.JordanNullSet
- NoteKsk.Chapter02.jordanMeasure_eq_zero_of_null
«12banach-definition-auto-84ba8f01ee»(Definition)
«def:lebesgue-caratheodory-measurable»(Definition)
Associated lean decls (1)
- NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable
«def:semiring»(Definition)
Associated lean decls (1)
- MeasureTheory.IsSetSemiring
«def:measurable-function-space-notation»(Definition)
Associated lean decls (3)
«14linear-opr-definition-auto-47597d0b80»(Definition)
«12banach-definition-auto-c460ce1e9c»(Definition)
«13hilbert-definition-auto-259d3f6153»(Definition)
«02jordan02-definition-auto-5793cf4a96»(Definition)
«def:jordan-box»(Definition)
Associated lean decls (9)
«13hilbert-definition-auto-2a28e9ed50»(Definition)
«14linear-opr-definition-auto-0b94de9aeb»(Definition)
«13hilbert-definition-auto-1f8d0f9182»(Definition)
«13hilbert-definition-auto-49c9982d69»(Definition)
«def:lebesgue-measurable-function»(Definition)
Associated lean decls (3)
«def:lebesgue-outer-measure»(Definition)
Associated lean decls (9)
«def:riemann-interval-partition»(Definition)
Associated lean decls (5)
«13hilbert-definition-auto-ab9f9cd0e4»(Definition)
«def:L1-space»(Definition)
Associated lean decls (1)
- NoteKsk.L1Space
«def:sections»(Definition)
Associated lean decls (4)
«14linear-opr-definition-auto-fd375cb2c0»(Definition)
«def:countably-additive-measure»(Definition)
Associated lean decls (1)
- MeasureTheory.Measure
«def:darboux-upper-lower-integral»(Definition)
Associated lean decls (4)
«06caratheodory02-definition-auto-86b8c96217»(Definition)
«def:lebesgue-integrable-function»(Definition)
Associated lean decls (4)
«def:darboux-integrable»(Definition)
Associated lean decls (2)
- NoteKsk.Chapter01.DarbouxIntegrableOn
- NoteKsk.Chapter01.darbouxIntegral
«def:lebesgue-measurable-local»(Definition)
Associated lean decls (6)
«def:generated-sigma-algebra»(Definition)
Associated lean decls (3)
«def:outer-measure»(Definition)
Associated lean decls (4)
«def:positive-negative-parts»(Definition)
Associated lean decls (4)
«03lebesgue-outer-definition-auto-aaf4aa3003»(Definition)
Associated lean decls (2)
- NoteKsk.Chapter03.IsOuterMeasureFunction
- MeasureTheory.OuterMeasure
«03lebesgue-outer-definition-auto-8d32644e77»(Definition)
«def:simple-function-integral»(Definition)
Associated lean decls (2)
- NoteKsk.simpleLintegral
- NoteKsk.Chapter08.lintegralNN_eq_simple
«def:ae-prop»(Definition)
Associated lean decls (1)
- NoteKsk.AlmostEverywhereOn
«def:sigma-algebra»(Definition)
Associated lean decls (6)
«12banach-definition-auto-5f93b3dba8»(Definition)
«def:algebra-generated-by-semiring»(Definition)
Associated lean decls (1)
- NoteKsk.algebraGeneratedBySemiring
«def:darboux-sums»(Definition)
Associated lean decls (4)
«def:finite-additive-family»(Definition)
Associated lean decls (2)
- NoteKsk.FiniteAdditiveFamily
- MeasureTheory.IsSetRing
«def:premeasure-on-algebra»(Definition)
Associated lean decls (2)
- MeasureTheory.AddContent
- NoteKsk.IsPremeasureOnSemiring
«12banach-definition-auto-5b8f6e3fc7»(Definition)
«def:measurable-map»(Definition)
Associated lean decls (2)
- NoteKsk.MeasurableMap
- NoteKsk.Chapter07.measurableMap_iff_preimage
«def:measure»(Definition)
Associated lean decls (3)
«def:jordan-measurable»(Definition)
Associated lean decls (4)
«def:jordan-elementary-set»(Definition)
Associated lean decls (2)
- NoteKsk.IsElementarySet
- NoteKsk.elementaryVolume
«def:sigma-finite-measure»(Definition)
Associated lean decls (3)
«def:ring-of-sets»(Definition)
«14linear-opr-definition-auto-6db1d33ddc»(Definition)
«13hilbert-definition-auto-aed2a40a16»(Definition)
«def:borel-measure»(Definition)
Associated lean decls (1)
- NoteKsk.Chapter06.borelMeasure
«def:nonnegative-lebesgue-integral»(Definition)
Associated lean decls (2)
- NoteKsk.lintegralNN
- NoteKsk.Chapter08.lintegralNN_def
«def:pointwise-limits»(Definition)
Associated lean decls (4)

Theorem / Proposition / Lemma / Corollary Index (229)

«ex:indicator-function-measurable»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter07.indicator_measurable
«thm:continuity-under-integral-sign»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter10.continuous_integral_of_dominated
- NoteKsk.Chapter10.continuousAt_integral_of_dominated
«lem:local-measurable-finite-union-additivity»(Lemma)
Associated lean decls (2)
- NoteKsk.Chapter05.localLebesgueMeasurable_union
- NoteKsk.Chapter05.localLebesgueMeasurable_union_additive
«prop:measurable-vector-map»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter07.measurable_vector_map
«ex:discrete-semirings»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter06.powerset_isSetSemiring
«lem:jordan-outer-finite-subadditive»(Lemma)
Associated lean decls (1)
- NoteKsk.Chapter02.jordanOuterMeasure_finite_subadditive
«07mble-funcs-example-auto-2838d2b582»(Proposition)
«13hilbert-proposition-auto-dd72d110eb»(Proposition)
«thm:outer-measure-from-premeasure»(Theorem)
Associated lean decls (4)
«thm:jordan-measurable-criterion»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter02.jordanMeasurable_iff_boundary_null
- NoteKsk.Chapter02.jordanMeasurable_iff_indicator_riemannIntegrable
«cor:iterated-integral-exchange»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter11.integral_integral_swap
«prop:integral-representation-independence»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter09.integral_eq_sub_of_ae_eq_sub
«thm:inner-measure-via-interval»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter04.lambdaInner_eq_boxVolume_sub_lambdaStar_diff
«thm:lebesgue-measure-completion-of-borel»(Theorem)
Associated lean decls (3)
«12banach-proposition-auto-92e612b4f2»(Proposition)
«thm:riemann-implies-lebesgue-integrable»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter08.boxRiemann_integrableOn_and_integral_eq_of_bounded_aeContinuous
«12banach-theorem-auto-426c0c8fac»(Theorem)
«thm:vitali-nonmeasurable»(Theorem)
«thm:nonnegative-integral-simple-approximation»(Theorem)
Associated lean decls (3)
«12banach-theorem-auto-e5bd950a27»(Theorem)
«thm:lebesgue-measure-outer-regularity»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasure_outerRegular
«prop:simple-function-integral-basic»(Proposition)
Associated lean decls (5)
«02jordan02-theorem-auto-cfc2847f0d»(Theorem)
«lem:compact-splits-outer-measure»(Lemma)
Associated lean decls (1)
- NoteKsk.Chapter03.compact_splits_lambdaStar
«thm:lebesgue-measurable-implies-caratheodory»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasurable_implies_caratheodory
«13hilbert-example-auto-05b528424a»(Proposition)
«13hilbert-theorem-auto-8638e2a37f»(Theorem)
«06caratheodory02-example-auto-70bceb8d84»(Proposition)
«prop:integral-disjoint-additivity»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter09.setIntegral_union_of_disjoint
- NoteKsk.Chapter09.setIntegral_union_of_disjoint_of_integrable
«14linear-opr-corollary-auto-3cbe01ecb7»(Corollary)
«12banach-theorem-auto-a903d22d15»(Theorem)
«03lebesgue-outer-proposition-auto-e312ac0c17»(Proposition)
«12banach-example-auto-e2034d98b1»(Proposition)
«ex:unbounded-not-riemann-integrable»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter01.not_riemannIntegrable_of_unboundedOn
«13hilbert-theorem-auto-921927e104»(Theorem)
«03lebesgue-outer-theorem-auto-bcfe17076e»(Theorem)
«13hilbert-proposition-auto-d8707bd73b»(Proposition)
«ex:elementary-set-jordan-measurable»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter02.elementarySet_jordanMeasurable
- NoteKsk.Chapter02.jordanMeasure_elementarySet
«01riemann-example-auto-7828e2d268»(Proposition)
«12banach-example-auto-ccfbaa66df»(Proposition)
«14linear-opr-example-auto-0f685b2c35»(Proposition)
«prop:measurable-limsup-liminf»(Proposition)
Associated lean decls (4)
«thm:algebra-generated-by-semiring»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter06.algebraGeneratedBySemiring_isSetRing
- NoteKsk.Chapter06.algebraGeneratedBySemiring_measurable
«prop:positive-negative-basic-identities»(Proposition)
Associated lean decls (7)
«thm:fubini»(Theorem)
Associated lean decls (5)
«thm:polar-coordinates-rn»(Theorem)
«02jordan02-example-auto-7771caf6bf»(Proposition)
«thm:lebesgue-integral-basic-formulas»(Theorem)
Associated lean decls (9)
«ex:change-order-triangle»(Proposition)
«12banach-proposition-auto-abba30c310»(Proposition)
«prop:chebyshev-inequality»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter09.chebyshev_integrable_abs
«prop:ae-equality-equivalence»(Proposition)
Associated lean decls (2)
- NoteKsk.AEEqualOn
- NoteKsk.Chapter07.aeEqualOn_equivalence
«04lebesgue-inner-example-auto-0225bc1c45»(Proposition)
«thm:banach-tarski»(Theorem)
«04lebesgue-inner-corollary-auto-37d04eb610»(Corollary)
«prop:simple-function-integral-well-defined»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter08.simpleLintegral_congr
«cor:riemann-integral-indicator-jordan-measure»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter02.riemannIntegral_indicator_eq_jordanMeasure
«ex:piecewise-constant-riemann-integrable»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter01.PiecewiseConstantOnInterval
- NoteKsk.Chapter01.riemannIntegrable_piecewiseConstant
«lem:positive-distance-additive»(Lemma)
Associated lean decls (2)
- NoteKsk.Chapter03.PositiveDistanceApart
- NoteKsk.Chapter03.lambdaStar_union_of_positiveDistanceApart
«thm:borel-sets-are-lebesgue-measurable»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter06.borelSet_lebesgueMeasurable
«ex:continuous-riemann-integrable»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter01.riemannIntegrable_of_continuousOn
«thm:jordan-measurable-set-operations»(Theorem)
Associated lean decls (3)
«cor:lebesgue-caratheodory-equivalence»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasurable_iff_caratheodory
«prop:measurable-reciprocal»(Proposition)
Associated lean decls (3)
«cor:beppo-levi-l1»(Corollary)
«prop:null-set-integral-nonnegative»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter08.setLintegralNN_eq_zero_of_measure_zero
«ex:dirichlet-not-riemann-integrable»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter01.dirichlet
- NoteKsk.Chapter01.not_riemannIntegrable_dirichlet
«prop:integral-bound-by-constants»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter09.integral_bounds_of_ae_const_le
«thm:integrable-iff-absolute»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter08.integrable_norm
- NoteKsk.Chapter08.lebesgueIntegrable_iff_abs
«prop:integral-zero-iff-ae-zero»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter09.integral_abs_eq_zero_iff_ae_eq_zero
«02jordan02-proposition-auto-2ff693ea48»(Proposition)
«cor:L1-convergence-in-measure»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter09.chebyshev_integrable_abs
«02jordan02-example-auto-47516d5758»(Proposition)
«thm:lebesgue-measure-countable-additivity»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_tsum
«12banach-lemma-auto-b357918422»(Lemma)
«cor:local-measurable-set-operations»(Corollary)
Associated lean decls (2)
- NoteKsk.Chapter05.localLebesgueMeasurable_inter
- NoteKsk.Chapter05.localLebesgueMeasurable_diff
«lem:borel-eRR»(Lemma)
Associated lean decls (1)
- NoteKsk.Chapter07.borel_eReal_eq_generate_Iic_real
«03lebesgue-outer-proposition-auto-07f01b1f71»(Proposition)
«prop:signed-integral-ae-invariance»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter08.signed_integral_congr_ae
- NoteKsk.Chapter08.integral_respects_ae_representatives
«prop:lebesgue-measure-nonnegative»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter05.lebesgueMeasure_empty
- NoteKsk.Chapter05.lebesgueMeasure_nonneg
«ex:piecewise-continuous-riemann-integrable»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter01.PiecewiseContinuousOnInterval
- NoteKsk.Chapter01.riemannIntegrable_piecewiseContinuous
«thm:lebesgue-measure-inner-regularity»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasure_innerRegular
«08lintegral-example-auto-08d592162e»(Proposition)
«thm:riemann-darboux-equivalence»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter01.riemann_integrable_iff_darboux_integrable
- NoteKsk.Chapter01.riemannIntegral_eq_darbouxIntegral
«05lebesgue03-example-auto-3b737bca05»(Proposition)
«cor:interval-outer-measure-split»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter04.lambdaInner_eq_lambdaStar_iff_boxVolume_eq
«thm:lebesgue-measure-continuity-from-above»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasure_iInter_eq_iInf_of_antitone
«prop:integral-absolute-value-bound»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter09.abs_integral_le_integral_abs
- NoteKsk.Chapter09.norm_integral_le_integral_norm
«14linear-opr-proposition-auto-100e285ffb»(Proposition)
«thm:fatou-lemma»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter10.fatou_lintegral
- NoteKsk.Chapter10.fatou_lintegral_atTop
«ex:counting-measure»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter06.countingMeasure_apply
«thm:tonelli»(Theorem)
Associated lean decls (3)
«cor:countable-lebesgue-null»(Corollary)
Associated lean decls (2)
- NoteKsk.Chapter05.countable_lebesgueMeasurable
- NoteKsk.Chapter05.countable_lebesgueMeasure_eq_zero
«cor:inner-measure-via-compact-set»(Corollary)
«prop:integrable-as-difference»(Proposition)
Associated lean decls (5)
«13hilbert-corollary-auto-28874ae3ee»(Corollary)
«thm:lebesgue-measurable-function-criterion»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter07.measurable_ereal_criterion_all_thresholds
- NoteKsk.Chapter07.measurable_ereal_real_level_criterion
«ex:riemann-integral-identity»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter01.riemannIntegrable_id
- NoteKsk.Chapter01.riemannIntegral_id
«ex:riemann-integral-constant»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter01.riemannIntegrable_const
- NoteKsk.Chapter01.riemannIntegral_const
«thm:lebesgue-measure-continuity-from-below»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_iSup_of_mono
«02jordan02-example-auto-fa3e18599e»(Proposition)
«ex:polar-coordinates»(Proposition)
«ex:finite-set-jordan-null»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter02.jordanNullSet_finite
«ex:lebesgue-measure-from-caratheodory-hahn»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter06.lambdaStar_eq_inducedOuterMeasureFromBoxes
«cor:integral-finite-sum»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter09.integral_finset_sum
«lem:lebesgue-measure-finite-additivity»(Lemma)
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasure_union_add
«prop:jordan-null-set-measurable»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter02.jordanNullSet_jordanMeasurable
«prop:ae-modification-measurable»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter07.measurable_of_ae_eq_complete
«prop:lebesgue-measure-translation-invariant»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter05.lebesgueMeasurableSet_translate
- NoteKsk.Chapter05.lebesgueMeasure_translate
«lem:finite-open-compact-split»(Lemma)
Associated lean decls (1)
- NoteKsk.Chapter03.finiteOpen_compact_split
«14linear-opr-example-auto-cf9db84d71»(Proposition)
«09lintegral-prop-example-auto-d3ad988065»(Proposition)
«12banach-lemma-auto-73df993c86»(Lemma)
«thm:lebesgue-null-measurable»(Theorem)
Associated lean decls (3)
«lem:simple-function-approximation»(Lemma)
Associated lean decls (4)
«prop:measurable-countable-sup-inf»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter07.measurable_pointwiseSup
- NoteKsk.Chapter07.measurable_pointwiseInf
«thm:measurable-continuous-composition»(Corollary)
Associated lean decls (2)
- NoteKsk.Chapter07.measurable_continuous_comp
- NoteKsk.Chapter07.measurable_continuous_real_comp
«thm:jordan-inner-lebesgue-inner»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter04.jordanInnerMeasure_le_lambdaInner
«13hilbert-proposition-auto-3d898884b4»(Proposition)
«14linear-opr-example-auto-f81b4cda27»(Proposition)
«02jordan02-example-auto-9ce4c86a8e»(Proposition)
«08lintegral-example-auto-aab23f2012»(Proposition)
«prop:integral-monotonicity»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter09.integral_mono_ae_real
- NoteKsk.Chapter09.integral_mono_real
«lem:jordan-grid-subdivision»(Lemma)
Associated lean decls (2)
- NoteKsk.Chapter02.elementarySet_finite_union_leftHalfOpenBoxes
- NoteKsk.Chapter02.elementaryVolume_eq_sum_boxVolume
«08lintegral-example-auto-985634d68c»(Proposition)
«lem:lebesgue-measurable-caratheodory-finite»(Lemma)
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasurable_caratheodory_finite
«prop:interval-outer-measure-volume»(Proposition)
Associated lean decls (6)
«thm:integral-absolute-continuity»(Theorem)
Associated lean decls (4)
«prop:lebesgue-outer-translation-invariant»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter03.lambdaStar_translate
«lem:commute-induce-generate-sigma-algebra»(Lemma)
Associated lean decls (2)
- NoteKsk.Chapter07.comap_generatedSigmaAlgebra
- NoteKsk.Chapter07.measurable_to_generatedSigmaAlgebra
«12banach-example-auto-df4f8139d9»(Proposition)
«14linear-opr-theorem-auto-1ee719cdc3»(Theorem)
«cor:volume-under-affine-map»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
«ex:parallelogram-area»(Proposition)
«14linear-opr-proposition-auto-6b36a220ec»(Proposition)
«13hilbert-example-auto-fed54eefed»(Proposition)
«13hilbert-theorem-auto-c0d78cf6a1»(Theorem)
«thm:riemann-sums-tendsto-integral»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter01.riemann_sums_tendsto_integral
«thm:solovay-model»(Theorem)
«thm:change-of-variables-diffeomorphism»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
- NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
«prop:nonnegative-integral-ae-invariance»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter08.lintegralNN_congr_ae
«prop:L1-space-structure»(Proposition)
Associated lean decls (7)
«ex:triangle-area-tonelli»(Proposition)
«12banach-proposition-auto-a113ca5409»(Proposition)
«cor:affine-change-of-variables»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
- NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
«cor:lebesgue-measurable-set-operations»(Corollary)
Associated lean decls (4)
«cor:bounded-convergence»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter10.tendsto_integral_of_bounded_convergence
«thm:caratheodory-theorem»(Theorem)
Associated lean decls (8)
«13hilbert-example-auto-137bd3a060»(Proposition)
«thm:sections-measurable-general»(Theorem)
Associated lean decls (4)
«thm:finite-outer-measurable-iff-inner-outer»(Theorem)
Associated lean decls (3)
«lem:local-measurable-complement»(Lemma)
Associated lean decls (3)
«ex:finite-partition-semiring»(Proposition)
«10limits-example-auto-7371ef5f8f»(Proposition)
«prop:integral-zero-on-null-set»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter09.integral_eq_zero_of_measure_univ_zero
- NoteKsk.Chapter09.setIntegral_eq_zero_of_measure_zero
«prop:integral-ae-invariance»(Proposition)
Associated lean decls (3)
«thm:lebesgue-measure-basic»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter05.lebesgueMeasure_mono
- NoteKsk.Chapter05.lebesgueMeasure_iUnion_le_tsum
«cor:measurable-algebra-operations»(Corollary)
Associated lean decls (7)
«12banach-theorem-auto-fde4450b71»(Theorem)
«prop:inverse-image-basic»(Proposition)
Associated lean decls (3)
«thm:local-measurable-sigma-algebra»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter05.localLebesgueMeasurable_iUnion
- NoteKsk.Chapter05.localLebesgueMeasurable_iUnion_additive
«10limits-example-auto-7455ac8402»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter10.hasDerivAt_laplace_transform_of_dominated_loc_of_lip
«ex:continuous-function-measurable»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter07.continuous_borelMeasurable
«prop:nonnegative-integral-disjoint-additivity»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter08.setLintegralNN_disjoint_union
«prop:measurable-comparison-sets»(Proposition)
Associated lean decls (3)
«01riemann-theorem-auto-5b3744507b»(Theorem)
«thm:differentiation-under-integral-sign»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter10.hasFDerivAt_integral_under_dominated_loc_of_lip
- NoteKsk.Chapter10.hasDerivAt_integral_under_dominated_loc_of_lip
«13hilbert-example-auto-450f5a5852»(Proposition)
«ex:discrete-premeasures»(Proposition)
«prop:louter-le-jouter»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter03.lambdaStar_le_jordanOuterMeasure
«14linear-opr-proposition-auto-fa8dc9caaf»(Proposition)
«ex:product-function-tonelli»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter11.lintegral_prod_mul
«02jordan02-example-auto-09f40721a5»(Proposition)
«thm:lebesgue-measurable-sigma-algebra»(Theorem)
Associated lean decls (4)
«prop:inverse-image-sigma-algebra»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter07.inducedMeasurableSpace
- NoteKsk.Chapter07.inducedMeasurableSpace_measurable
«10limits-example-auto-ef82d9de32»(Proposition)
«03lebesgue-outer-example-auto-56b6bf606f»(Proposition)
«01riemann-theorem-auto-b4a925f916»(Theorem)
«cor:dominated-convergence-l1»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence
«cor:nonnegative-series-termwise-integration»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter10.lintegral_tsum
«thm:caratheodory-hahn-extension»(Theorem)
Associated lean decls (5)
«cor:ae-limit-measurable»(Corollary)
Associated lean decls (2)
- NoteKsk.Chapter07.measurable_of_ae_tendsto_real
- NoteKsk.Chapter07.measurable_of_ae_tendsto_ereal
«prop:nonnegative-chebyshev-inequality»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter09.chebyshev_lintegral
«01riemann-example-auto-4910acf622»(Proposition)
«lem:lebesgue-measure-limit»(Lemma)
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_iSup_of_mono
«ex:dirac-measure»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter06.diracMeasure_apply
«cor:dominated-integrability»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter08.dominated_integrability
«thm:dominated-convergence»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter10.integrable_limit_of_dominated_convergence
- NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence
«prop:compact-inner-outer-equal»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter04.lambdaInner_eq_lambdaStar_of_isCompact
- NoteKsk.Chapter04.lambdaInner_eq_zero_of_lambdaStar_eq_zero
«thm:inner-measure-via-open-set»(Theorem)
«thm:premeasure-extension-to-algebra»(Theorem)
Associated lean decls (3)
«prop:nonnegative-integral-basic»(Proposition)
Associated lean decls (3)
«thm:caratheodory-implies-lebesgue-measurable»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter05.caratheodory_implies_lebesgueMeasurable
«13hilbert-theorem-auto-ea6e5c2177»(Theorem)
«lem:finite-outer-compact-criterion»(Lemma)
Associated lean decls (2)
- NoteKsk.Chapter05.finiteOuter_compact_approx_criterion
- NoteKsk.Chapter05.finiteOuter_open_approx_criterion
«thm:riemann-ftc»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter01.fundamental_theorem_of_calculus_for_riemann
«thm:lebesgue-outer-regularity-open»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter03.lambdaStarByOpenSupersets
- NoteKsk.Chapter03.lambdaStar_outerRegular_open
«prop:nonnegative-integral-zero-iff-ae-zero»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter08.lintegralNN_eq_zero_iff_ae_eq_zero
«thm:cavalieri-product-measure»(Theorem)
Associated lean decls (4)
«12banach-proposition-auto-5ac0dfc586»(Proposition)
«thm:open-closed-lebesgue-measurable»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter05.isClosed_lebesgueMeasurable
- NoteKsk.Chapter05.isOpen_lebesgueMeasurable
«thm:jordan-elementary-volume-properties»(Theorem)
Associated lean decls (5)
«01riemann-example-auto-4bf36b1bd4»(Proposition)
«ex:singleton-jordan-null»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter02.jordanNullSet_singleton
«thm:jordan-measurable-lebesgue»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter05.jordanMeasurable_lebesgueMeasurable
- NoteKsk.Chapter05.lebesgueMeasure_eq_jordanMeasure
«14linear-opr-theorem-auto-a02e256b7f»(Theorem)
«03lebesgue-outer-example-auto-ee91c30bff»(Proposition)
«prop:lebesgue-global-local»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasurableSet_windows
«prop:integral-homogeneity»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter09.integral_const_mul_real
- NoteKsk.Chapter09.integral_smul
«thm:countable-outer-measure-zero»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter03.lambdaStar_singleton
- NoteKsk.Chapter03.lambdaStar_countable_eq_zero
«13hilbert-proposition-auto-c72a2bf678»(Proposition)
«thm:monotone-convergence»(Theorem)
Associated lean decls (3)
«08lintegral-example-auto-ae9b38d1f9»(Proposition)
«03lebesgue-outer-theorem-auto-2e7c2024ee»(Theorem)
«lem:finite-open-inner-compact»(Lemma)
Associated lean decls (1)
- NoteKsk.Chapter03.finiteOpen_innerCompact_exists
«cor:l1-absolutely-summable-series-termwise-integration»(Corollary)
Associated lean decls (2)
- NoteKsk.Chapter10.integral_tsum_eq_tsum_integral_of_summable_integral_norm
- NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm
«13hilbert-corollary-auto-720f5d0c1a»(Corollary)
«prop:lebesgue-inner-basic»(Proposition)
Associated lean decls (3)
«thm:jordan-measure-properties»(Theorem)
Associated lean decls (3)
«prop:jordan-inner-le-outer»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter02.jordanInnerMeasure_le_jordanOuterMeasure
«02jordan02-example-auto-3a4895ebda»(Proposition)
«ex:boundary-elementary-jordan-null»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter02.jordanNullSet_boundary_elementary
«prop:integral-additivity»(Proposition)
Associated lean decls (4)
«prop:null-set-integral-signed»(Proposition)
Associated lean decls (2)
- NoteKsk.Chapter08.integrableOn_of_measure_zero
- NoteKsk.Chapter08.setIntegral_eq_zero_of_measure_zero
«thm:dominated-series-termwise-integration»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter10.hasSum_integral_of_dominated_convergence
- NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm
«ex:left-half-open-semiring»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter06.leftHalfOpenBox_isSetSemiring
«cor:integrable-finite-ae»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter08.integrable_real_finite_ae
«thm:lebesgue-outer-measure»(Theorem)
Associated lean decls (5)
«thm:measurable-map-composition»(Theorem)
Associated lean decls (1)
- NoteKsk.Chapter07.measurable_comp

Dependency insights

Statement-used entries150Entries reused in statement dependencies.

Most used in statements (150)

«def:riemann-integrable»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 10
Associated lean decls (3)
«def:lebesgue-outer-measure»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 49
Associated lean decls (9)
«def:measure»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 13
Associated lean decls (3)
«def:nonnegative-lebesgue-integral»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 46
Associated lean decls (2)
- NoteKsk.lintegralNN
- NoteKsk.Chapter08.lintegralNN_def
«prop:nonnegative-integral-basic»(Proposition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 26
Associated lean decls (3)
«def:jordan-elementary-set»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 16
Associated lean decls (2)
- NoteKsk.IsElementarySet
- NoteKsk.elementaryVolume
«thm:lebesgue-measurable-sigma-algebra»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 15
Associated lean decls (4)
«thm:dominated-convergence»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 7
Associated lean decls (2)
- NoteKsk.Chapter10.integrable_limit_of_dominated_convergence
- NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence
«def:lebesgue-inner-measure»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 37
Associated lean decls (1)
- NoteKsk.Chapter04.lambdaInner
«thm:lebesgue-outer-regularity-open»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 32
Associated lean decls (2)
- NoteKsk.Chapter03.lambdaStarByOpenSupersets
- NoteKsk.Chapter03.lambdaStar_outerRegular_open
Show all 140 more statement-used entries
- «def:lebesgue-measurable-local»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 29
  Associated lean decls (6)
- «thm:integrable-iff-absolute»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 24
  Associated lean decls (2)
  - NoteKsk.Chapter08.integrable_norm
  - NoteKsk.Chapter08.lebesgueIntegrable_iff_abs
- «prop:integral-ae-invariance»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 15
  Associated lean decls (3)
- «cor:dominated-integrability»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 13
  Associated lean decls (1)
  - NoteKsk.Chapter08.dominated_integrability
- «def:jordan-outer-inner-measure»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 13
  Associated lean decls (2)
  - NoteKsk.jordanOuterMeasure
  - NoteKsk.jordanInnerMeasure
- «def:semiring»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 12
  Associated lean decls (1)
  - MeasureTheory.IsSetSemiring
- «thm:monotone-convergence»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 11
  Associated lean decls (3)
- «def:jordan-null-set»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 8
  Associated lean decls (2)
  - NoteKsk.JordanNullSet
  - NoteKsk.Chapter02.jordanMeasure_eq_zero_of_null
- «def:premeasure-on-semiring»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 7
  Associated lean decls (2)
  - MeasureTheory.AddContent
  - NoteKsk.IsPremeasureOnSemiring
- «def:jordan-measurable»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
  Associated lean decls (4)
- «thm:lebesgue-measurable-function-criterion»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 5
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_ereal_criterion_all_thresholds
  - NoteKsk.Chapter07.measurable_ereal_real_level_criterion
- «def:measurable-map»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 68
  Associated lean decls (2)
  - NoteKsk.MeasurableMap
  - NoteKsk.Chapter07.measurableMap_iff_preimage
- «def:measurable-function-space-notation»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 56
  Associated lean decls (3)
- «thm:lebesgue-outer-measure»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 34
  Associated lean decls (5)
- «def:lebesgue-integrable-function»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 29
  Associated lean decls (4)
- «cor:interval-outer-measure-split»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 27
  Associated lean decls (1)
  - NoteKsk.Chapter04.lambdaInner_eq_lambdaStar_iff_boxVolume_eq
- «def:integral-over-subset»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 27
  Associated lean decls (2)
  - NoteKsk.setLintegralNN
  - NoteKsk.Chapter08.setLintegralNN_eq_indicator
- «thm:finite-outer-measurable-iff-inner-outer»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 24
  Associated lean decls (3)
- «lem:local-measurable-finite-union-additivity»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 21
  Associated lean decls (2)
  - NoteKsk.Chapter05.localLebesgueMeasurable_union
  - NoteKsk.Chapter05.localLebesgueMeasurable_union_additive
- «thm:local-measurable-sigma-algebra»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 19
  Associated lean decls (2)
  - NoteKsk.Chapter05.localLebesgueMeasurable_iUnion
  - NoteKsk.Chapter05.localLebesgueMeasurable_iUnion_additive
- «prop:integral-monotonicity»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 11
  Associated lean decls (2)
  - NoteKsk.Chapter09.integral_mono_ae_real
  - NoteKsk.Chapter09.integral_mono_real
- «lem:lebesgue-measure-limit»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 10
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_iSup_of_mono
- «thm:open-closed-lebesgue-measurable»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 9
  Associated lean decls (2)
  - NoteKsk.Chapter05.isClosed_lebesgueMeasurable
  - NoteKsk.Chapter05.isOpen_lebesgueMeasurable
- «def:sections»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 6
  Associated lean decls (4)
- «prop:integral-additivity»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (4)
- «thm:change-of-variables-diffeomorphism»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (2)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
  - NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
- «thm:tonelli»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (3)
- «lem:borel-eRR»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 63
  Associated lean decls (1)
  - NoteKsk.Chapter07.borel_eReal_eq_generate_Iic_real
- «def:nonnegative-simple-function»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 50
  Associated lean decls (2)
  - NoteKsk.SimpleNNFun
  - NoteKsk.Chapter08.simpleNNFun_measurable
- «def:positive-negative-parts»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 31
  Associated lean decls (4)
- «def:simple-function-integral»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 29
  Associated lean decls (2)
  - NoteKsk.simpleLintegral
  - NoteKsk.Chapter08.lintegralNN_eq_simple
- «prop:null-set-integral-nonnegative»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 23
  Associated lean decls (1)
  - NoteKsk.Chapter08.setLintegralNN_eq_zero_of_measure_zero
- «lem:local-measurable-complement»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 22
  Associated lean decls (3)
- «prop:null-set-integral-signed»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 19
  Associated lean decls (2)
  - NoteKsk.Chapter08.integrableOn_of_measure_zero
  - NoteKsk.Chapter08.setIntegral_eq_zero_of_measure_zero
- «def:sigma-algebra»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 18
  Associated lean decls (6)
- «prop:signed-integral-ae-invariance»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 17
  Associated lean decls (2)
  - NoteKsk.Chapter08.signed_integral_congr_ae
  - NoteKsk.Chapter08.integral_respects_ae_representatives
- «def:riemann-interval-partition»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 15
  Associated lean decls (5)
- «prop:compact-inner-outer-equal»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 12
  Associated lean decls (2)
  - NoteKsk.Chapter04.lambdaInner_eq_lambdaStar_of_isCompact
  - NoteKsk.Chapter04.lambdaInner_eq_zero_of_lambdaStar_eq_zero
- «lem:commute-induce-generate-sigma-algebra»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (2)
  - NoteKsk.Chapter07.comap_generatedSigmaAlgebra
  - NoteKsk.Chapter07.measurable_to_generatedSigmaAlgebra
- «prop:integral-absolute-value-bound»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (2)
  - NoteKsk.Chapter09.abs_integral_le_integral_abs
  - NoteKsk.Chapter09.norm_integral_le_integral_norm
- «def:finite-additive-family»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 7
  Associated lean decls (2)
  - NoteKsk.FiniteAdditiveFamily
  - MeasureTheory.IsSetRing
- «prop:nonnegative-integral-disjoint-additivity»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 7
  Associated lean decls (1)
  - NoteKsk.Chapter08.setLintegralNN_disjoint_union
- «def:outer-measure»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (4)
- «def:algebra-generated-by-semiring»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - NoteKsk.algebraGeneratedBySemiring
- «def:generated-sigma-algebra»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (3)
- «def:lebesgue-caratheodory-measurable»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable
- «lem:lebesgue-measure-finite-additivity»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_union_add
- «thm:lebesgue-measure-outer-regularity»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_outerRegular
- «cor:lebesgue-measurable-set-operations»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (4)
- «def:ae-prop»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (1)
  - NoteKsk.AlmostEverywhereOn
- «def:caratheodory-condition»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (3)
- «prop:integrable-as-difference»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (5)
- «prop:nonnegative-integral-zero-iff-ae-zero»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (1)
  - NoteKsk.Chapter08.lintegralNN_eq_zero_iff_ae_eq_zero
- «def:borel-sigma-algebra»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter06.borelSigmaAlgebra
- «thm:jordan-measurable-criterion»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (2)
  - NoteKsk.Chapter02.jordanMeasurable_iff_boundary_null
  - NoteKsk.Chapter02.jordanMeasurable_iff_indicator_riemannIntegrable
- «thm:lebesgue-measure-countable-additivity»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_tsum
- «thm:premeasure-extension-to-algebra»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (3)
- «prop:chebyshev-inequality»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_integrable_abs
- «prop:integral-homogeneity»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.Chapter09.integral_const_mul_real
  - NoteKsk.Chapter09.integral_smul
- «prop:integral-zero-iff-ae-zero»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_abs_eq_zero_iff_ae_eq_zero
- «thm:countable-outer-measure-zero»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.Chapter03.lambdaStar_singleton
  - NoteKsk.Chapter03.lambdaStar_countable_eq_zero
- «def:measurable-space»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 69
  Associated lean decls (2)
  - MeasurableSpace
  - NoteKsk.SigmaAlgebra
- «def:lebesgue-measurable-function»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 57
  Associated lean decls (3)
- «lem:finite-open-inner-compact»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 31
  Associated lean decls (1)
  - NoteKsk.Chapter03.finiteOpen_innerCompact_exists
- «lem:positive-distance-additive»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 31
  Associated lean decls (2)
  - NoteKsk.Chapter03.PositiveDistanceApart
  - NoteKsk.Chapter03.lambdaStar_union_of_positiveDistanceApart
- «lem:finite-open-compact-split»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 30
  Associated lean decls (1)
  - NoteKsk.Chapter03.finiteOpen_compact_split
- «lem:compact-splits-outer-measure»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 29
  Associated lean decls (1)
  - NoteKsk.Chapter03.compact_splits_lambdaStar
- «prop:interval-outer-measure-volume»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 29
  Associated lean decls (6)
- «lem:simple-function-approximation»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 28
  Associated lean decls (4)
- «thm:inner-measure-via-interval»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 28
  Associated lean decls (1)
  - NoteKsk.Chapter04.lambdaInner_eq_boxVolume_sub_lambdaStar_diff
- «prop:simple-function-integral-basic»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 27
  Associated lean decls (5)
- «thm:nonnegative-integral-simple-approximation»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 27
  Associated lean decls (3)
- «lem:finite-outer-compact-criterion»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 22
  Associated lean decls (2)
  - NoteKsk.Chapter05.finiteOuter_compact_approx_criterion
  - NoteKsk.Chapter05.finiteOuter_open_approx_criterion
- «cor:local-measurable-set-operations»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 20
  Associated lean decls (2)
  - NoteKsk.Chapter05.localLebesgueMeasurable_inter
  - NoteKsk.Chapter05.localLebesgueMeasurable_diff
- «def:jordan-one-dimensional-interval»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 18
- «def:jordan-box»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 17
  Associated lean decls (9)
- «prop:lebesgue-global-local»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 16
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurableSet_windows
- «prop:lebesgue-inner-basic»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
  Associated lean decls (3)
- «def:riemann-sum»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (2)
  - NoteKsk.Chapter01.IntervalPartition.IsTagged
  - NoteKsk.Chapter01.riemannSum
- «prop:inverse-image-basic»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (3)
- «prop:inverse-image-sigma-algebra»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (2)
  - NoteKsk.Chapter07.inducedMeasurableSpace
  - NoteKsk.Chapter07.inducedMeasurableSpace_measurable
- «thm:fatou-lemma»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (2)
  - NoteKsk.Chapter10.fatou_lintegral
  - NoteKsk.Chapter10.fatou_lintegral_atTop
- «prop:integral-representation-independence»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_eq_sub_of_ae_eq_sub
- «prop:nonnegative-integral-ae-invariance»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (1)
  - NoteKsk.Chapter08.lintegralNN_congr_ae
- «prop:positive-negative-basic-identities»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (7)
- «def:darboux-sums»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (4)
- «def:premeasure-on-algebra»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (2)
  - MeasureTheory.AddContent
  - NoteKsk.IsPremeasureOnSemiring
- «ex:boundary-elementary-jordan-null»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_boundary_elementary
- «lem:jordan-outer-finite-subadditive»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanOuterMeasure_finite_subadditive
- «def:darboux-upper-lower-integral»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (4)
- «def:outer-measure-generated-by-premeasure»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure
- «def:pointwise-limits»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (4)
- «ex:continuous-function-measurable»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter07.continuous_borelMeasurable
- «lem:lebesgue-measurable-caratheodory-finite»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurable_caratheodory_finite
- «prop:nonnegative-chebyshev-inequality»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_lintegral
- «thm:measurable-map-composition»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter07.measurable_comp
- «cor:affine-change-of-variables»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
  - NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
- «cor:integral-finite-sum»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_finset_sum
- «def:darboux-integrable»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.Chapter01.DarbouxIntegrableOn
  - NoteKsk.Chapter01.darbouxIntegral
- «def:ring-of-sets»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
- «prop:ae-equality-equivalence»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.AEEqualOn
  - NoteKsk.Chapter07.aeEqualOn_equivalence
- «prop:lebesgue-outer-translation-invariant»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter03.lambdaStar_translate
- «prop:measurable-countable-sup-inf»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_pointwiseSup
  - NoteKsk.Chapter07.measurable_pointwiseInf
- «prop:measurable-vector-map»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter07.measurable_vector_map
- «thm:caratheodory-implies-lebesgue-measurable»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter05.caratheodory_implies_lebesgueMeasurable
- «thm:caratheodory-theorem»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (8)
- «thm:lebesgue-measurable-implies-caratheodory»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurable_implies_caratheodory
- «thm:measurable-continuous-composition»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_continuous_comp
  - NoteKsk.Chapter07.measurable_continuous_real_comp
- «thm:outer-measure-from-premeasure»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (4)
- «cor:lebesgue-caratheodory-equivalence»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurable_iff_caratheodory
- «cor:measurable-algebra-operations»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (7)
- «cor:riemann-integral-indicator-jordan-measure»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter02.riemannIntegral_indicator_eq_jordanMeasure
- «cor:volume-under-affine-map»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
- «def:L1-space»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.L1Space
- «def:ae-convergence»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.AEConvergesOn
- «def:borel-measure»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter06.borelMeasure
- «def:completion»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- «def:sigma-finite-measure»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- «ex:continuous-riemann-integrable»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter01.riemannIntegrable_of_continuousOn
- «ex:discrete-semirings»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter06.powerset_isSetSemiring
- «ex:left-half-open-semiring»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter06.leftHalfOpenBox_isSetSemiring
- «ex:singleton-jordan-null»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_singleton
- «lem:jordan-grid-subdivision»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter02.elementarySet_finite_union_leftHalfOpenBoxes
  - NoteKsk.Chapter02.elementaryVolume_eq_sum_boxVolume
- «prop:ae-modification-measurable»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter07.measurable_of_ae_eq_complete
- «prop:integral-disjoint-additivity»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter09.setIntegral_union_of_disjoint
  - NoteKsk.Chapter09.setIntegral_union_of_disjoint_of_integrable
- «prop:integral-zero-on-null-set»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter09.integral_eq_zero_of_measure_univ_zero
  - NoteKsk.Chapter09.setIntegral_eq_zero_of_measure_zero
- «prop:lebesgue-measure-translation-invariant»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter05.lebesgueMeasurableSet_translate
  - NoteKsk.Chapter05.lebesgueMeasure_translate
- «prop:louter-le-jouter»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter03.lambdaStar_le_jordanOuterMeasure
- «prop:measurable-limsup-liminf»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (4)
- «thm:caratheodory-hahn-extension»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (5)
- «thm:differentiation-under-integral-sign»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter10.hasFDerivAt_integral_under_dominated_loc_of_lip
  - NoteKsk.Chapter10.hasDerivAt_integral_under_dominated_loc_of_lip
- «thm:dominated-series-termwise-integration»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter10.hasSum_integral_of_dominated_convergence
  - NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm
- «thm:fubini»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (5)
- «thm:jordan-inner-lebesgue-inner»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter04.jordanInnerMeasure_le_lambdaInner
- «thm:jordan-measurable-set-operations»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- «thm:lebesgue-measure-continuity-from-below»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_iSup_of_mono
- «thm:lebesgue-null-measurable»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- «thm:riemann-darboux-equivalence»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter01.riemann_integrable_iff_darboux_integrable
  - NoteKsk.Chapter01.riemannIntegral_eq_darbouxIntegral
- «thm:riemann-sums-tendsto-integral»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter01.riemann_sums_tendsto_integral
- «thm:sections-measurable-general»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (4)

Metadata

Tags in use4Distinct tags currently attached to blueprint entries.

Tag rollups (4)

tag: notready

entries: 23actionable: 3quick wins: 0linked PRs: 0
tag: example

entries: 58actionable: 1quick wins: 0linked PRs: 0
tag: leanok

entries: 148actionable: 0quick wins: 0linked PRs: 0
tag: mathlibok

entries: 9actionable: 0quick wins: 0linked PRs: 0

Metadata audit

Missing owner307

Missing effort307

Untagged88

Missing owner (307)

«01riemann-example-auto-4910acf622»(Proposition)

Missing owner metadata.

tag: example
«01riemann-example-auto-4bf36b1bd4»(Proposition)

Missing owner metadata.

tag: example
«01riemann-example-auto-7828e2d268»(Proposition)

Missing owner metadata.

tag: example
«01riemann-theorem-auto-5b3744507b»(Theorem)

Missing owner metadata.
«01riemann-theorem-auto-b4a925f916»(Theorem)

Missing owner metadata.
«02jordan02-definition-auto-09fd3f3928»(Definition)

Missing owner metadata.
«02jordan02-definition-auto-11f0199ce8»(Definition)

Missing owner metadata.
«02jordan02-definition-auto-5793cf4a96»(Definition)

Missing owner metadata.
«02jordan02-example-auto-09f40721a5»(Proposition)

Missing owner metadata.

tag: example
«02jordan02-example-auto-3a4895ebda»(Proposition)

Missing owner metadata.

tag: example
Show all 297 more entries missing owner
- «02jordan02-example-auto-47516d5758»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «02jordan02-example-auto-7771caf6bf»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «02jordan02-example-auto-9ce4c86a8e»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «02jordan02-example-auto-fa3e18599e»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «02jordan02-proposition-auto-2ff693ea48»(Proposition)
  
  Missing owner metadata.
- «02jordan02-theorem-auto-cfc2847f0d»(Theorem)
  
  Missing owner metadata.
- «03lebesgue-outer-definition-auto-8d32644e77»(Definition)
  
  Missing owner metadata.
- «03lebesgue-outer-definition-auto-aaf4aa3003»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter03.IsOuterMeasureFunction
  - MeasureTheory.OuterMeasure
- «03lebesgue-outer-example-auto-56b6bf606f»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «03lebesgue-outer-example-auto-ee91c30bff»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «03lebesgue-outer-proposition-auto-07f01b1f71»(Proposition)
  
  Missing owner metadata.
- «03lebesgue-outer-proposition-auto-e312ac0c17»(Proposition)
  
  Missing owner metadata.
- «03lebesgue-outer-theorem-auto-2e7c2024ee»(Theorem)
  
  Missing owner metadata.
- «03lebesgue-outer-theorem-auto-bcfe17076e»(Theorem)
  
  Missing owner metadata.
- «04lebesgue-inner-corollary-auto-37d04eb610»(Corollary)
  
  Missing owner metadata.
- «04lebesgue-inner-example-auto-0225bc1c45»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «05lebesgue03-definition-auto-ab11a0a94e»(Definition)
  
  Missing owner metadata.
- «05lebesgue03-example-auto-3b737bca05»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «06caratheodory02-definition-auto-2113b228f0»(Definition)
  
  Missing owner metadata.
- «06caratheodory02-definition-auto-86b8c96217»(Definition)
  
  Missing owner metadata.
- «06caratheodory02-example-auto-70bceb8d84»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «07mble-funcs-example-auto-2838d2b582»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «08lintegral-example-auto-08d592162e»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «08lintegral-example-auto-985634d68c»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «08lintegral-example-auto-aab23f2012»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «08lintegral-example-auto-ae9b38d1f9»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «09lintegral-prop-example-auto-d3ad988065»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «10limits-example-auto-7371ef5f8f»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «10limits-example-auto-7455ac8402»(Proposition)
  
  Missing owner metadata.
  
  tag: example
  Associated lean decls (1)
  - NoteKsk.Chapter10.hasDerivAt_laplace_transform_of_dominated_loc_of_lip
- «10limits-example-auto-ef82d9de32»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «12banach-definition-auto-4a6ca6d5ba»(Definition)
  
  Missing owner metadata.
- «12banach-definition-auto-5b8f6e3fc7»(Definition)
  
  Missing owner metadata.
- «12banach-definition-auto-5dcf314007»(Definition)
  
  Missing owner metadata.
- «12banach-definition-auto-5f93b3dba8»(Definition)
  
  Missing owner metadata.
- «12banach-definition-auto-7bd2c77569»(Definition)
  
  Missing owner metadata.
- «12banach-definition-auto-84ba8f01ee»(Definition)
  
  Missing owner metadata.
- «12banach-definition-auto-c460ce1e9c»(Definition)
  
  Missing owner metadata.
- «12banach-definition-auto-de1b622eef»(Definition)
  
  Missing owner metadata.
- «12banach-example-auto-ccfbaa66df»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «12banach-example-auto-df4f8139d9»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «12banach-example-auto-e2034d98b1»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «12banach-lemma-auto-73df993c86»(Lemma)
  
  Missing owner metadata.
- «12banach-lemma-auto-b357918422»(Lemma)
  
  Missing owner metadata.
- «12banach-proposition-auto-5ac0dfc586»(Proposition)
  
  Missing owner metadata.
- «12banach-proposition-auto-92e612b4f2»(Proposition)
  
  Missing owner metadata.
- «12banach-proposition-auto-a113ca5409»(Proposition)
  
  Missing owner metadata.
- «12banach-proposition-auto-abba30c310»(Proposition)
  
  Missing owner metadata.
- «12banach-theorem-auto-426c0c8fac»(Theorem)
  
  Missing owner metadata.
- «12banach-theorem-auto-a903d22d15»(Theorem)
  
  Missing owner metadata.
- «12banach-theorem-auto-e5bd950a27»(Theorem)
  
  Missing owner metadata.
- «12banach-theorem-auto-fde4450b71»(Theorem)
  
  Missing owner metadata.
- «13hilbert-corollary-auto-28874ae3ee»(Corollary)
  
  Missing owner metadata.
- «13hilbert-corollary-auto-720f5d0c1a»(Corollary)
  
  Missing owner metadata.
- «13hilbert-definition-auto-1f8d0f9182»(Definition)
  
  Missing owner metadata.
- «13hilbert-definition-auto-259d3f6153»(Definition)
  
  Missing owner metadata.
- «13hilbert-definition-auto-2a28e9ed50»(Definition)
  
  Missing owner metadata.
- «13hilbert-definition-auto-32a874c6ce»(Definition)
  
  Missing owner metadata.
- «13hilbert-definition-auto-49c9982d69»(Definition)
  
  Missing owner metadata.
- «13hilbert-definition-auto-5d4ee5bb89»(Definition)
  
  Missing owner metadata.
- «13hilbert-definition-auto-ab9f9cd0e4»(Definition)
  
  Missing owner metadata.
- «13hilbert-definition-auto-aed2a40a16»(Definition)
  
  Missing owner metadata.
- «13hilbert-example-auto-05b528424a»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «13hilbert-example-auto-137bd3a060»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «13hilbert-example-auto-450f5a5852»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «13hilbert-example-auto-fed54eefed»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «13hilbert-proposition-auto-3d898884b4»(Proposition)
  
  Missing owner metadata.
- «13hilbert-proposition-auto-c72a2bf678»(Proposition)
  
  Missing owner metadata.
- «13hilbert-proposition-auto-d8707bd73b»(Proposition)
  
  Missing owner metadata.
- «13hilbert-proposition-auto-dd72d110eb»(Proposition)
  
  Missing owner metadata.
- «13hilbert-theorem-auto-8638e2a37f»(Theorem)
  
  Missing owner metadata.
- «13hilbert-theorem-auto-921927e104»(Theorem)
  
  Missing owner metadata.
- «13hilbert-theorem-auto-c0d78cf6a1»(Theorem)
  
  Missing owner metadata.
- «13hilbert-theorem-auto-ea6e5c2177»(Theorem)
  
  Missing owner metadata.
- «14linear-opr-corollary-auto-3cbe01ecb7»(Corollary)
  
  Missing owner metadata.
- «14linear-opr-definition-auto-0b94de9aeb»(Definition)
  
  Missing owner metadata.
- «14linear-opr-definition-auto-47597d0b80»(Definition)
  
  Missing owner metadata.
- «14linear-opr-definition-auto-5c90b2f36a»(Definition)
  
  Missing owner metadata.
- «14linear-opr-definition-auto-6db1d33ddc»(Definition)
  
  Missing owner metadata.
- «14linear-opr-definition-auto-fd375cb2c0»(Definition)
  
  Missing owner metadata.
- «14linear-opr-definition-auto-fe652db767»(Definition)
  
  Missing owner metadata.
- «14linear-opr-example-auto-0f685b2c35»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «14linear-opr-example-auto-cf9db84d71»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «14linear-opr-example-auto-f81b4cda27»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «14linear-opr-proposition-auto-100e285ffb»(Proposition)
  
  Missing owner metadata.
- «14linear-opr-proposition-auto-6b36a220ec»(Proposition)
  
  Missing owner metadata.
- «14linear-opr-proposition-auto-fa8dc9caaf»(Proposition)
  
  Missing owner metadata.
- «14linear-opr-theorem-auto-1ee719cdc3»(Theorem)
  
  Missing owner metadata.
- «14linear-opr-theorem-auto-a02e256b7f»(Theorem)
  
  Missing owner metadata.
- «cor:L1-convergence-in-measure»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_integrable_abs
- «cor:ae-limit-measurable»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_of_ae_tendsto_real
  - NoteKsk.Chapter07.measurable_of_ae_tendsto_ereal
- «cor:affine-change-of-variables»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
  - NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
- «cor:beppo-levi-l1»(Corollary)
  
  Missing owner metadata.
- «cor:bounded-convergence»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter10.tendsto_integral_of_bounded_convergence
- «cor:countable-lebesgue-null»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.countable_lebesgueMeasurable
  - NoteKsk.Chapter05.countable_lebesgueMeasure_eq_zero
- «cor:dominated-convergence-l1»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence
- «cor:dominated-integrability»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.dominated_integrability
- «cor:inner-measure-via-compact-set»(Corollary)
  
  Missing owner metadata.
- «cor:integrable-finite-ae»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.integrable_real_finite_ae
- «cor:integral-finite-sum»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_finset_sum
- «cor:interval-outer-measure-split»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter04.lambdaInner_eq_lambdaStar_iff_boxVolume_eq
- «cor:iterated-integral-exchange»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter11.integral_integral_swap
- «cor:l1-absolutely-summable-series-termwise-integration»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter10.integral_tsum_eq_tsum_integral_of_summable_integral_norm
  - NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm
- «cor:lebesgue-caratheodory-equivalence»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurable_iff_caratheodory
- «cor:lebesgue-measurable-set-operations»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «cor:local-measurable-set-operations»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.localLebesgueMeasurable_inter
  - NoteKsk.Chapter05.localLebesgueMeasurable_diff
- «cor:measurable-algebra-operations»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (7)
- «cor:nonnegative-series-termwise-integration»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter10.lintegral_tsum
- «cor:riemann-integral-indicator-jordan-measure»(Corollary)
  
  Missing owner metadata.
  
  tag: notready
  Associated lean decls (1)
  - NoteKsk.Chapter02.riemannIntegral_indicator_eq_jordanMeasure
- «cor:volume-under-affine-map»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
- «def:L1-space»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.L1Space
- «def:ae-convergence»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.AEConvergesOn
- «def:ae-prop»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.AlmostEverywhereOn
- «def:algebra-generated-by-semiring»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.algebraGeneratedBySemiring
- «def:borel-measure»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter06.borelMeasure
- «def:borel-sigma-algebra»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter06.borelSigmaAlgebra
- «def:caratheodory-condition»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «def:completion»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «def:countably-additive-measure»(Definition)
  
  Missing owner metadata.
  
  tag: mathlibok
  Associated lean decls (1)
  - MeasureTheory.Measure
- «def:darboux-integrable»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter01.DarbouxIntegrableOn
  - NoteKsk.Chapter01.darbouxIntegral
- «def:darboux-sums»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:darboux-upper-lower-integral»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:finite-additive-family»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - NoteKsk.FiniteAdditiveFamily
  - MeasureTheory.IsSetRing
- «def:generated-sigma-algebra»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «def:integral-over-subset»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.setLintegralNN
  - NoteKsk.Chapter08.setLintegralNN_eq_indicator
- «def:jordan-box»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (9)
- «def:jordan-elementary-set»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.IsElementarySet
  - NoteKsk.elementaryVolume
- «def:jordan-measurable»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:jordan-null-set»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.JordanNullSet
  - NoteKsk.Chapter02.jordanMeasure_eq_zero_of_null
- «def:jordan-one-dimensional-interval»(Definition)
  
  Missing owner metadata.
- «def:jordan-outer-inner-measure»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.jordanOuterMeasure
  - NoteKsk.jordanInnerMeasure
- «def:lebesgue-caratheodory-measurable»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable
- «def:lebesgue-inner-measure»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter04.lambdaInner
- «def:lebesgue-integrable-function»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:lebesgue-measurable-function»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «def:lebesgue-measurable-local»(Definition)
  
  Missing owner metadata.
  Associated lean decls (6)
- «def:lebesgue-outer-measure»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (9)
- «def:measurable-function-space-notation»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «def:measurable-map»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.MeasurableMap
  - NoteKsk.Chapter07.measurableMap_iff_preimage
- «def:measurable-space»(Definition)
  
  Missing owner metadata.
  
  tag: mathlibok
  Associated lean decls (2)
  - MeasurableSpace
  - NoteKsk.SigmaAlgebra
- «def:measure»(Definition)
  
  Missing owner metadata.
  
  tag: mathlibok
  Associated lean decls (3)
- «def:nonnegative-lebesgue-integral»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.lintegralNN
  - NoteKsk.Chapter08.lintegralNN_def
- «def:nonnegative-simple-function»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.SimpleNNFun
  - NoteKsk.Chapter08.simpleNNFun_measurable
- «def:outer-measure-generated-by-premeasure»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure
- «def:outer-measure»(Definition)
  
  Missing owner metadata.
  
  tag: mathlibok
  Associated lean decls (4)
- «def:pointwise-limits»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:positive-negative-parts»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:premeasure-on-algebra»(Definition)
  
  Missing owner metadata.
  
  tag: mathlibok
  Associated lean decls (2)
  - MeasureTheory.AddContent
  - NoteKsk.IsPremeasureOnSemiring
- «def:premeasure-on-semiring»(Definition)
  
  Missing owner metadata.
  
  tag: mathlibok
  Associated lean decls (2)
  - MeasureTheory.AddContent
  - NoteKsk.IsPremeasureOnSemiring
- «def:riemann-integrable»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «def:riemann-interval-partition»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (5)
- «def:riemann-sum»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter01.IntervalPartition.IsTagged
  - NoteKsk.Chapter01.riemannSum
- «def:ring-of-sets»(Definition)
  
  Missing owner metadata.
- «def:sections»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:semiring»(Definition)
  
  Missing owner metadata.
  
  tag: mathlibok
  Associated lean decls (1)
  - MeasureTheory.IsSetSemiring
- «def:sigma-algebra»(Definition)
  
  Missing owner metadata.
  
  tag: mathlibok
  Associated lean decls (6)
- «def:sigma-finite-measure»(Definition)
  
  Missing owner metadata.
  
  tag: mathlibok
  Associated lean decls (3)
- «def:simple-function-integral»(Definition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.simpleLintegral
  - NoteKsk.Chapter08.lintegralNN_eq_simple
- «ex:boundary-elementary-jordan-null»(Proposition)
  
  Missing owner metadata.
  
  tag: notreadytag: example
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_boundary_elementary
- «ex:change-order-triangle»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «ex:continuous-function-measurable»(Proposition)
  
  Missing owner metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter07.continuous_borelMeasurable
- «ex:continuous-riemann-integrable»(Proposition)
  
  Missing owner metadata.
  
  tag: notreadytag: example
  Associated lean decls (1)
  - NoteKsk.Chapter01.riemannIntegrable_of_continuousOn
- «ex:counting-measure»(Proposition)
  
  Missing owner metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter06.countingMeasure_apply
- «ex:dirac-measure»(Proposition)
  
  Missing owner metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter06.diracMeasure_apply
- «ex:dirichlet-not-riemann-integrable»(Proposition)
  
  Missing owner metadata.
  
  tag: notreadytag: example
  Associated lean decls (2)
  - NoteKsk.Chapter01.dirichlet
  - NoteKsk.Chapter01.not_riemannIntegrable_dirichlet
- «ex:discrete-premeasures»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «ex:discrete-semirings»(Proposition)
  
  Missing owner metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter06.powerset_isSetSemiring
- «ex:elementary-set-jordan-measurable»(Proposition)
  
  Missing owner metadata.
  
  tag: notreadytag: example
  Associated lean decls (2)
  - NoteKsk.Chapter02.elementarySet_jordanMeasurable
  - NoteKsk.Chapter02.jordanMeasure_elementarySet
- «ex:finite-partition-semiring»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «ex:finite-set-jordan-null»(Proposition)
  
  Missing owner metadata.
  
  tag: notreadytag: example
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_finite
- «ex:indicator-function-measurable»(Proposition)
  
  Missing owner metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter07.indicator_measurable
- «ex:lebesgue-measure-from-caratheodory-hahn»(Proposition)
  
  Missing owner metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter06.lambdaStar_eq_inducedOuterMeasureFromBoxes
- «ex:left-half-open-semiring»(Proposition)
  
  Missing owner metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter06.leftHalfOpenBox_isSetSemiring
- «ex:parallelogram-area»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «ex:piecewise-constant-riemann-integrable»(Proposition)
  
  Missing owner metadata.
  
  tag: notreadytag: example
  Associated lean decls (2)
  - NoteKsk.Chapter01.PiecewiseConstantOnInterval
  - NoteKsk.Chapter01.riemannIntegrable_piecewiseConstant
- «ex:piecewise-continuous-riemann-integrable»(Proposition)
  
  Missing owner metadata.
  
  tag: notreadytag: example
  Associated lean decls (2)
  - NoteKsk.Chapter01.PiecewiseContinuousOnInterval
  - NoteKsk.Chapter01.riemannIntegrable_piecewiseContinuous
- «ex:polar-coordinates»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «ex:product-function-tonelli»(Proposition)
  
  Missing owner metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter11.lintegral_prod_mul
- «ex:riemann-integral-constant»(Proposition)
  
  Missing owner metadata.
  
  tag: notreadytag: example
  Associated lean decls (2)
  - NoteKsk.Chapter01.riemannIntegrable_const
  - NoteKsk.Chapter01.riemannIntegral_const
- «ex:riemann-integral-identity»(Proposition)
  
  Missing owner metadata.
  
  tag: notreadytag: example
  Associated lean decls (2)
  - NoteKsk.Chapter01.riemannIntegrable_id
  - NoteKsk.Chapter01.riemannIntegral_id
- «ex:singleton-jordan-null»(Proposition)
  
  Missing owner metadata.
  
  tag: notreadytag: example
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_singleton
- «ex:triangle-area-tonelli»(Proposition)
  
  Missing owner metadata.
  
  tag: example
- «ex:unbounded-not-riemann-integrable»(Proposition)
  
  Missing owner metadata.
  
  tag: notreadytag: example
  Associated lean decls (1)
  - NoteKsk.Chapter01.not_riemannIntegrable_of_unboundedOn
- «lem:borel-eRR»(Lemma)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter07.borel_eReal_eq_generate_Iic_real
- «lem:commute-induce-generate-sigma-algebra»(Lemma)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter07.comap_generatedSigmaAlgebra
  - NoteKsk.Chapter07.measurable_to_generatedSigmaAlgebra
- «lem:compact-splits-outer-measure»(Lemma)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter03.compact_splits_lambdaStar
- «lem:finite-open-compact-split»(Lemma)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter03.finiteOpen_compact_split
- «lem:finite-open-inner-compact»(Lemma)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter03.finiteOpen_innerCompact_exists
- «lem:finite-outer-compact-criterion»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter05.finiteOuter_compact_approx_criterion
  - NoteKsk.Chapter05.finiteOuter_open_approx_criterion
- «lem:jordan-grid-subdivision»(Lemma)
  
  Missing owner metadata.
  
  tag: notready
  Associated lean decls (2)
  - NoteKsk.Chapter02.elementarySet_finite_union_leftHalfOpenBoxes
  - NoteKsk.Chapter02.elementaryVolume_eq_sum_boxVolume
- «lem:jordan-outer-finite-subadditive»(Lemma)
  
  Missing owner metadata.
  
  tag: notready
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanOuterMeasure_finite_subadditive
- «lem:lebesgue-measurable-caratheodory-finite»(Lemma)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurable_caratheodory_finite
- «lem:lebesgue-measure-finite-additivity»(Lemma)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_union_add
- «lem:lebesgue-measure-limit»(Lemma)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_iSup_of_mono
- «lem:local-measurable-complement»(Lemma)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «lem:local-measurable-finite-union-additivity»(Lemma)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.localLebesgueMeasurable_union
  - NoteKsk.Chapter05.localLebesgueMeasurable_union_additive
- «lem:positive-distance-additive»(Lemma)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter03.PositiveDistanceApart
  - NoteKsk.Chapter03.lambdaStar_union_of_positiveDistanceApart
- «lem:simple-function-approximation»(Lemma)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «prop:L1-space-structure»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (7)
- «prop:ae-equality-equivalence»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.AEEqualOn
  - NoteKsk.Chapter07.aeEqualOn_equivalence
- «prop:ae-modification-measurable»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter07.measurable_of_ae_eq_complete
- «prop:chebyshev-inequality»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_integrable_abs
- «prop:compact-inner-outer-equal»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter04.lambdaInner_eq_lambdaStar_of_isCompact
  - NoteKsk.Chapter04.lambdaInner_eq_zero_of_lambdaStar_eq_zero
- «prop:integrable-as-difference»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (5)
- «prop:integral-absolute-value-bound»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter09.abs_integral_le_integral_abs
  - NoteKsk.Chapter09.norm_integral_le_integral_norm
- «prop:integral-additivity»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «prop:integral-ae-invariance»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «prop:integral-bound-by-constants»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_bounds_of_ae_const_le
- «prop:integral-disjoint-additivity»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter09.setIntegral_union_of_disjoint
  - NoteKsk.Chapter09.setIntegral_union_of_disjoint_of_integrable
- «prop:integral-homogeneity»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter09.integral_const_mul_real
  - NoteKsk.Chapter09.integral_smul
- «prop:integral-monotonicity»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter09.integral_mono_ae_real
  - NoteKsk.Chapter09.integral_mono_real
- «prop:integral-representation-independence»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_eq_sub_of_ae_eq_sub
- «prop:integral-zero-iff-ae-zero»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_abs_eq_zero_iff_ae_eq_zero
- «prop:integral-zero-on-null-set»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter09.integral_eq_zero_of_measure_univ_zero
  - NoteKsk.Chapter09.setIntegral_eq_zero_of_measure_zero
- «prop:interval-outer-measure-volume»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (6)
- «prop:inverse-image-basic»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «prop:inverse-image-sigma-algebra»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter07.inducedMeasurableSpace
  - NoteKsk.Chapter07.inducedMeasurableSpace_measurable
- «prop:jordan-inner-le-outer»(Proposition)
  
  Missing owner metadata.
  
  tag: notready
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanInnerMeasure_le_jordanOuterMeasure
- «prop:jordan-null-set-measurable»(Proposition)
  
  Missing owner metadata.
  
  tag: notready
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_jordanMeasurable
- «prop:lebesgue-global-local»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurableSet_windows
- «prop:lebesgue-inner-basic»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «prop:lebesgue-measure-nonnegative»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.lebesgueMeasure_empty
  - NoteKsk.Chapter05.lebesgueMeasure_nonneg
- «prop:lebesgue-measure-translation-invariant»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.lebesgueMeasurableSet_translate
  - NoteKsk.Chapter05.lebesgueMeasure_translate
- «prop:lebesgue-outer-translation-invariant»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter03.lambdaStar_translate
- «prop:louter-le-jouter»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter03.lambdaStar_le_jordanOuterMeasure
- «prop:measurable-comparison-sets»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «prop:measurable-countable-sup-inf»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_pointwiseSup
  - NoteKsk.Chapter07.measurable_pointwiseInf
- «prop:measurable-limsup-liminf»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «prop:measurable-reciprocal»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «prop:measurable-vector-map»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter07.measurable_vector_map
- «prop:nonnegative-chebyshev-inequality»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_lintegral
- «prop:nonnegative-integral-ae-invariance»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.lintegralNN_congr_ae
- «prop:nonnegative-integral-basic»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «prop:nonnegative-integral-disjoint-additivity»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.setLintegralNN_disjoint_union
- «prop:nonnegative-integral-zero-iff-ae-zero»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.lintegralNN_eq_zero_iff_ae_eq_zero
- «prop:null-set-integral-nonnegative»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.setLintegralNN_eq_zero_of_measure_zero
- «prop:null-set-integral-signed»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter08.integrableOn_of_measure_zero
  - NoteKsk.Chapter08.setIntegral_eq_zero_of_measure_zero
- «prop:positive-negative-basic-identities»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (7)
- «prop:signed-integral-ae-invariance»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter08.signed_integral_congr_ae
  - NoteKsk.Chapter08.integral_respects_ae_representatives
- «prop:simple-function-integral-basic»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (5)
- «prop:simple-function-integral-well-defined»(Proposition)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.simpleLintegral_congr
- «thm:algebra-generated-by-semiring»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter06.algebraGeneratedBySemiring_isSetRing
  - NoteKsk.Chapter06.algebraGeneratedBySemiring_measurable
- «thm:banach-tarski»(Theorem)
  
  Missing owner metadata.
- «thm:borel-sets-are-lebesgue-measurable»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter06.borelSet_lebesgueMeasurable
- «thm:caratheodory-hahn-extension»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (5)
- «thm:caratheodory-implies-lebesgue-measurable»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.caratheodory_implies_lebesgueMeasurable
- «thm:caratheodory-theorem»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (8)
- «thm:cavalieri-product-measure»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «thm:change-of-variables-diffeomorphism»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
  - NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
- «thm:continuity-under-integral-sign»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter10.continuous_integral_of_dominated
  - NoteKsk.Chapter10.continuousAt_integral_of_dominated
- «thm:countable-outer-measure-zero»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter03.lambdaStar_singleton
  - NoteKsk.Chapter03.lambdaStar_countable_eq_zero
- «thm:differentiation-under-integral-sign»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter10.hasFDerivAt_integral_under_dominated_loc_of_lip
  - NoteKsk.Chapter10.hasDerivAt_integral_under_dominated_loc_of_lip
- «thm:dominated-convergence»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter10.integrable_limit_of_dominated_convergence
  - NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence
- «thm:dominated-series-termwise-integration»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter10.hasSum_integral_of_dominated_convergence
  - NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm
- «thm:fatou-lemma»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter10.fatou_lintegral
  - NoteKsk.Chapter10.fatou_lintegral_atTop
- «thm:finite-outer-measurable-iff-inner-outer»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- «thm:fubini»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (5)
- «thm:inner-measure-via-interval»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter04.lambdaInner_eq_boxVolume_sub_lambdaStar_diff
- «thm:inner-measure-via-open-set»(Theorem)
  
  Missing owner metadata.
- «thm:integrable-iff-absolute»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter08.integrable_norm
  - NoteKsk.Chapter08.lebesgueIntegrable_iff_abs
- «thm:integral-absolute-continuity»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «thm:jordan-elementary-volume-properties»(Theorem)
  
  Missing owner metadata.
  
  tag: notready
  Associated lean decls (5)
- «thm:jordan-inner-lebesgue-inner»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter04.jordanInnerMeasure_le_lambdaInner
- «thm:jordan-measurable-criterion»(Theorem)
  
  Missing owner metadata.
  
  tag: notready
  Associated lean decls (2)
  - NoteKsk.Chapter02.jordanMeasurable_iff_boundary_null
  - NoteKsk.Chapter02.jordanMeasurable_iff_indicator_riemannIntegrable
- «thm:jordan-measurable-lebesgue»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.jordanMeasurable_lebesgueMeasurable
  - NoteKsk.Chapter05.lebesgueMeasure_eq_jordanMeasure
- «thm:jordan-measurable-set-operations»(Theorem)
  
  Missing owner metadata.
  
  tag: notready
  Associated lean decls (3)
- «thm:jordan-measure-properties»(Theorem)
  
  Missing owner metadata.
  
  tag: notready
  Associated lean decls (3)
- «thm:lebesgue-integral-basic-formulas»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (9)
- «thm:lebesgue-measurable-function-criterion»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_ereal_criterion_all_thresholds
  - NoteKsk.Chapter07.measurable_ereal_real_level_criterion
- «thm:lebesgue-measurable-implies-caratheodory»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurable_implies_caratheodory
- «thm:lebesgue-measurable-sigma-algebra»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «thm:lebesgue-measure-basic»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.lebesgueMeasure_mono
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_le_tsum
- «thm:lebesgue-measure-completion-of-borel»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «thm:lebesgue-measure-continuity-from-above»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iInter_eq_iInf_of_antitone
- «thm:lebesgue-measure-continuity-from-below»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_iSup_of_mono
- «thm:lebesgue-measure-countable-additivity»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_tsum
- «thm:lebesgue-measure-inner-regularity»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_innerRegular
- «thm:lebesgue-measure-outer-regularity»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_outerRegular
- «thm:lebesgue-null-measurable»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «thm:lebesgue-outer-measure»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (5)
- «thm:lebesgue-outer-regularity-open»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter03.lambdaStarByOpenSupersets
  - NoteKsk.Chapter03.lambdaStar_outerRegular_open
- «thm:local-measurable-sigma-algebra»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.localLebesgueMeasurable_iUnion
  - NoteKsk.Chapter05.localLebesgueMeasurable_iUnion_additive
- «thm:measurable-continuous-composition»(Corollary)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_continuous_comp
  - NoteKsk.Chapter07.measurable_continuous_real_comp
- «thm:measurable-map-composition»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter07.measurable_comp
- «thm:monotone-convergence»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «thm:nonnegative-integral-simple-approximation»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «thm:open-closed-lebesgue-measurable»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.isClosed_lebesgueMeasurable
  - NoteKsk.Chapter05.isOpen_lebesgueMeasurable
- «thm:outer-measure-from-premeasure»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «thm:polar-coordinates-rn»(Theorem)
  
  Missing owner metadata.
- «thm:premeasure-extension-to-algebra»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «thm:riemann-darboux-equivalence»(Theorem)
  
  Missing owner metadata.
  
  tag: notready
  Associated lean decls (2)
  - NoteKsk.Chapter01.riemann_integrable_iff_darboux_integrable
  - NoteKsk.Chapter01.riemannIntegral_eq_darbouxIntegral
- «thm:riemann-ftc»(Theorem)
  
  Missing owner metadata.
  
  tag: notready
  Associated lean decls (1)
  - NoteKsk.Chapter01.fundamental_theorem_of_calculus_for_riemann
- «thm:riemann-implies-lebesgue-integrable»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.boxRiemann_integrableOn_and_integral_eq_of_bounded_aeContinuous
- «thm:riemann-sums-tendsto-integral»(Theorem)
  
  Missing owner metadata.
  
  tag: notready
  Associated lean decls (1)
  - NoteKsk.Chapter01.riemann_sums_tendsto_integral
- «thm:sections-measurable-general»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (4)
- «thm:solovay-model»(Theorem)
  
  Missing owner metadata.
- «thm:tonelli»(Theorem)
  
  Missing owner metadata.
  
  tag: leanok
  Associated lean decls (3)
- «thm:vitali-nonmeasurable»(Theorem)
  
  Missing owner metadata.

Missing effort (307)

«01riemann-example-auto-4910acf622»(Proposition)

Missing effort metadata.

tag: example
«01riemann-example-auto-4bf36b1bd4»(Proposition)

Missing effort metadata.

tag: example
«01riemann-example-auto-7828e2d268»(Proposition)

Missing effort metadata.

tag: example
«01riemann-theorem-auto-5b3744507b»(Theorem)

Missing effort metadata.
«01riemann-theorem-auto-b4a925f916»(Theorem)

Missing effort metadata.
«02jordan02-definition-auto-09fd3f3928»(Definition)

Missing effort metadata.
«02jordan02-definition-auto-11f0199ce8»(Definition)

Missing effort metadata.
«02jordan02-definition-auto-5793cf4a96»(Definition)

Missing effort metadata.
«02jordan02-example-auto-09f40721a5»(Proposition)

Missing effort metadata.

tag: example
«02jordan02-example-auto-3a4895ebda»(Proposition)

Missing effort metadata.

tag: example
Show all 297 more entries missing effort
- «02jordan02-example-auto-47516d5758»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «02jordan02-example-auto-7771caf6bf»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «02jordan02-example-auto-9ce4c86a8e»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «02jordan02-example-auto-fa3e18599e»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «02jordan02-proposition-auto-2ff693ea48»(Proposition)
  
  Missing effort metadata.
- «02jordan02-theorem-auto-cfc2847f0d»(Theorem)
  
  Missing effort metadata.
- «03lebesgue-outer-definition-auto-8d32644e77»(Definition)
  
  Missing effort metadata.
- «03lebesgue-outer-definition-auto-aaf4aa3003»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter03.IsOuterMeasureFunction
  - MeasureTheory.OuterMeasure
- «03lebesgue-outer-example-auto-56b6bf606f»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «03lebesgue-outer-example-auto-ee91c30bff»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «03lebesgue-outer-proposition-auto-07f01b1f71»(Proposition)
  
  Missing effort metadata.
- «03lebesgue-outer-proposition-auto-e312ac0c17»(Proposition)
  
  Missing effort metadata.
- «03lebesgue-outer-theorem-auto-2e7c2024ee»(Theorem)
  
  Missing effort metadata.
- «03lebesgue-outer-theorem-auto-bcfe17076e»(Theorem)
  
  Missing effort metadata.
- «04lebesgue-inner-corollary-auto-37d04eb610»(Corollary)
  
  Missing effort metadata.
- «04lebesgue-inner-example-auto-0225bc1c45»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «05lebesgue03-definition-auto-ab11a0a94e»(Definition)
  
  Missing effort metadata.
- «05lebesgue03-example-auto-3b737bca05»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «06caratheodory02-definition-auto-2113b228f0»(Definition)
  
  Missing effort metadata.
- «06caratheodory02-definition-auto-86b8c96217»(Definition)
  
  Missing effort metadata.
- «06caratheodory02-example-auto-70bceb8d84»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «07mble-funcs-example-auto-2838d2b582»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «08lintegral-example-auto-08d592162e»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «08lintegral-example-auto-985634d68c»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «08lintegral-example-auto-aab23f2012»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «08lintegral-example-auto-ae9b38d1f9»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «09lintegral-prop-example-auto-d3ad988065»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «10limits-example-auto-7371ef5f8f»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «10limits-example-auto-7455ac8402»(Proposition)
  
  Missing effort metadata.
  
  tag: example
  Associated lean decls (1)
  - NoteKsk.Chapter10.hasDerivAt_laplace_transform_of_dominated_loc_of_lip
- «10limits-example-auto-ef82d9de32»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «12banach-definition-auto-4a6ca6d5ba»(Definition)
  
  Missing effort metadata.
- «12banach-definition-auto-5b8f6e3fc7»(Definition)
  
  Missing effort metadata.
- «12banach-definition-auto-5dcf314007»(Definition)
  
  Missing effort metadata.
- «12banach-definition-auto-5f93b3dba8»(Definition)
  
  Missing effort metadata.
- «12banach-definition-auto-7bd2c77569»(Definition)
  
  Missing effort metadata.
- «12banach-definition-auto-84ba8f01ee»(Definition)
  
  Missing effort metadata.
- «12banach-definition-auto-c460ce1e9c»(Definition)
  
  Missing effort metadata.
- «12banach-definition-auto-de1b622eef»(Definition)
  
  Missing effort metadata.
- «12banach-example-auto-ccfbaa66df»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «12banach-example-auto-df4f8139d9»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «12banach-example-auto-e2034d98b1»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «12banach-lemma-auto-73df993c86»(Lemma)
  
  Missing effort metadata.
- «12banach-lemma-auto-b357918422»(Lemma)
  
  Missing effort metadata.
- «12banach-proposition-auto-5ac0dfc586»(Proposition)
  
  Missing effort metadata.
- «12banach-proposition-auto-92e612b4f2»(Proposition)
  
  Missing effort metadata.
- «12banach-proposition-auto-a113ca5409»(Proposition)
  
  Missing effort metadata.
- «12banach-proposition-auto-abba30c310»(Proposition)
  
  Missing effort metadata.
- «12banach-theorem-auto-426c0c8fac»(Theorem)
  
  Missing effort metadata.
- «12banach-theorem-auto-a903d22d15»(Theorem)
  
  Missing effort metadata.
- «12banach-theorem-auto-e5bd950a27»(Theorem)
  
  Missing effort metadata.
- «12banach-theorem-auto-fde4450b71»(Theorem)
  
  Missing effort metadata.
- «13hilbert-corollary-auto-28874ae3ee»(Corollary)
  
  Missing effort metadata.
- «13hilbert-corollary-auto-720f5d0c1a»(Corollary)
  
  Missing effort metadata.
- «13hilbert-definition-auto-1f8d0f9182»(Definition)
  
  Missing effort metadata.
- «13hilbert-definition-auto-259d3f6153»(Definition)
  
  Missing effort metadata.
- «13hilbert-definition-auto-2a28e9ed50»(Definition)
  
  Missing effort metadata.
- «13hilbert-definition-auto-32a874c6ce»(Definition)
  
  Missing effort metadata.
- «13hilbert-definition-auto-49c9982d69»(Definition)
  
  Missing effort metadata.
- «13hilbert-definition-auto-5d4ee5bb89»(Definition)
  
  Missing effort metadata.
- «13hilbert-definition-auto-ab9f9cd0e4»(Definition)
  
  Missing effort metadata.
- «13hilbert-definition-auto-aed2a40a16»(Definition)
  
  Missing effort metadata.
- «13hilbert-example-auto-05b528424a»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «13hilbert-example-auto-137bd3a060»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «13hilbert-example-auto-450f5a5852»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «13hilbert-example-auto-fed54eefed»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «13hilbert-proposition-auto-3d898884b4»(Proposition)
  
  Missing effort metadata.
- «13hilbert-proposition-auto-c72a2bf678»(Proposition)
  
  Missing effort metadata.
- «13hilbert-proposition-auto-d8707bd73b»(Proposition)
  
  Missing effort metadata.
- «13hilbert-proposition-auto-dd72d110eb»(Proposition)
  
  Missing effort metadata.
- «13hilbert-theorem-auto-8638e2a37f»(Theorem)
  
  Missing effort metadata.
- «13hilbert-theorem-auto-921927e104»(Theorem)
  
  Missing effort metadata.
- «13hilbert-theorem-auto-c0d78cf6a1»(Theorem)
  
  Missing effort metadata.
- «13hilbert-theorem-auto-ea6e5c2177»(Theorem)
  
  Missing effort metadata.
- «14linear-opr-corollary-auto-3cbe01ecb7»(Corollary)
  
  Missing effort metadata.
- «14linear-opr-definition-auto-0b94de9aeb»(Definition)
  
  Missing effort metadata.
- «14linear-opr-definition-auto-47597d0b80»(Definition)
  
  Missing effort metadata.
- «14linear-opr-definition-auto-5c90b2f36a»(Definition)
  
  Missing effort metadata.
- «14linear-opr-definition-auto-6db1d33ddc»(Definition)
  
  Missing effort metadata.
- «14linear-opr-definition-auto-fd375cb2c0»(Definition)
  
  Missing effort metadata.
- «14linear-opr-definition-auto-fe652db767»(Definition)
  
  Missing effort metadata.
- «14linear-opr-example-auto-0f685b2c35»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «14linear-opr-example-auto-cf9db84d71»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «14linear-opr-example-auto-f81b4cda27»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «14linear-opr-proposition-auto-100e285ffb»(Proposition)
  
  Missing effort metadata.
- «14linear-opr-proposition-auto-6b36a220ec»(Proposition)
  
  Missing effort metadata.
- «14linear-opr-proposition-auto-fa8dc9caaf»(Proposition)
  
  Missing effort metadata.
- «14linear-opr-theorem-auto-1ee719cdc3»(Theorem)
  
  Missing effort metadata.
- «14linear-opr-theorem-auto-a02e256b7f»(Theorem)
  
  Missing effort metadata.
- «cor:L1-convergence-in-measure»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_integrable_abs
- «cor:ae-limit-measurable»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_of_ae_tendsto_real
  - NoteKsk.Chapter07.measurable_of_ae_tendsto_ereal
- «cor:affine-change-of-variables»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
  - NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
- «cor:beppo-levi-l1»(Corollary)
  
  Missing effort metadata.
- «cor:bounded-convergence»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter10.tendsto_integral_of_bounded_convergence
- «cor:countable-lebesgue-null»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.countable_lebesgueMeasurable
  - NoteKsk.Chapter05.countable_lebesgueMeasure_eq_zero
- «cor:dominated-convergence-l1»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence
- «cor:dominated-integrability»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.dominated_integrability
- «cor:inner-measure-via-compact-set»(Corollary)
  
  Missing effort metadata.
- «cor:integrable-finite-ae»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.integrable_real_finite_ae
- «cor:integral-finite-sum»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_finset_sum
- «cor:interval-outer-measure-split»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter04.lambdaInner_eq_lambdaStar_iff_boxVolume_eq
- «cor:iterated-integral-exchange»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter11.integral_integral_swap
- «cor:l1-absolutely-summable-series-termwise-integration»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter10.integral_tsum_eq_tsum_integral_of_summable_integral_norm
  - NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm
- «cor:lebesgue-caratheodory-equivalence»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurable_iff_caratheodory
- «cor:lebesgue-measurable-set-operations»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «cor:local-measurable-set-operations»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.localLebesgueMeasurable_inter
  - NoteKsk.Chapter05.localLebesgueMeasurable_diff
- «cor:measurable-algebra-operations»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (7)
- «cor:nonnegative-series-termwise-integration»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter10.lintegral_tsum
- «cor:riemann-integral-indicator-jordan-measure»(Corollary)
  
  Missing effort metadata.
  
  tag: notready
  Associated lean decls (1)
  - NoteKsk.Chapter02.riemannIntegral_indicator_eq_jordanMeasure
- «cor:volume-under-affine-map»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
- «def:L1-space»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.L1Space
- «def:ae-convergence»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.AEConvergesOn
- «def:ae-prop»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.AlmostEverywhereOn
- «def:algebra-generated-by-semiring»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.algebraGeneratedBySemiring
- «def:borel-measure»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter06.borelMeasure
- «def:borel-sigma-algebra»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter06.borelSigmaAlgebra
- «def:caratheodory-condition»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «def:completion»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «def:countably-additive-measure»(Definition)
  
  Missing effort metadata.
  
  tag: mathlibok
  Associated lean decls (1)
  - MeasureTheory.Measure
- «def:darboux-integrable»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter01.DarbouxIntegrableOn
  - NoteKsk.Chapter01.darbouxIntegral
- «def:darboux-sums»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:darboux-upper-lower-integral»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:finite-additive-family»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - NoteKsk.FiniteAdditiveFamily
  - MeasureTheory.IsSetRing
- «def:generated-sigma-algebra»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «def:integral-over-subset»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.setLintegralNN
  - NoteKsk.Chapter08.setLintegralNN_eq_indicator
- «def:jordan-box»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (9)
- «def:jordan-elementary-set»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.IsElementarySet
  - NoteKsk.elementaryVolume
- «def:jordan-measurable»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:jordan-null-set»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.JordanNullSet
  - NoteKsk.Chapter02.jordanMeasure_eq_zero_of_null
- «def:jordan-one-dimensional-interval»(Definition)
  
  Missing effort metadata.
- «def:jordan-outer-inner-measure»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.jordanOuterMeasure
  - NoteKsk.jordanInnerMeasure
- «def:lebesgue-caratheodory-measurable»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable
- «def:lebesgue-inner-measure»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter04.lambdaInner
- «def:lebesgue-integrable-function»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:lebesgue-measurable-function»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «def:lebesgue-measurable-local»(Definition)
  
  Missing effort metadata.
  Associated lean decls (6)
- «def:lebesgue-outer-measure»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (9)
- «def:measurable-function-space-notation»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «def:measurable-map»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.MeasurableMap
  - NoteKsk.Chapter07.measurableMap_iff_preimage
- «def:measurable-space»(Definition)
  
  Missing effort metadata.
  
  tag: mathlibok
  Associated lean decls (2)
  - MeasurableSpace
  - NoteKsk.SigmaAlgebra
- «def:measure»(Definition)
  
  Missing effort metadata.
  
  tag: mathlibok
  Associated lean decls (3)
- «def:nonnegative-lebesgue-integral»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.lintegralNN
  - NoteKsk.Chapter08.lintegralNN_def
- «def:nonnegative-simple-function»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.SimpleNNFun
  - NoteKsk.Chapter08.simpleNNFun_measurable
- «def:outer-measure-generated-by-premeasure»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure
- «def:outer-measure»(Definition)
  
  Missing effort metadata.
  
  tag: mathlibok
  Associated lean decls (4)
- «def:pointwise-limits»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:positive-negative-parts»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:premeasure-on-algebra»(Definition)
  
  Missing effort metadata.
  
  tag: mathlibok
  Associated lean decls (2)
  - MeasureTheory.AddContent
  - NoteKsk.IsPremeasureOnSemiring
- «def:premeasure-on-semiring»(Definition)
  
  Missing effort metadata.
  
  tag: mathlibok
  Associated lean decls (2)
  - MeasureTheory.AddContent
  - NoteKsk.IsPremeasureOnSemiring
- «def:riemann-integrable»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «def:riemann-interval-partition»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (5)
- «def:riemann-sum»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter01.IntervalPartition.IsTagged
  - NoteKsk.Chapter01.riemannSum
- «def:ring-of-sets»(Definition)
  
  Missing effort metadata.
- «def:sections»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «def:semiring»(Definition)
  
  Missing effort metadata.
  
  tag: mathlibok
  Associated lean decls (1)
  - MeasureTheory.IsSetSemiring
- «def:sigma-algebra»(Definition)
  
  Missing effort metadata.
  
  tag: mathlibok
  Associated lean decls (6)
- «def:sigma-finite-measure»(Definition)
  
  Missing effort metadata.
  
  tag: mathlibok
  Associated lean decls (3)
- «def:simple-function-integral»(Definition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.simpleLintegral
  - NoteKsk.Chapter08.lintegralNN_eq_simple
- «ex:boundary-elementary-jordan-null»(Proposition)
  
  Missing effort metadata.
  
  tag: notreadytag: example
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_boundary_elementary
- «ex:change-order-triangle»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «ex:continuous-function-measurable»(Proposition)
  
  Missing effort metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter07.continuous_borelMeasurable
- «ex:continuous-riemann-integrable»(Proposition)
  
  Missing effort metadata.
  
  tag: notreadytag: example
  Associated lean decls (1)
  - NoteKsk.Chapter01.riemannIntegrable_of_continuousOn
- «ex:counting-measure»(Proposition)
  
  Missing effort metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter06.countingMeasure_apply
- «ex:dirac-measure»(Proposition)
  
  Missing effort metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter06.diracMeasure_apply
- «ex:dirichlet-not-riemann-integrable»(Proposition)
  
  Missing effort metadata.
  
  tag: notreadytag: example
  Associated lean decls (2)
  - NoteKsk.Chapter01.dirichlet
  - NoteKsk.Chapter01.not_riemannIntegrable_dirichlet
- «ex:discrete-premeasures»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «ex:discrete-semirings»(Proposition)
  
  Missing effort metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter06.powerset_isSetSemiring
- «ex:elementary-set-jordan-measurable»(Proposition)
  
  Missing effort metadata.
  
  tag: notreadytag: example
  Associated lean decls (2)
  - NoteKsk.Chapter02.elementarySet_jordanMeasurable
  - NoteKsk.Chapter02.jordanMeasure_elementarySet
- «ex:finite-partition-semiring»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «ex:finite-set-jordan-null»(Proposition)
  
  Missing effort metadata.
  
  tag: notreadytag: example
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_finite
- «ex:indicator-function-measurable»(Proposition)
  
  Missing effort metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter07.indicator_measurable
- «ex:lebesgue-measure-from-caratheodory-hahn»(Proposition)
  
  Missing effort metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter06.lambdaStar_eq_inducedOuterMeasureFromBoxes
- «ex:left-half-open-semiring»(Proposition)
  
  Missing effort metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter06.leftHalfOpenBox_isSetSemiring
- «ex:parallelogram-area»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «ex:piecewise-constant-riemann-integrable»(Proposition)
  
  Missing effort metadata.
  
  tag: notreadytag: example
  Associated lean decls (2)
  - NoteKsk.Chapter01.PiecewiseConstantOnInterval
  - NoteKsk.Chapter01.riemannIntegrable_piecewiseConstant
- «ex:piecewise-continuous-riemann-integrable»(Proposition)
  
  Missing effort metadata.
  
  tag: notreadytag: example
  Associated lean decls (2)
  - NoteKsk.Chapter01.PiecewiseContinuousOnInterval
  - NoteKsk.Chapter01.riemannIntegrable_piecewiseContinuous
- «ex:polar-coordinates»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «ex:product-function-tonelli»(Proposition)
  
  Missing effort metadata.
  
  tag: leanoktag: example
  Associated lean decls (1)
  - NoteKsk.Chapter11.lintegral_prod_mul
- «ex:riemann-integral-constant»(Proposition)
  
  Missing effort metadata.
  
  tag: notreadytag: example
  Associated lean decls (2)
  - NoteKsk.Chapter01.riemannIntegrable_const
  - NoteKsk.Chapter01.riemannIntegral_const
- «ex:riemann-integral-identity»(Proposition)
  
  Missing effort metadata.
  
  tag: notreadytag: example
  Associated lean decls (2)
  - NoteKsk.Chapter01.riemannIntegrable_id
  - NoteKsk.Chapter01.riemannIntegral_id
- «ex:singleton-jordan-null»(Proposition)
  
  Missing effort metadata.
  
  tag: notreadytag: example
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_singleton
- «ex:triangle-area-tonelli»(Proposition)
  
  Missing effort metadata.
  
  tag: example
- «ex:unbounded-not-riemann-integrable»(Proposition)
  
  Missing effort metadata.
  
  tag: notreadytag: example
  Associated lean decls (1)
  - NoteKsk.Chapter01.not_riemannIntegrable_of_unboundedOn
- «lem:borel-eRR»(Lemma)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter07.borel_eReal_eq_generate_Iic_real
- «lem:commute-induce-generate-sigma-algebra»(Lemma)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter07.comap_generatedSigmaAlgebra
  - NoteKsk.Chapter07.measurable_to_generatedSigmaAlgebra
- «lem:compact-splits-outer-measure»(Lemma)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter03.compact_splits_lambdaStar
- «lem:finite-open-compact-split»(Lemma)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter03.finiteOpen_compact_split
- «lem:finite-open-inner-compact»(Lemma)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter03.finiteOpen_innerCompact_exists
- «lem:finite-outer-compact-criterion»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter05.finiteOuter_compact_approx_criterion
  - NoteKsk.Chapter05.finiteOuter_open_approx_criterion
- «lem:jordan-grid-subdivision»(Lemma)
  
  Missing effort metadata.
  
  tag: notready
  Associated lean decls (2)
  - NoteKsk.Chapter02.elementarySet_finite_union_leftHalfOpenBoxes
  - NoteKsk.Chapter02.elementaryVolume_eq_sum_boxVolume
- «lem:jordan-outer-finite-subadditive»(Lemma)
  
  Missing effort metadata.
  
  tag: notready
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanOuterMeasure_finite_subadditive
- «lem:lebesgue-measurable-caratheodory-finite»(Lemma)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurable_caratheodory_finite
- «lem:lebesgue-measure-finite-additivity»(Lemma)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_union_add
- «lem:lebesgue-measure-limit»(Lemma)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_iSup_of_mono
- «lem:local-measurable-complement»(Lemma)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «lem:local-measurable-finite-union-additivity»(Lemma)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.localLebesgueMeasurable_union
  - NoteKsk.Chapter05.localLebesgueMeasurable_union_additive
- «lem:positive-distance-additive»(Lemma)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter03.PositiveDistanceApart
  - NoteKsk.Chapter03.lambdaStar_union_of_positiveDistanceApart
- «lem:simple-function-approximation»(Lemma)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «prop:L1-space-structure»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (7)
- «prop:ae-equality-equivalence»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.AEEqualOn
  - NoteKsk.Chapter07.aeEqualOn_equivalence
- «prop:ae-modification-measurable»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter07.measurable_of_ae_eq_complete
- «prop:chebyshev-inequality»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_integrable_abs
- «prop:compact-inner-outer-equal»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter04.lambdaInner_eq_lambdaStar_of_isCompact
  - NoteKsk.Chapter04.lambdaInner_eq_zero_of_lambdaStar_eq_zero
- «prop:integrable-as-difference»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (5)
- «prop:integral-absolute-value-bound»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter09.abs_integral_le_integral_abs
  - NoteKsk.Chapter09.norm_integral_le_integral_norm
- «prop:integral-additivity»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «prop:integral-ae-invariance»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «prop:integral-bound-by-constants»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_bounds_of_ae_const_le
- «prop:integral-disjoint-additivity»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter09.setIntegral_union_of_disjoint
  - NoteKsk.Chapter09.setIntegral_union_of_disjoint_of_integrable
- «prop:integral-homogeneity»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter09.integral_const_mul_real
  - NoteKsk.Chapter09.integral_smul
- «prop:integral-monotonicity»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter09.integral_mono_ae_real
  - NoteKsk.Chapter09.integral_mono_real
- «prop:integral-representation-independence»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_eq_sub_of_ae_eq_sub
- «prop:integral-zero-iff-ae-zero»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_abs_eq_zero_iff_ae_eq_zero
- «prop:integral-zero-on-null-set»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter09.integral_eq_zero_of_measure_univ_zero
  - NoteKsk.Chapter09.setIntegral_eq_zero_of_measure_zero
- «prop:interval-outer-measure-volume»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (6)
- «prop:inverse-image-basic»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «prop:inverse-image-sigma-algebra»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter07.inducedMeasurableSpace
  - NoteKsk.Chapter07.inducedMeasurableSpace_measurable
- «prop:jordan-inner-le-outer»(Proposition)
  
  Missing effort metadata.
  
  tag: notready
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanInnerMeasure_le_jordanOuterMeasure
- «prop:jordan-null-set-measurable»(Proposition)
  
  Missing effort metadata.
  
  tag: notready
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_jordanMeasurable
- «prop:lebesgue-global-local»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurableSet_windows
- «prop:lebesgue-inner-basic»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «prop:lebesgue-measure-nonnegative»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.lebesgueMeasure_empty
  - NoteKsk.Chapter05.lebesgueMeasure_nonneg
- «prop:lebesgue-measure-translation-invariant»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.lebesgueMeasurableSet_translate
  - NoteKsk.Chapter05.lebesgueMeasure_translate
- «prop:lebesgue-outer-translation-invariant»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter03.lambdaStar_translate
- «prop:louter-le-jouter»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter03.lambdaStar_le_jordanOuterMeasure
- «prop:measurable-comparison-sets»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «prop:measurable-countable-sup-inf»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_pointwiseSup
  - NoteKsk.Chapter07.measurable_pointwiseInf
- «prop:measurable-limsup-liminf»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «prop:measurable-reciprocal»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «prop:measurable-vector-map»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter07.measurable_vector_map
- «prop:nonnegative-chebyshev-inequality»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_lintegral
- «prop:nonnegative-integral-ae-invariance»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.lintegralNN_congr_ae
- «prop:nonnegative-integral-basic»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «prop:nonnegative-integral-disjoint-additivity»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.setLintegralNN_disjoint_union
- «prop:nonnegative-integral-zero-iff-ae-zero»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.lintegralNN_eq_zero_iff_ae_eq_zero
- «prop:null-set-integral-nonnegative»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.setLintegralNN_eq_zero_of_measure_zero
- «prop:null-set-integral-signed»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter08.integrableOn_of_measure_zero
  - NoteKsk.Chapter08.setIntegral_eq_zero_of_measure_zero
- «prop:positive-negative-basic-identities»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (7)
- «prop:signed-integral-ae-invariance»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter08.signed_integral_congr_ae
  - NoteKsk.Chapter08.integral_respects_ae_representatives
- «prop:simple-function-integral-basic»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (5)
- «prop:simple-function-integral-well-defined»(Proposition)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.simpleLintegral_congr
- «thm:algebra-generated-by-semiring»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter06.algebraGeneratedBySemiring_isSetRing
  - NoteKsk.Chapter06.algebraGeneratedBySemiring_measurable
- «thm:banach-tarski»(Theorem)
  
  Missing effort metadata.
- «thm:borel-sets-are-lebesgue-measurable»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter06.borelSet_lebesgueMeasurable
- «thm:caratheodory-hahn-extension»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (5)
- «thm:caratheodory-implies-lebesgue-measurable»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.caratheodory_implies_lebesgueMeasurable
- «thm:caratheodory-theorem»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (8)
- «thm:cavalieri-product-measure»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «thm:change-of-variables-diffeomorphism»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
  - NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
- «thm:continuity-under-integral-sign»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter10.continuous_integral_of_dominated
  - NoteKsk.Chapter10.continuousAt_integral_of_dominated
- «thm:countable-outer-measure-zero»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter03.lambdaStar_singleton
  - NoteKsk.Chapter03.lambdaStar_countable_eq_zero
- «thm:differentiation-under-integral-sign»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter10.hasFDerivAt_integral_under_dominated_loc_of_lip
  - NoteKsk.Chapter10.hasDerivAt_integral_under_dominated_loc_of_lip
- «thm:dominated-convergence»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter10.integrable_limit_of_dominated_convergence
  - NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence
- «thm:dominated-series-termwise-integration»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter10.hasSum_integral_of_dominated_convergence
  - NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm
- «thm:fatou-lemma»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter10.fatou_lintegral
  - NoteKsk.Chapter10.fatou_lintegral_atTop
- «thm:finite-outer-measurable-iff-inner-outer»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- «thm:fubini»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (5)
- «thm:inner-measure-via-interval»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter04.lambdaInner_eq_boxVolume_sub_lambdaStar_diff
- «thm:inner-measure-via-open-set»(Theorem)
  
  Missing effort metadata.
- «thm:integrable-iff-absolute»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter08.integrable_norm
  - NoteKsk.Chapter08.lebesgueIntegrable_iff_abs
- «thm:integral-absolute-continuity»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «thm:jordan-elementary-volume-properties»(Theorem)
  
  Missing effort metadata.
  
  tag: notready
  Associated lean decls (5)
- «thm:jordan-inner-lebesgue-inner»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter04.jordanInnerMeasure_le_lambdaInner
- «thm:jordan-measurable-criterion»(Theorem)
  
  Missing effort metadata.
  
  tag: notready
  Associated lean decls (2)
  - NoteKsk.Chapter02.jordanMeasurable_iff_boundary_null
  - NoteKsk.Chapter02.jordanMeasurable_iff_indicator_riemannIntegrable
- «thm:jordan-measurable-lebesgue»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.jordanMeasurable_lebesgueMeasurable
  - NoteKsk.Chapter05.lebesgueMeasure_eq_jordanMeasure
- «thm:jordan-measurable-set-operations»(Theorem)
  
  Missing effort metadata.
  
  tag: notready
  Associated lean decls (3)
- «thm:jordan-measure-properties»(Theorem)
  
  Missing effort metadata.
  
  tag: notready
  Associated lean decls (3)
- «thm:lebesgue-integral-basic-formulas»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (9)
- «thm:lebesgue-measurable-function-criterion»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_ereal_criterion_all_thresholds
  - NoteKsk.Chapter07.measurable_ereal_real_level_criterion
- «thm:lebesgue-measurable-implies-caratheodory»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurable_implies_caratheodory
- «thm:lebesgue-measurable-sigma-algebra»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «thm:lebesgue-measure-basic»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.lebesgueMeasure_mono
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_le_tsum
- «thm:lebesgue-measure-completion-of-borel»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «thm:lebesgue-measure-continuity-from-above»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iInter_eq_iInf_of_antitone
- «thm:lebesgue-measure-continuity-from-below»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_iSup_of_mono
- «thm:lebesgue-measure-countable-additivity»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_tsum
- «thm:lebesgue-measure-inner-regularity»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_innerRegular
- «thm:lebesgue-measure-outer-regularity»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_outerRegular
- «thm:lebesgue-null-measurable»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «thm:lebesgue-outer-measure»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (5)
- «thm:lebesgue-outer-regularity-open»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter03.lambdaStarByOpenSupersets
  - NoteKsk.Chapter03.lambdaStar_outerRegular_open
- «thm:local-measurable-sigma-algebra»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.localLebesgueMeasurable_iUnion
  - NoteKsk.Chapter05.localLebesgueMeasurable_iUnion_additive
- «thm:measurable-continuous-composition»(Corollary)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_continuous_comp
  - NoteKsk.Chapter07.measurable_continuous_real_comp
- «thm:measurable-map-composition»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter07.measurable_comp
- «thm:monotone-convergence»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «thm:nonnegative-integral-simple-approximation»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «thm:open-closed-lebesgue-measurable»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (2)
  - NoteKsk.Chapter05.isClosed_lebesgueMeasurable
  - NoteKsk.Chapter05.isOpen_lebesgueMeasurable
- «thm:outer-measure-from-premeasure»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «thm:polar-coordinates-rn»(Theorem)
  
  Missing effort metadata.
- «thm:premeasure-extension-to-algebra»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «thm:riemann-darboux-equivalence»(Theorem)
  
  Missing effort metadata.
  
  tag: notready
  Associated lean decls (2)
  - NoteKsk.Chapter01.riemann_integrable_iff_darboux_integrable
  - NoteKsk.Chapter01.riemannIntegral_eq_darbouxIntegral
- «thm:riemann-ftc»(Theorem)
  
  Missing effort metadata.
  
  tag: notready
  Associated lean decls (1)
  - NoteKsk.Chapter01.fundamental_theorem_of_calculus_for_riemann
- «thm:riemann-implies-lebesgue-integrable»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (1)
  - NoteKsk.Chapter08.boxRiemann_integrableOn_and_integral_eq_of_bounded_aeContinuous
- «thm:riemann-sums-tendsto-integral»(Theorem)
  
  Missing effort metadata.
  
  tag: notready
  Associated lean decls (1)
  - NoteKsk.Chapter01.riemann_sums_tendsto_integral
- «thm:sections-measurable-general»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (4)
- «thm:solovay-model»(Theorem)
  
  Missing effort metadata.
- «thm:tonelli»(Theorem)
  
  Missing effort metadata.
  
  tag: leanok
  Associated lean decls (3)
- «thm:vitali-nonmeasurable»(Theorem)
  
  Missing effort metadata.

Untagged (88)

«01riemann-theorem-auto-5b3744507b»(Theorem)

Missing tag metadata.
«01riemann-theorem-auto-b4a925f916»(Theorem)

Missing tag metadata.
«02jordan02-definition-auto-09fd3f3928»(Definition)

Missing tag metadata.
«02jordan02-definition-auto-11f0199ce8»(Definition)

Missing tag metadata.
«02jordan02-definition-auto-5793cf4a96»(Definition)

Missing tag metadata.
«02jordan02-proposition-auto-2ff693ea48»(Proposition)

Missing tag metadata.
«02jordan02-theorem-auto-cfc2847f0d»(Theorem)

Missing tag metadata.
«03lebesgue-outer-definition-auto-8d32644e77»(Definition)

Missing tag metadata.
«03lebesgue-outer-definition-auto-aaf4aa3003»(Definition)

Missing tag metadata.
Associated lean decls (2)
- NoteKsk.Chapter03.IsOuterMeasureFunction
- MeasureTheory.OuterMeasure
«03lebesgue-outer-proposition-auto-07f01b1f71»(Proposition)

Missing tag metadata.
Show all 78 more untagged entries
- «03lebesgue-outer-proposition-auto-e312ac0c17»(Proposition)
  
  Missing tag metadata.
- «03lebesgue-outer-theorem-auto-2e7c2024ee»(Theorem)
  
  Missing tag metadata.
- «03lebesgue-outer-theorem-auto-bcfe17076e»(Theorem)
  
  Missing tag metadata.
- «04lebesgue-inner-corollary-auto-37d04eb610»(Corollary)
  
  Missing tag metadata.
- «05lebesgue03-definition-auto-ab11a0a94e»(Definition)
  
  Missing tag metadata.
- «06caratheodory02-definition-auto-2113b228f0»(Definition)
  
  Missing tag metadata.
- «06caratheodory02-definition-auto-86b8c96217»(Definition)
  
  Missing tag metadata.
- «12banach-definition-auto-4a6ca6d5ba»(Definition)
  
  Missing tag metadata.
- «12banach-definition-auto-5b8f6e3fc7»(Definition)
  
  Missing tag metadata.
- «12banach-definition-auto-5dcf314007»(Definition)
  
  Missing tag metadata.
- «12banach-definition-auto-5f93b3dba8»(Definition)
  
  Missing tag metadata.
- «12banach-definition-auto-7bd2c77569»(Definition)
  
  Missing tag metadata.
- «12banach-definition-auto-84ba8f01ee»(Definition)
  
  Missing tag metadata.
- «12banach-definition-auto-c460ce1e9c»(Definition)
  
  Missing tag metadata.
- «12banach-definition-auto-de1b622eef»(Definition)
  
  Missing tag metadata.
- «12banach-lemma-auto-73df993c86»(Lemma)
  
  Missing tag metadata.
- «12banach-lemma-auto-b357918422»(Lemma)
  
  Missing tag metadata.
- «12banach-proposition-auto-5ac0dfc586»(Proposition)
  
  Missing tag metadata.
- «12banach-proposition-auto-92e612b4f2»(Proposition)
  
  Missing tag metadata.
- «12banach-proposition-auto-a113ca5409»(Proposition)
  
  Missing tag metadata.
- «12banach-proposition-auto-abba30c310»(Proposition)
  
  Missing tag metadata.
- «12banach-theorem-auto-426c0c8fac»(Theorem)
  
  Missing tag metadata.
- «12banach-theorem-auto-a903d22d15»(Theorem)
  
  Missing tag metadata.
- «12banach-theorem-auto-e5bd950a27»(Theorem)
  
  Missing tag metadata.
- «12banach-theorem-auto-fde4450b71»(Theorem)
  
  Missing tag metadata.
- «13hilbert-corollary-auto-28874ae3ee»(Corollary)
  
  Missing tag metadata.
- «13hilbert-corollary-auto-720f5d0c1a»(Corollary)
  
  Missing tag metadata.
- «13hilbert-definition-auto-1f8d0f9182»(Definition)
  
  Missing tag metadata.
- «13hilbert-definition-auto-259d3f6153»(Definition)
  
  Missing tag metadata.
- «13hilbert-definition-auto-2a28e9ed50»(Definition)
  
  Missing tag metadata.
- «13hilbert-definition-auto-32a874c6ce»(Definition)
  
  Missing tag metadata.
- «13hilbert-definition-auto-49c9982d69»(Definition)
  
  Missing tag metadata.
- «13hilbert-definition-auto-5d4ee5bb89»(Definition)
  
  Missing tag metadata.
- «13hilbert-definition-auto-ab9f9cd0e4»(Definition)
  
  Missing tag metadata.
- «13hilbert-definition-auto-aed2a40a16»(Definition)
  
  Missing tag metadata.
- «13hilbert-proposition-auto-3d898884b4»(Proposition)
  
  Missing tag metadata.
- «13hilbert-proposition-auto-c72a2bf678»(Proposition)
  
  Missing tag metadata.
- «13hilbert-proposition-auto-d8707bd73b»(Proposition)
  
  Missing tag metadata.
- «13hilbert-proposition-auto-dd72d110eb»(Proposition)
  
  Missing tag metadata.
- «13hilbert-theorem-auto-8638e2a37f»(Theorem)
  
  Missing tag metadata.
- «13hilbert-theorem-auto-921927e104»(Theorem)
  
  Missing tag metadata.
- «13hilbert-theorem-auto-c0d78cf6a1»(Theorem)
  
  Missing tag metadata.
- «13hilbert-theorem-auto-ea6e5c2177»(Theorem)
  
  Missing tag metadata.
- «14linear-opr-corollary-auto-3cbe01ecb7»(Corollary)
  
  Missing tag metadata.
- «14linear-opr-definition-auto-0b94de9aeb»(Definition)
  
  Missing tag metadata.
- «14linear-opr-definition-auto-47597d0b80»(Definition)
  
  Missing tag metadata.
- «14linear-opr-definition-auto-5c90b2f36a»(Definition)
  
  Missing tag metadata.
- «14linear-opr-definition-auto-6db1d33ddc»(Definition)
  
  Missing tag metadata.
- «14linear-opr-definition-auto-fd375cb2c0»(Definition)
  
  Missing tag metadata.
- «14linear-opr-definition-auto-fe652db767»(Definition)
  
  Missing tag metadata.
- «14linear-opr-proposition-auto-100e285ffb»(Proposition)
  
  Missing tag metadata.
- «14linear-opr-proposition-auto-6b36a220ec»(Proposition)
  
  Missing tag metadata.
- «14linear-opr-proposition-auto-fa8dc9caaf»(Proposition)
  
  Missing tag metadata.
- «14linear-opr-theorem-auto-1ee719cdc3»(Theorem)
  
  Missing tag metadata.
- «14linear-opr-theorem-auto-a02e256b7f»(Theorem)
  
  Missing tag metadata.
- «cor:L1-convergence-in-measure»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_integrable_abs
- «cor:affine-change-of-variables»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
  - NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
- «cor:beppo-levi-l1»(Corollary)
  
  Missing tag metadata.
- «cor:dominated-convergence-l1»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence
- «cor:inner-measure-via-compact-set»(Corollary)
  
  Missing tag metadata.
- «cor:iterated-integral-exchange»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter11.integral_integral_swap
- «cor:l1-absolutely-summable-series-termwise-integration»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter10.integral_tsum_eq_tsum_integral_of_summable_integral_norm
  - NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm
- «cor:volume-under-affine-map»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
- «def:finite-additive-family»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - NoteKsk.FiniteAdditiveFamily
  - MeasureTheory.IsSetRing
- «def:jordan-one-dimensional-interval»(Definition)
  
  Missing tag metadata.
- «def:lebesgue-measurable-local»(Definition)
  
  Missing tag metadata.
  Associated lean decls (6)
- «def:ring-of-sets»(Definition)
  
  Missing tag metadata.
- «lem:finite-outer-compact-criterion»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter05.finiteOuter_compact_approx_criterion
  - NoteKsk.Chapter05.finiteOuter_open_approx_criterion
- «prop:L1-space-structure»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (7)
- «prop:integral-representation-independence»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_eq_sub_of_ae_eq_sub
- «prop:lebesgue-global-local»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurableSet_windows
- «thm:banach-tarski»(Theorem)
  
  Missing tag metadata.
- «thm:dominated-series-termwise-integration»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - NoteKsk.Chapter10.hasSum_integral_of_dominated_convergence
  - NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm
- «thm:finite-outer-measurable-iff-inner-outer»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- «thm:inner-measure-via-open-set»(Theorem)
  
  Missing tag metadata.
- «thm:polar-coordinates-rn»(Theorem)
  
  Missing tag metadata.
- «thm:solovay-model»(Theorem)
  
  Missing tag metadata.
- «thm:vitali-nonmeasurable»(Theorem)
  
  Missing tag metadata.

Structure and coverage

Informal-only111Statements with no associated Lean code yet.

Ready to formalize8Entries whose next step is currently unblocked.

Formalized, ancestors open5Local Lean work is done, but prerequisite closure is still open.

Fully closed168Local code and ancestor closure are both complete.

Blocked or incomplete15Entries not covered by the highlighted readiness buckets above.

Heaviest prerequisites (188)

«thm:lebesgue-integral-basic-formulas»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 9statement deps: 9proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (9)
«prop:L1-space-structure»(Proposition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (7)
«thm:jordan-measurable-criterion»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 3
Associated lean decls (2)
- NoteKsk.Chapter02.jordanMeasurable_iff_boundary_null
- NoteKsk.Chapter02.jordanMeasurable_iff_indicator_riemannIntegrable
«cor:ae-limit-measurable»(Corollary)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
- NoteKsk.Chapter07.measurable_of_ae_tendsto_real
- NoteKsk.Chapter07.measurable_of_ae_tendsto_ereal
«ex:lebesgue-measure-from-caratheodory-hahn»(Proposition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- NoteKsk.Chapter06.lambdaStar_eq_inducedOuterMeasureFromBoxes
«lem:lebesgue-measurable-caratheodory-finite»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- NoteKsk.Chapter05.lebesgueMeasurable_caratheodory_finite
«prop:lebesgue-measure-translation-invariant»(Proposition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (2)
- NoteKsk.Chapter05.lebesgueMeasurableSet_translate
- NoteKsk.Chapter05.lebesgueMeasure_translate
«thm:borel-sets-are-lebesgue-measurable»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- NoteKsk.Chapter06.borelSet_lebesgueMeasurable
«thm:caratheodory-hahn-extension»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (5)
«thm:dominated-convergence»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 5downstream unlocks: 7
Associated lean decls (2)
- NoteKsk.Chapter10.integrable_limit_of_dominated_convergence
- NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence
Show all 178 more heaviest-prerequisite entries
- «thm:inner-measure-via-interval»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 28
  Associated lean decls (1)
  - NoteKsk.Chapter04.lambdaInner_eq_boxVolume_sub_lambdaStar_diff
- «thm:jordan-measurable-lebesgue»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter05.jordanMeasurable_lebesgueMeasurable
  - NoteKsk.Chapter05.lebesgueMeasure_eq_jordanMeasure
- «thm:jordan-measure-properties»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (3)
- «thm:lebesgue-measure-completion-of-borel»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (3)
- «thm:lebesgue-measure-countable-additivity»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_tsum
- «thm:outer-measure-from-premeasure»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (4)
- «thm:premeasure-extension-to-algebra»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (3)
- «cor:beppo-levi-l1»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
- «cor:countable-lebesgue-null»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter05.countable_lebesgueMeasurable
  - NoteKsk.Chapter05.countable_lebesgueMeasure_eq_zero
- «cor:iterated-integral-exchange»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter11.integral_integral_swap
- «cor:l1-absolutely-summable-series-termwise-integration»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter10.integral_tsum_eq_tsum_integral_of_summable_integral_norm
  - NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm
- «cor:lebesgue-caratheodory-equivalence»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurable_iff_caratheodory
- «cor:local-measurable-set-operations»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 20
  Associated lean decls (2)
  - NoteKsk.Chapter05.localLebesgueMeasurable_inter
  - NoteKsk.Chapter05.localLebesgueMeasurable_diff
- «cor:measurable-algebra-operations»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (7)
- «cor:nonnegative-series-termwise-integration»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter10.lintegral_tsum
- «def:algebra-generated-by-semiring»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - NoteKsk.algebraGeneratedBySemiring
- «def:borel-measure»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter06.borelMeasure
- «def:lebesgue-integrable-function»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 29
  Associated lean decls (4)
- «def:lebesgue-measurable-function»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 57
  Associated lean decls (3)
- «def:lebesgue-measurable-local»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 29
  Associated lean decls (6)
- «def:outer-measure-generated-by-premeasure»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter06.inducedOuterMeasureFromPremeasure
- «def:premeasure-on-algebra»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (2)
  - MeasureTheory.AddContent
  - NoteKsk.IsPremeasureOnSemiring
- «ex:boundary-elementary-jordan-null»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_boundary_elementary
- «ex:counting-measure»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter06.countingMeasure_apply
- «ex:discrete-premeasures»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
- «ex:elementary-set-jordan-measurable»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter02.elementarySet_jordanMeasurable
  - NoteKsk.Chapter02.jordanMeasure_elementarySet
- «ex:riemann-integral-identity»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter01.riemannIntegrable_id
  - NoteKsk.Chapter01.riemannIntegral_id
- «lem:compact-splits-outer-measure»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 29
  Associated lean decls (1)
  - NoteKsk.Chapter03.compact_splits_lambdaStar
- «lem:finite-open-compact-split»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 30
  Associated lean decls (1)
  - NoteKsk.Chapter03.finiteOpen_compact_split
- «lem:finite-outer-compact-criterion»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 22
  Associated lean decls (2)
  - NoteKsk.Chapter05.finiteOuter_compact_approx_criterion
  - NoteKsk.Chapter05.finiteOuter_open_approx_criterion
- «lem:lebesgue-measure-finite-additivity»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_union_add
- «lem:local-measurable-finite-union-additivity»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 21
  Associated lean decls (2)
  - NoteKsk.Chapter05.localLebesgueMeasurable_union
  - NoteKsk.Chapter05.localLebesgueMeasurable_union_additive
- «prop:ae-modification-measurable»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter07.measurable_of_ae_eq_complete
- «prop:integrable-as-difference»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (5)
- «prop:integral-additivity»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (4)
- «prop:integral-disjoint-additivity»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter09.setIntegral_union_of_disjoint
  - NoteKsk.Chapter09.setIntegral_union_of_disjoint_of_integrable
- «prop:integral-monotonicity»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 11
  Associated lean decls (2)
  - NoteKsk.Chapter09.integral_mono_ae_real
  - NoteKsk.Chapter09.integral_mono_real
- «prop:integral-representation-independence»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_eq_sub_of_ae_eq_sub
- «prop:integral-zero-iff-ae-zero»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_abs_eq_zero_iff_ae_eq_zero
- «prop:inverse-image-sigma-algebra»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (2)
  - NoteKsk.Chapter07.inducedMeasurableSpace
  - NoteKsk.Chapter07.inducedMeasurableSpace_measurable
- «prop:jordan-null-set-measurable»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_jordanMeasurable
- «prop:measurable-reciprocal»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (3)
- «prop:nonnegative-integral-ae-invariance»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (1)
  - NoteKsk.Chapter08.lintegralNN_congr_ae
- «prop:nonnegative-integral-basic»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 26
  Associated lean decls (3)
- «prop:nonnegative-integral-disjoint-additivity»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 7
  Associated lean decls (1)
  - NoteKsk.Chapter08.setLintegralNN_disjoint_union
- «prop:signed-integral-ae-invariance»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 17
  Associated lean decls (2)
  - NoteKsk.Chapter08.signed_integral_congr_ae
  - NoteKsk.Chapter08.integral_respects_ae_representatives
- «thm:algebra-generated-by-semiring»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter06.algebraGeneratedBySemiring_isSetRing
  - NoteKsk.Chapter06.algebraGeneratedBySemiring_measurable
- «thm:caratheodory-implies-lebesgue-measurable»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter05.caratheodory_implies_lebesgueMeasurable
- «thm:cavalieri-product-measure»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (4)
- «thm:dominated-series-termwise-integration»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter10.hasSum_integral_of_dominated_convergence
  - NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm
- «thm:finite-outer-measurable-iff-inner-outer»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 24
  Associated lean decls (3)
- «thm:integral-absolute-continuity»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (4)
- «thm:jordan-elementary-volume-properties»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (5)
- «thm:jordan-inner-lebesgue-inner»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter04.jordanInnerMeasure_le_lambdaInner
- «thm:jordan-measurable-set-operations»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- «thm:lebesgue-measurable-function-criterion»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 5
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_ereal_criterion_all_thresholds
  - NoteKsk.Chapter07.measurable_ereal_real_level_criterion
- «thm:lebesgue-measurable-sigma-algebra»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 15
  Associated lean decls (4)
- «thm:lebesgue-measure-basic»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter05.lebesgueMeasure_mono
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_le_tsum
- «thm:lebesgue-measure-continuity-from-above»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iInter_eq_iInf_of_antitone
- «thm:lebesgue-measure-continuity-from-below»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_iSup_of_mono
- «thm:lebesgue-measure-inner-regularity»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_innerRegular
- «thm:lebesgue-measure-outer-regularity»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_outerRegular
- «thm:lebesgue-null-measurable»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- «thm:local-measurable-sigma-algebra»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 19
  Associated lean decls (2)
  - NoteKsk.Chapter05.localLebesgueMeasurable_iUnion
  - NoteKsk.Chapter05.localLebesgueMeasurable_iUnion_additive
- «thm:measurable-continuous-composition»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_continuous_comp
  - NoteKsk.Chapter07.measurable_continuous_real_comp
- «thm:nonnegative-integral-simple-approximation»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 27
  Associated lean decls (3)
- «thm:open-closed-lebesgue-measurable»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 9
  Associated lean decls (2)
  - NoteKsk.Chapter05.isClosed_lebesgueMeasurable
  - NoteKsk.Chapter05.isOpen_lebesgueMeasurable
- «thm:riemann-darboux-equivalence»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter01.riemann_integrable_iff_darboux_integrable
  - NoteKsk.Chapter01.riemannIntegral_eq_darbouxIntegral
- «thm:riemann-ftc»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter01.fundamental_theorem_of_calculus_for_riemann
- «thm:riemann-implies-lebesgue-integrable»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter08.boxRiemann_integrableOn_and_integral_eq_of_bounded_aeContinuous
- «thm:vitali-nonmeasurable»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
- «10limits-example-auto-7455ac8402»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter10.hasDerivAt_laplace_transform_of_dominated_loc_of_lip
- «cor:L1-convergence-in-measure»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_integrable_abs
- «cor:affine-change-of-variables»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
  - NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
- «cor:bounded-convergence»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter10.tendsto_integral_of_bounded_convergence
- «cor:dominated-convergence-l1»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence
- «cor:dominated-integrability»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 13
  Associated lean decls (1)
  - NoteKsk.Chapter08.dominated_integrability
- «cor:integrable-finite-ae»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter08.integrable_real_finite_ae
- «cor:integral-finite-sum»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_finset_sum
- «cor:interval-outer-measure-split»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 27
  Associated lean decls (1)
  - NoteKsk.Chapter04.lambdaInner_eq_lambdaStar_iff_boxVolume_eq
- «cor:lebesgue-measurable-set-operations»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (4)
- «cor:riemann-integral-indicator-jordan-measure»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter02.riemannIntegral_indicator_eq_jordanMeasure
- «cor:volume-under-affine-map»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
- «def:L1-space»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.L1Space
- «def:ae-convergence»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.AEConvergesOn
- «def:borel-sigma-algebra»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter06.borelSigmaAlgebra
- «def:caratheodory-condition»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (3)
- «def:completion»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- «def:darboux-integrable»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.Chapter01.DarbouxIntegrableOn
  - NoteKsk.Chapter01.darbouxIntegral
- «def:darboux-sums»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (4)
- «def:darboux-upper-lower-integral»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (4)
- «def:generated-sigma-algebra»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (3)
- «def:integral-over-subset»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 27
  Associated lean decls (2)
  - NoteKsk.setLintegralNN
  - NoteKsk.Chapter08.setLintegralNN_eq_indicator
- «def:jordan-box»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 17
  Associated lean decls (9)
- «def:jordan-elementary-set»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 16
  Associated lean decls (2)
  - NoteKsk.IsElementarySet
  - NoteKsk.elementaryVolume
- «def:jordan-measurable»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 6
  Associated lean decls (4)
- «def:jordan-null-set»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 8
  Associated lean decls (2)
  - NoteKsk.JordanNullSet
  - NoteKsk.Chapter02.jordanMeasure_eq_zero_of_null
- «def:jordan-outer-inner-measure»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 13
  Associated lean decls (2)
  - NoteKsk.jordanOuterMeasure
  - NoteKsk.jordanInnerMeasure
- «def:lebesgue-caratheodory-measurable»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - NoteKsk.Chapter05.LebesgueCaratheodoryMeasurable
- «def:lebesgue-inner-measure»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 37
  Associated lean decls (1)
  - NoteKsk.Chapter04.lambdaInner
- «def:measurable-function-space-notation»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 56
  Associated lean decls (3)
- «def:measurable-map»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 68
  Associated lean decls (2)
  - NoteKsk.MeasurableMap
  - NoteKsk.Chapter07.measurableMap_iff_preimage
- «def:measure»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 13
  Associated lean decls (3)
- «def:nonnegative-lebesgue-integral»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 46
  Associated lean decls (2)
  - NoteKsk.lintegralNN
  - NoteKsk.Chapter08.lintegralNN_def
- «def:nonnegative-simple-function»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 50
  Associated lean decls (2)
  - NoteKsk.SimpleNNFun
  - NoteKsk.Chapter08.simpleNNFun_measurable
- «def:outer-measure»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (4)
- «def:positive-negative-parts»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 31
  Associated lean decls (4)
- «def:premeasure-on-semiring»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 7
  Associated lean decls (2)
  - MeasureTheory.AddContent
  - NoteKsk.IsPremeasureOnSemiring
- «def:riemann-integrable»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 9downstream unlocks: 10
  Associated lean decls (3)
- «def:riemann-sum»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (2)
  - NoteKsk.Chapter01.IntervalPartition.IsTagged
  - NoteKsk.Chapter01.riemannSum
- «def:sigma-finite-measure»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- «def:simple-function-integral»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 29
  Associated lean decls (2)
  - NoteKsk.simpleLintegral
  - NoteKsk.Chapter08.lintegralNN_eq_simple
- «ex:continuous-function-measurable»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter07.continuous_borelMeasurable
- «ex:continuous-riemann-integrable»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter01.riemannIntegrable_of_continuousOn
- «ex:dirac-measure»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter06.diracMeasure_apply
- «ex:dirichlet-not-riemann-integrable»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter01.dirichlet
  - NoteKsk.Chapter01.not_riemannIntegrable_dirichlet
- «ex:discrete-semirings»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter06.powerset_isSetSemiring
- «ex:finite-set-jordan-null»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_finite
- «ex:indicator-function-measurable»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter07.indicator_measurable
- «ex:left-half-open-semiring»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter06.leftHalfOpenBox_isSetSemiring
- «ex:parallelogram-area»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
- «ex:piecewise-constant-riemann-integrable»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter01.PiecewiseConstantOnInterval
  - NoteKsk.Chapter01.riemannIntegrable_piecewiseConstant
- «ex:piecewise-continuous-riemann-integrable»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter01.PiecewiseContinuousOnInterval
  - NoteKsk.Chapter01.riemannIntegrable_piecewiseContinuous
- «ex:polar-coordinates»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
- «ex:product-function-tonelli»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter11.lintegral_prod_mul
- «ex:riemann-integral-constant»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter01.riemannIntegrable_const
  - NoteKsk.Chapter01.riemannIntegral_const
- «ex:singleton-jordan-null»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_singleton
- «ex:unbounded-not-riemann-integrable»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter01.not_riemannIntegrable_of_unboundedOn
- «lem:commute-induce-generate-sigma-algebra»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (2)
  - NoteKsk.Chapter07.comap_generatedSigmaAlgebra
  - NoteKsk.Chapter07.measurable_to_generatedSigmaAlgebra
- «lem:finite-open-inner-compact»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 31
  Associated lean decls (1)
  - NoteKsk.Chapter03.finiteOpen_innerCompact_exists
- «lem:jordan-grid-subdivision»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter02.elementarySet_finite_union_leftHalfOpenBoxes
  - NoteKsk.Chapter02.elementaryVolume_eq_sum_boxVolume
- «lem:jordan-outer-finite-subadditive»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanOuterMeasure_finite_subadditive
- «lem:lebesgue-measure-limit»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 10
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_eq_iSup_of_mono
- «lem:local-measurable-complement»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 22
  Associated lean decls (3)
- «lem:positive-distance-additive»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 31
  Associated lean decls (2)
  - NoteKsk.Chapter03.PositiveDistanceApart
  - NoteKsk.Chapter03.lambdaStar_union_of_positiveDistanceApart
- «lem:simple-function-approximation»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 28
  Associated lean decls (4)
- «prop:ae-equality-equivalence»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.AEEqualOn
  - NoteKsk.Chapter07.aeEqualOn_equivalence
- «prop:chebyshev-inequality»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_integrable_abs
- «prop:compact-inner-outer-equal»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 12
  Associated lean decls (2)
  - NoteKsk.Chapter04.lambdaInner_eq_lambdaStar_of_isCompact
  - NoteKsk.Chapter04.lambdaInner_eq_zero_of_lambdaStar_eq_zero
- «prop:integral-absolute-value-bound»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (2)
  - NoteKsk.Chapter09.abs_integral_le_integral_abs
  - NoteKsk.Chapter09.norm_integral_le_integral_norm
- «prop:integral-ae-invariance»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 15
  Associated lean decls (3)
- «prop:integral-bound-by-constants»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_bounds_of_ae_const_le
- «prop:integral-homogeneity»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.Chapter09.integral_const_mul_real
  - NoteKsk.Chapter09.integral_smul
- «prop:integral-zero-on-null-set»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter09.integral_eq_zero_of_measure_univ_zero
  - NoteKsk.Chapter09.setIntegral_eq_zero_of_measure_zero
- «prop:interval-outer-measure-volume»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 29
  Associated lean decls (6)
- «prop:jordan-inner-le-outer»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanInnerMeasure_le_jordanOuterMeasure
- «prop:lebesgue-global-local»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 16
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurableSet_windows
- «prop:lebesgue-inner-basic»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 13
  Associated lean decls (3)
- «prop:lebesgue-measure-nonnegative»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter05.lebesgueMeasure_empty
  - NoteKsk.Chapter05.lebesgueMeasure_nonneg
- «prop:lebesgue-outer-translation-invariant»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter03.lambdaStar_translate
- «prop:louter-le-jouter»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter03.lambdaStar_le_jordanOuterMeasure
- «prop:measurable-comparison-sets»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (3)
- «prop:measurable-countable-sup-inf»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_pointwiseSup
  - NoteKsk.Chapter07.measurable_pointwiseInf
- «prop:measurable-limsup-liminf»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (4)
- «prop:measurable-vector-map»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter07.measurable_vector_map
- «prop:nonnegative-chebyshev-inequality»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_lintegral
- «prop:nonnegative-integral-zero-iff-ae-zero»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (1)
  - NoteKsk.Chapter08.lintegralNN_eq_zero_iff_ae_eq_zero
- «prop:null-set-integral-nonnegative»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 23
  Associated lean decls (1)
  - NoteKsk.Chapter08.setLintegralNN_eq_zero_of_measure_zero
- «prop:null-set-integral-signed»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 19
  Associated lean decls (2)
  - NoteKsk.Chapter08.integrableOn_of_measure_zero
  - NoteKsk.Chapter08.setIntegral_eq_zero_of_measure_zero
- «prop:positive-negative-basic-identities»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (7)
- «prop:simple-function-integral-basic»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 27
  Associated lean decls (5)
- «prop:simple-function-integral-well-defined»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - NoteKsk.Chapter08.simpleLintegral_congr
- «thm:caratheodory-theorem»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (8)
- «thm:continuity-under-integral-sign»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - NoteKsk.Chapter10.continuous_integral_of_dominated
  - NoteKsk.Chapter10.continuousAt_integral_of_dominated
- «thm:countable-outer-measure-zero»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (2)
  - NoteKsk.Chapter03.lambdaStar_singleton
  - NoteKsk.Chapter03.lambdaStar_countable_eq_zero
- «thm:differentiation-under-integral-sign»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - NoteKsk.Chapter10.hasFDerivAt_integral_under_dominated_loc_of_lip
  - NoteKsk.Chapter10.hasDerivAt_integral_under_dominated_loc_of_lip
- «thm:fatou-lemma»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (2)
  - NoteKsk.Chapter10.fatou_lintegral
  - NoteKsk.Chapter10.fatou_lintegral_atTop
- «thm:fubini»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (5)
- «thm:integrable-iff-absolute»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 24
  Associated lean decls (2)
  - NoteKsk.Chapter08.integrable_norm
  - NoteKsk.Chapter08.lebesgueIntegrable_iff_abs
- «thm:lebesgue-measurable-implies-caratheodory»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasurable_implies_caratheodory
- «thm:lebesgue-outer-measure»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 34
  Associated lean decls (5)
- «thm:lebesgue-outer-regularity-open»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 32
  Associated lean decls (2)
  - NoteKsk.Chapter03.lambdaStarByOpenSupersets
  - NoteKsk.Chapter03.lambdaStar_outerRegular_open
- «thm:measurable-map-composition»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - NoteKsk.Chapter07.measurable_comp
- «thm:monotone-convergence»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 11
  Associated lean decls (3)
- «thm:polar-coordinates-rn»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
- «thm:riemann-sums-tendsto-integral»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - NoteKsk.Chapter01.riemann_sums_tendsto_integral
- «thm:sections-measurable-general»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (4)
- «thm:tonelli»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (3)

No prerequisites (119)

«06caratheodory02-definition-auto-2113b228f0»(Definition)
«07mble-funcs-example-auto-2838d2b582»(Proposition)
«13hilbert-proposition-auto-dd72d110eb»(Proposition)
«12banach-theorem-auto-426c0c8fac»(Theorem)
«12banach-theorem-auto-e5bd950a27»(Theorem)
«13hilbert-example-auto-05b528424a»(Proposition)
«12banach-definition-auto-5dcf314007»(Definition)
«13hilbert-theorem-auto-8638e2a37f»(Theorem)
«06caratheodory02-example-auto-70bceb8d84»(Proposition)
«13hilbert-theorem-auto-921927e104»(Theorem)
Show all 109 more entries without prerequisites
- «13hilbert-definition-auto-32a874c6ce»(Definition)
- «03lebesgue-outer-theorem-auto-bcfe17076e»(Theorem)
- «13hilbert-proposition-auto-d8707bd73b»(Proposition)
- «02jordan02-definition-auto-09fd3f3928»(Definition)
- «14linear-opr-definition-auto-5c90b2f36a»(Definition)
- «01riemann-example-auto-7828e2d268»(Proposition)
- «02jordan02-example-auto-7771caf6bf»(Proposition)
- «ex:change-order-triangle»(Proposition)
- «12banach-proposition-auto-abba30c310»(Proposition)
- «thm:banach-tarski»(Theorem)
- «04lebesgue-inner-corollary-auto-37d04eb610»(Corollary)
- «02jordan02-example-auto-47516d5758»(Proposition)
- «12banach-lemma-auto-b357918422»(Lemma)
- «12banach-definition-auto-84ba8f01ee»(Definition)
- «def:semiring»(Definition)
  Associated lean decls (1)
  - MeasureTheory.IsSetSemiring
- «08lintegral-example-auto-08d592162e»(Proposition)
- «14linear-opr-definition-auto-47597d0b80»(Definition)
- «12banach-definition-auto-c460ce1e9c»(Definition)
- «13hilbert-corollary-auto-28874ae3ee»(Corollary)
- «13hilbert-definition-auto-259d3f6153»(Definition)
- «02jordan02-example-auto-fa3e18599e»(Proposition)
- «02jordan02-definition-auto-5793cf4a96»(Definition)
- «13hilbert-definition-auto-2a28e9ed50»(Definition)
- «14linear-opr-definition-auto-0b94de9aeb»(Definition)
- «13hilbert-definition-auto-1f8d0f9182»(Definition)
- «14linear-opr-example-auto-cf9db84d71»(Proposition)
- «13hilbert-definition-auto-49c9982d69»(Definition)
- «09lintegral-prop-example-auto-d3ad988065»(Proposition)
- «12banach-lemma-auto-73df993c86»(Lemma)
- «08lintegral-example-auto-985634d68c»(Proposition)
- «def:lebesgue-outer-measure»(Definition)
  Associated lean decls (9)
- «def:riemann-interval-partition»(Definition)
  Associated lean decls (5)
- «13hilbert-definition-auto-ab9f9cd0e4»(Definition)
- «def:sections»(Definition)
  Associated lean decls (4)
- «12banach-example-auto-df4f8139d9»(Proposition)
- «14linear-opr-theorem-auto-1ee719cdc3»(Theorem)
- «14linear-opr-proposition-auto-6b36a220ec»(Proposition)
- «13hilbert-example-auto-fed54eefed»(Proposition)
- «def:countably-additive-measure»(Definition)
  Associated lean decls (1)
  - MeasureTheory.Measure
- «13hilbert-theorem-auto-c0d78cf6a1»(Theorem)
- «06caratheodory02-definition-auto-86b8c96217»(Definition)
- «13hilbert-example-auto-137bd3a060»(Proposition)
- «12banach-theorem-auto-fde4450b71»(Theorem)
- «prop:inverse-image-basic»(Proposition)
  Associated lean decls (3)
- «01riemann-theorem-auto-5b3744507b»(Theorem)
- «02jordan02-example-auto-09f40721a5»(Proposition)
- «01riemann-example-auto-4910acf622»(Proposition)
- «def:ae-prop»(Definition)
  Associated lean decls (1)
  - NoteKsk.AlmostEverywhereOn
- «def:sigma-algebra»(Definition)
  Associated lean decls (6)
- «13hilbert-theorem-auto-ea6e5c2177»(Theorem)
- «12banach-definition-auto-5f93b3dba8»(Definition)
- «08lintegral-example-auto-ae9b38d1f9»(Proposition)
- «def:ring-of-sets»(Definition)
- «13hilbert-definition-auto-aed2a40a16»(Definition)
- «02jordan02-example-auto-3a4895ebda»(Proposition)
- «def:pointwise-limits»(Definition)
  Associated lean decls (4)
- «14linear-opr-definition-auto-6db1d33ddc»(Definition)
- «13hilbert-corollary-auto-720f5d0c1a»(Corollary)
- «03lebesgue-outer-theorem-auto-2e7c2024ee»(Theorem)
- «12banach-definition-auto-5b8f6e3fc7»(Definition)
- «13hilbert-proposition-auto-c72a2bf678»(Proposition)
- «03lebesgue-outer-example-auto-ee91c30bff»(Proposition)
- «14linear-opr-theorem-auto-a02e256b7f»(Theorem)
- «def:finite-additive-family»(Definition)
  Associated lean decls (2)
  - NoteKsk.FiniteAdditiveFamily
  - MeasureTheory.IsSetRing
- «01riemann-example-auto-4bf36b1bd4»(Proposition)
- «12banach-proposition-auto-5ac0dfc586»(Proposition)
- «thm:inner-measure-via-open-set»(Theorem)
- «03lebesgue-outer-definition-auto-8d32644e77»(Definition)
- «03lebesgue-outer-definition-auto-aaf4aa3003»(Definition)
  Associated lean decls (2)
  - NoteKsk.Chapter03.IsOuterMeasureFunction
  - MeasureTheory.OuterMeasure
- «01riemann-theorem-auto-b4a925f916»(Theorem)
- «03lebesgue-outer-example-auto-56b6bf606f»(Proposition)
- «10limits-example-auto-ef82d9de32»(Proposition)
- «14linear-opr-proposition-auto-fa8dc9caaf»(Proposition)
- «13hilbert-example-auto-450f5a5852»(Proposition)
- «10limits-example-auto-7371ef5f8f»(Proposition)
- «ex:finite-partition-semiring»(Proposition)
- «12banach-proposition-auto-a113ca5409»(Proposition)
- «ex:triangle-area-tonelli»(Proposition)
- «thm:change-of-variables-diffeomorphism»(Theorem)
  Associated lean decls (2)
  - NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul
  - NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul
- «thm:solovay-model»(Theorem)
- «14linear-opr-definition-auto-fd375cb2c0»(Definition)
- «08lintegral-example-auto-aab23f2012»(Proposition)
- «02jordan02-example-auto-9ce4c86a8e»(Proposition)
- «14linear-opr-example-auto-f81b4cda27»(Proposition)
- «13hilbert-proposition-auto-3d898884b4»(Proposition)
- «cor:inner-measure-via-compact-set»(Corollary)
- «14linear-opr-proposition-auto-100e285ffb»(Proposition)
- «05lebesgue03-example-auto-3b737bca05»(Proposition)
- «03lebesgue-outer-proposition-auto-07f01b1f71»(Proposition)
- «lem:borel-eRR»(Lemma)
  Associated lean decls (1)
  - NoteKsk.Chapter07.borel_eReal_eq_generate_Iic_real
- «02jordan02-proposition-auto-2ff693ea48»(Proposition)
- «def:measurable-space»(Definition)
  Associated lean decls (2)
  - MeasurableSpace
  - NoteKsk.SigmaAlgebra
- «05lebesgue03-definition-auto-ab11a0a94e»(Definition)
- «02jordan02-definition-auto-11f0199ce8»(Definition)
- «13hilbert-definition-auto-5d4ee5bb89»(Definition)
- «04lebesgue-inner-example-auto-0225bc1c45»(Proposition)
- «14linear-opr-example-auto-0f685b2c35»(Proposition)
- «12banach-example-auto-ccfbaa66df»(Proposition)
- «12banach-example-auto-e2034d98b1»(Proposition)
- «12banach-definition-auto-de1b622eef»(Definition)
- «03lebesgue-outer-proposition-auto-e312ac0c17»(Proposition)
- «12banach-theorem-auto-a903d22d15»(Theorem)
- «14linear-opr-corollary-auto-3cbe01ecb7»(Corollary)
- «12banach-definition-auto-7bd2c77569»(Definition)
- «02jordan02-theorem-auto-cfc2847f0d»(Theorem)
- «def:jordan-one-dimensional-interval»(Definition)
- «12banach-proposition-auto-92e612b4f2»(Proposition)
- «14linear-opr-definition-auto-fe652db767»(Definition)
- «12banach-definition-auto-4a6ca6d5ba»(Definition)

No dependents (157)

«06caratheodory02-definition-auto-2113b228f0»(Definition)
«ex:indicator-function-measurable»(Proposition)
Associated lean decls (1)
- NoteKsk.Chapter07.indicator_measurable
«thm:continuity-under-integral-sign»(Theorem)
Associated lean decls (2)
- NoteKsk.Chapter10.continuous_integral_of_dominated
- NoteKsk.Chapter10.continuousAt_integral_of_dominated
«07mble-funcs-example-auto-2838d2b582»(Proposition)
«13hilbert-proposition-auto-dd72d110eb»(Proposition)
«cor:iterated-integral-exchange»(Corollary)
Associated lean decls (1)
- NoteKsk.Chapter11.integral_integral_swap
«14linear-opr-definition-auto-fe652db767»(Definition)
«12banach-theorem-auto-e5bd950a27»(Theorem)
«02jordan02-theorem-auto-cfc2847f0d»(Theorem)
«12banach-definition-auto-7bd2c77569»(Definition)
Show all 147 more entries without dependents
- «14linear-opr-corollary-auto-3cbe01ecb7»(Corollary)
- «12banach-theorem-auto-a903d22d15»(Theorem)
- «03lebesgue-outer-proposition-auto-e312ac0c17»(Proposition)
- «12banach-definition-auto-de1b622eef»(Definition)
- «12banach-example-auto-e2034d98b1»(Proposition)
- «ex:unbounded-not-riemann-integrable»(Proposition)
  Associated lean decls (1)
  - NoteKsk.Chapter01.not_riemannIntegrable_of_unboundedOn
- «13hilbert-theorem-auto-921927e104»(Theorem)
- «13hilbert-definition-auto-32a874c6ce»(Definition)
- «03lebesgue-outer-theorem-auto-bcfe17076e»(Theorem)
- «13hilbert-proposition-auto-d8707bd73b»(Proposition)
- «02jordan02-definition-auto-09fd3f3928»(Definition)
- «ex:elementary-set-jordan-measurable»(Proposition)
  Associated lean decls (2)
  - NoteKsk.Chapter02.elementarySet_jordanMeasurable
  - NoteKsk.Chapter02.jordanMeasure_elementarySet
- «12banach-example-auto-ccfbaa66df»(Proposition)
- «14linear-opr-example-auto-0f685b2c35»(Proposition)
- «ex:change-order-triangle»(Proposition)
- «12banach-proposition-auto-abba30c310»(Proposition)
- «thm:banach-tarski»(Theorem)
- «04lebesgue-inner-corollary-auto-37d04eb610»(Corollary)
- «prop:simple-function-integral-well-defined»(Proposition)
  Associated lean decls (1)
  - NoteKsk.Chapter08.simpleLintegral_congr
- «ex:piecewise-constant-riemann-integrable»(Proposition)
  Associated lean decls (2)
  - NoteKsk.Chapter01.PiecewiseConstantOnInterval
  - NoteKsk.Chapter01.riemannIntegrable_piecewiseConstant
- «prop:measurable-reciprocal»(Proposition)
  Associated lean decls (3)
- «cor:beppo-levi-l1»(Corollary)
- «02jordan02-definition-auto-11f0199ce8»(Definition)
- «05lebesgue03-definition-auto-ab11a0a94e»(Definition)
- «prop:lebesgue-measure-nonnegative»(Proposition)
  Associated lean decls (2)
  - NoteKsk.Chapter05.lebesgueMeasure_empty
  - NoteKsk.Chapter05.lebesgueMeasure_nonneg
- «ex:piecewise-continuous-riemann-integrable»(Proposition)
  Associated lean decls (2)
  - NoteKsk.Chapter01.PiecewiseContinuousOnInterval
  - NoteKsk.Chapter01.riemannIntegrable_piecewiseContinuous
- «thm:lebesgue-measure-inner-regularity»(Theorem)
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_innerRegular
- «08lintegral-example-auto-08d592162e»(Proposition)
- «14linear-opr-proposition-auto-100e285ffb»(Proposition)
- «12banach-definition-auto-c460ce1e9c»(Definition)
- «cor:countable-lebesgue-null»(Corollary)
  Associated lean decls (2)
  - NoteKsk.Chapter05.countable_lebesgueMeasurable
  - NoteKsk.Chapter05.countable_lebesgueMeasure_eq_zero
- «cor:inner-measure-via-compact-set»(Corollary)
- «ex:riemann-integral-identity»(Proposition)
  Associated lean decls (2)
  - NoteKsk.Chapter01.riemannIntegrable_id
  - NoteKsk.Chapter01.riemannIntegral_id
- «13hilbert-definition-auto-259d3f6153»(Definition)
- «ex:riemann-integral-constant»(Proposition)
  Associated lean decls (2)
  - NoteKsk.Chapter01.riemannIntegrable_const
  - NoteKsk.Chapter01.riemannIntegral_const
- «13hilbert-definition-auto-2a28e9ed50»(Definition)
- «ex:finite-set-jordan-null»(Proposition)
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_finite
- «ex:lebesgue-measure-from-caratheodory-hahn»(Proposition)
  Associated lean decls (1)
  - NoteKsk.Chapter06.lambdaStar_eq_inducedOuterMeasureFromBoxes
- «14linear-opr-definition-auto-0b94de9aeb»(Definition)
- «prop:jordan-null-set-measurable»(Proposition)
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanNullSet_jordanMeasurable
- «13hilbert-proposition-auto-3d898884b4»(Proposition)
- «14linear-opr-example-auto-f81b4cda27»(Proposition)
- «02jordan02-example-auto-9ce4c86a8e»(Proposition)
- «08lintegral-example-auto-aab23f2012»(Proposition)
- «14linear-opr-definition-auto-fd375cb2c0»(Definition)
- «ex:parallelogram-area»(Proposition)
- «14linear-opr-proposition-auto-6b36a220ec»(Proposition)
- «13hilbert-example-auto-fed54eefed»(Proposition)
- «def:countably-additive-measure»(Definition)
  Associated lean decls (1)
  - MeasureTheory.Measure
- «13hilbert-theorem-auto-c0d78cf6a1»(Theorem)
- «ex:finite-partition-semiring»(Proposition)
- «10limits-example-auto-7371ef5f8f»(Proposition)
- «12banach-theorem-auto-fde4450b71»(Theorem)
- «10limits-example-auto-7455ac8402»(Proposition)
  Associated lean decls (1)
  - NoteKsk.Chapter10.hasDerivAt_laplace_transform_of_dominated_loc_of_lip
- «13hilbert-example-auto-450f5a5852»(Proposition)
- «ex:discrete-premeasures»(Proposition)
- «10limits-example-auto-ef82d9de32»(Proposition)
- «03lebesgue-outer-example-auto-56b6bf606f»(Proposition)
- «01riemann-theorem-auto-b4a925f916»(Theorem)
- «cor:dominated-convergence-l1»(Corollary)
  Associated lean decls (1)
  - NoteKsk.Chapter10.tendsto_integral_of_dominated_convergence
- «cor:ae-limit-measurable»(Corollary)
  Associated lean decls (2)
  - NoteKsk.Chapter07.measurable_of_ae_tendsto_real
  - NoteKsk.Chapter07.measurable_of_ae_tendsto_ereal
- «01riemann-example-auto-4910acf622»(Proposition)
- «ex:dirac-measure»(Proposition)
  Associated lean decls (1)
  - NoteKsk.Chapter06.diracMeasure_apply
- «thm:inner-measure-via-open-set»(Theorem)
- «thm:riemann-ftc»(Theorem)
  Associated lean decls (1)
  - NoteKsk.Chapter01.fundamental_theorem_of_calculus_for_riemann
- «thm:cavalieri-product-measure»(Theorem)
  Associated lean decls (4)
- «12banach-proposition-auto-5ac0dfc586»(Proposition)
- «thm:jordan-measurable-lebesgue»(Theorem)
  Associated lean decls (2)
  - NoteKsk.Chapter05.jordanMeasurable_lebesgueMeasurable
  - NoteKsk.Chapter05.lebesgueMeasure_eq_jordanMeasure
- «08lintegral-example-auto-ae9b38d1f9»(Proposition)
- «13hilbert-corollary-auto-720f5d0c1a»(Corollary)
- «thm:jordan-measure-properties»(Theorem)
  Associated lean decls (3)
- «14linear-opr-definition-auto-6db1d33ddc»(Definition)
- «prop:jordan-inner-le-outer»(Proposition)
  Associated lean decls (1)
  - NoteKsk.Chapter02.jordanInnerMeasure_le_jordanOuterMeasure
- «13hilbert-definition-auto-aed2a40a16»(Definition)
- «02jordan02-example-auto-3a4895ebda»(Proposition)
- «cor:integrable-finite-ae»(Corollary)
  Associated lean decls (1)
  - NoteKsk.Chapter08.integrable_real_finite_ae
- «cor:l1-absolutely-summable-series-termwise-integration»(Corollary)
  Associated lean decls (2)
  - NoteKsk.Chapter10.integral_tsum_eq_tsum_integral_of_summable_integral_norm
  - NoteKsk.Chapter10.integral_tsum_of_summable_integral_norm
- «03lebesgue-outer-theorem-auto-2e7c2024ee»(Theorem)
- «12banach-definition-auto-5b8f6e3fc7»(Definition)
- «13hilbert-proposition-auto-c72a2bf678»(Proposition)
- «03lebesgue-outer-example-auto-ee91c30bff»(Proposition)
- «14linear-opr-theorem-auto-a02e256b7f»(Theorem)
- «01riemann-example-auto-4bf36b1bd4»(Proposition)
- «thm:jordan-elementary-volume-properties»(Theorem)
  Associated lean decls (5)
- «12banach-definition-auto-5f93b3dba8»(Definition)
- «13hilbert-theorem-auto-ea6e5c2177»(Theorem)
- «cor:nonnegative-series-termwise-integration»(Corollary)
  Associated lean decls (1)
  - NoteKsk.Chapter10.lintegral_tsum
- «03lebesgue-outer-definition-auto-8d32644e77»(Definition)
- «03lebesgue-outer-definition-auto-aaf4aa3003»(Definition)
  Associated lean decls (2)
  - NoteKsk.Chapter03.IsOuterMeasureFunction
  - MeasureTheory.OuterMeasure
- «02jordan02-example-auto-09f40721a5»(Proposition)
- «ex:product-function-tonelli»(Proposition)
  Associated lean decls (1)
  - NoteKsk.Chapter11.lintegral_prod_mul
- «14linear-opr-proposition-auto-fa8dc9caaf»(Proposition)
- «01riemann-theorem-auto-5b3744507b»(Theorem)
- «prop:measurable-comparison-sets»(Proposition)
  Associated lean decls (3)
- «thm:lebesgue-measure-basic»(Theorem)
  Associated lean decls (2)
  - NoteKsk.Chapter05.lebesgueMeasure_mono
  - NoteKsk.Chapter05.lebesgueMeasure_iUnion_le_tsum
- «13hilbert-example-auto-137bd3a060»(Proposition)
- «06caratheodory02-definition-auto-86b8c96217»(Definition)
- «cor:bounded-convergence»(Corollary)
  Associated lean decls (1)
  - NoteKsk.Chapter10.tendsto_integral_of_bounded_convergence
- «12banach-proposition-auto-a113ca5409»(Proposition)
- «ex:triangle-area-tonelli»(Proposition)
- «prop:L1-space-structure»(Proposition)
  Associated lean decls (7)
- «thm:solovay-model»(Theorem)
- «14linear-opr-theorem-auto-1ee719cdc3»(Theorem)
- «12banach-example-auto-df4f8139d9»(Proposition)
- «thm:integral-absolute-continuity»(Theorem)
  Associated lean decls (4)
- «13hilbert-definition-auto-ab9f9cd0e4»(Definition)
- «08lintegral-example-auto-985634d68c»(Proposition)
- «12banach-lemma-auto-73df993c86»(Lemma)
- «09lintegral-prop-example-auto-d3ad988065»(Proposition)
- «13hilbert-definition-auto-49c9982d69»(Definition)
- «14linear-opr-example-auto-cf9db84d71»(Proposition)
- «13hilbert-definition-auto-1f8d0f9182»(Definition)
- «ex:polar-coordinates»(Proposition)
- «02jordan02-definition-auto-5793cf4a96»(Definition)
- «02jordan02-example-auto-fa3e18599e»(Proposition)
- «13hilbert-corollary-auto-28874ae3ee»(Corollary)
- «ex:counting-measure»(Proposition)
  Associated lean decls (1)
  - NoteKsk.Chapter06.countingMeasure_apply
- «14linear-opr-definition-auto-47597d0b80»(Definition)
- «thm:lebesgue-measure-continuity-from-above»(Theorem)
  Associated lean decls (1)
  - NoteKsk.Chapter05.lebesgueMeasure_iInter_eq_iInf_of_antitone
- «05lebesgue03-example-auto-3b737bca05»(Proposition)
- «03lebesgue-outer-proposition-auto-07f01b1f71»(Proposition)
- «12banach-definition-auto-84ba8f01ee»(Definition)
- «12banach-lemma-auto-b357918422»(Lemma)
- «02jordan02-example-auto-47516d5758»(Proposition)
- «cor:L1-convergence-in-measure»(Corollary)
  Associated lean decls (1)
  - NoteKsk.Chapter09.chebyshev_integrable_abs
- «02jordan02-proposition-auto-2ff693ea48»(Proposition)
- «prop:integral-bound-by-constants»(Proposition)
  Associated lean decls (1)
  - NoteKsk.Chapter09.integral_bounds_of_ae_const_le
- «ex:dirichlet-not-riemann-integrable»(Proposition)
  Associated lean decls (2)
  - NoteKsk.Chapter01.dirichlet
  - NoteKsk.Chapter01.not_riemannIntegrable_dirichlet
- «thm:borel-sets-are-lebesgue-measurable»(Theorem)
  Associated lean decls (1)
  - NoteKsk.Chapter06.borelSet_lebesgueMeasurable
- «13hilbert-definition-auto-5d4ee5bb89»(Definition)
- «04lebesgue-inner-example-auto-0225bc1c45»(Proposition)
- «thm:lebesgue-integral-basic-formulas»(Theorem)
  Associated lean decls (9)
- «02jordan02-example-auto-7771caf6bf»(Proposition)
- «thm:polar-coordinates-rn»(Theorem)
- «thm:algebra-generated-by-semiring»(Theorem)
  Associated lean decls (2)
  - NoteKsk.Chapter06.algebraGeneratedBySemiring_isSetRing
  - NoteKsk.Chapter06.algebraGeneratedBySemiring_measurable
- «01riemann-example-auto-7828e2d268»(Proposition)
- «14linear-opr-definition-auto-5c90b2f36a»(Definition)
- «06caratheodory02-example-auto-70bceb8d84»(Proposition)
- «13hilbert-theorem-auto-8638e2a37f»(Theorem)
- «12banach-definition-auto-5dcf314007»(Definition)
- «13hilbert-example-auto-05b528424a»(Proposition)
- «thm:vitali-nonmeasurable»(Theorem)
- «12banach-theorem-auto-426c0c8fac»(Theorem)
- «thm:riemann-implies-lebesgue-integrable»(Theorem)
  Associated lean decls (1)
  - NoteKsk.Chapter08.boxRiemann_integrableOn_and_integral_eq_of_bounded_aeContinuous
- «12banach-proposition-auto-92e612b4f2»(Proposition)
- «thm:lebesgue-measure-completion-of-borel»(Theorem)
  Associated lean decls (3)
- «12banach-definition-auto-4a6ca6d5ba»(Definition)