feat: add add Liu's uncertainty theory foundations (core/distribution/process modules)#35976
feat: add add Liu's uncertainty theory foundations (core/distribution/process modules)#35976Phelixh wants to merge 25 commits intoleanprover-community:masterfrom
Conversation
Phelixh
commented
Mar 2, 2026
Phelixh
commented
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary a237616fe5
|
| Files | Import difference |
|---|---|
Mathlib.Uncertainty.BaseCore (new file) |
2528 |
Mathlib.Uncertainty.BaseDistribution (new file) |
2529 |
Mathlib.Uncertainty.BaseProcess (new file) |
2530 |
Mathlib.Uncertainty.Base (new file) |
2531 |
Mathlib.Uncertainty.Uncertainty (new file) |
2532 |
Declarations diff
+ AlgebraicUncertainSpace
+ BookAxiomSet
+ ChanceSpace
+ ChanceVariable
+ CompleteLiuProcess
+ ConvergenceBridgeStrongAssumption
+ ConvergenceBridgeStructure
+ ConvergesAlmostSurelyTo
+ ConvergesInDistributionTo
+ ConvergesInMeanTo
+ ConvergesInMeasureTo
+ Cov
+ Cov_comm
+ Cov_self
+ CreatedLinearVariable
+ DistributionFormulaStructure
+ E
+ E_add
+ E_add_const
+ E_affine
+ E_centered
+ E_const
+ E_linearComb
+ E_mono
+ E_smul
+ E_sub
+ EulerSchemeStructure
+ EulerTerminalBridgeStructure
+ EulerTerminalConsistency
+ EulerTerminalConvergenceInMeasure
+ EulerTerminalStrongAssumption
+ ExpectationConstStructure
+ ExpectationIndependenceStructure
+ ExpectationOrderStructure
+ ExpectationStructure
+ IncrementLaw
+ ItoStructure
+ LimitTheoryStructure
+ LinearDistributionRegularityStructure
+ LinearParams
+ LiuProcess
+ MixedLLNStrongAssumption
+ MixedLLNStructure
+ NormalDistributionForm
+ NormalDistributionRegularityStructure
+ NormalParams
+ OperationalLawStructure
+ RegularDistributionLike
+ RenewalUpdateStrongAssumption
+ RenewalUpdateTheoryStructure
+ SecondMomentIdentityStructure
+ SecondMomentStructure
+ SpecialDistributionStatsStructure
+ UncertainDE
+ UncertainDEWellposednessStructure
+ UncertainDistributionLike
+ UncertainInequalityStructure
+ UncertainMeasureBoundsStructure
+ UncertainMeasureDefaultInstance
+ UncertainMeasureMonotoneStructure
+ UncertainNullEventStructure
+ UncertainProcess
+ UncertainProgrammingStructure
+ UncertainRandomVariable
+ UncertainRenewalProcess
+ UncertainSequence
+ UncertainSequenceIID
+ UncertainSpace
+ UncertainSpaceContinuity
+ UncertainVariable
+ Var
+ Var_nonneg
+ ZigzagDistributionRegularityStructure
+ ZigzagParams
+ absPow_uncertain
+ add_uncertain
+ add_uncertain_f
+ add_uncertain_of_meas
+ bookAxiom1_normality
+ bookAxiom1_normality_from_space
+ bookAxiom1_normality_holds
+ bookAxiom2_duality
+ bookAxiom2_duality_from_space
+ bookAxiom2_duality_holds
+ bookAxiom3_subadditivity
+ bookAxiom3_subadditivity_from_space
+ bookAxiom3_subadditivity_holds
+ bookAxiom4_product
+ centered_uncertain
+ centered_uncertain_f
+ central_limit_theorem_interface
+ completeLiu_increment_independent
+ completeLiu_increment_stationary_dist
+ completeLiu_increment_stationary_shift_dist
+ completeLiu_path_continuous
+ const_uncertain
+ const_uncertain_f
+ convergence_mean_to_measure
+ convergence_measure_to_distribution
+ createLinearVariable
+ createLinearVariable_cdf
+ createLinearVariable_has_linear_distribution
+ createLinearVariable_quantile
+ diff_with_null_event_eq
+ dual_theorem
+ e2e_centered_affine_zero
+ e2e_exampleLinear_pipeline
+ elementary_renewal_theorem_distribution
+ elementary_renewal_theorem_expectation
+ engineeringCutoff
+ eulerGridTime
+ eulerSchemeTraceVar
+ eulerStep
+ eulerStep_f
+ eulerTerminalErrorEvent
+ eulerTerminalErrorMeasure
+ eulerTerminalPathError
+ eulerTrace
+ eulerTracePath
+ eulerTraceVar
+ eulerTraceVar_f
+ eulerTraceVar_succ
+ eulerTraceVar_zero
+ eulerTrace_succ
+ eulerTrace_zero
+ euler_gridConsistency_of_terminalConvergence
+ euler_terminalConsistency_of_terminalConvergence
+ even_moment_formula_interface
+ exampleExpectation
+ exampleLinear
+ exampleLinearParams
+ expectedValue_add
+ expectedValue_linear
+ expectedValue_linearComb
+ expectedValue_linearComb_example
+ expectedValue_smul
+ expectedValue_via_inverse_interface
+ finite_subadditive
+ iid_pairwise_independent
+ iid_same_distribution
+ incrementLaw_apply
+ increment_uncertain
+ increment_uncertain_f
+ instance (priority := 100)
+ instance (priority := 100) convergenceBridge_of_strongAssumption
+ instance (priority := 100) instUncertainMeasureBounds_fromDefault
+ instance (priority := 100) instUncertainMeasureMonotone_fromDefault
+ instance (priority := 100) instUncertainNullEvent_fromDefault
+ instance (priority := 100) mixedLLN_of_strongAssumption
+ instance (priority := 100) renewalUpdate_of_strongAssumption
+ instance (priority := 90) mixedLLNStrong_of_structure
+ instance : SpecialDistributionStatsStructure
+ instance : UncertainDistributionLike LinearParams
+ instance : UncertainDistributionLike NormalParams
+ instance : UncertainDistributionLike ZigzagParams
+ instance [LinearDistributionRegularityStructure] : RegularDistributionLike LinearParams
+ instance [NormalDistributionRegularityStructure] :
+ instance [ZigzagDistributionRegularityStructure] : RegularDistributionLike ZigzagParams
+ integral_affine
+ intervalMassLE
+ ito_formula_interface
+ law_of_large_numbers_interface
+ law_of_large_numbers_mixed
+ linearComb_uncertain
+ linearComb_uncertain_f
+ linearDistribution
+ linearDistribution_continuous
+ linearDistribution_eq_intervalMassLE
+ linearDistribution_is_uncertain
+ linearDistribution_le_one
+ linearDistribution_mem_Icc
+ linearDistribution_nonneg
+ linearDistribution_of_gt
+ linearDistribution_of_lt
+ linearDistribution_of_mem_Icc
+ linearDistribution_strictMonoOn_core
+ linearDistribution_tendsto_atBot
+ linearDistribution_tendsto_atTop
+ linearExpectedValue
+ linearInverse
+ linearInverseTotal
+ linearInverse_eq_affine
+ linearInverse_one
+ linearInverse_zero
+ linearVarianceClosedForm
+ linearVarianceClosedForm_nonneg
+ linear_expectation_interface
+ linear_variance_nonneg_interface
+ liuAt
+ liuAt_f
+ liu_increment_independent
+ lognormalInverseBook
+ lognormalUncertainDistribution
+ measurable_iInter
+ measurable_linearComb
+ measure_bounds
+ measure_monotone
+ mkEulerSchemeFromTrace
+ mkMixedLLNStrongAssumption
+ mkRenewalUpdateStrongAssumption
+ normalBookToLegacyParams
+ normalDistributionUnified
+ normalDistributionUnified_book
+ normalDistributionUnified_book_as_legacy_scaled
+ normalDistributionUnified_legacy
+ normalDistributionUnified_legacy_as_book_scaled
+ normalInverseBook
+ normalInverseBook_median
+ normalLegacyToBookParams
+ normalUncertainDistribution
+ normalUncertainDistributionBook
+ normalUncertainDistributionBook_eq_normalUncertainDistribution_scaled
+ normalUncertainDistributionBook_le_one
+ normalUncertainDistributionBook_mem_Icc
+ normalUncertainDistributionBook_nonneg
+ normalUncertainDistribution_continuous
+ normalUncertainDistribution_eq_normalUncertainDistributionBook_scaled
+ normalUncertainDistribution_le_one
+ normalUncertainDistribution_mem_Icc
+ normalUncertainDistribution_nonneg
+ normalUncertainDistribution_strictMonoOn_core
+ normalUncertainDistribution_tendsto_atBot
+ normalUncertainDistribution_tendsto_atTop
+ normalVarianceClosedForm
+ normalVarianceClosedForm_pos
+ normal_inverse_median_interface
+ normal_variance_positive_interface
+ odd_moment_formula_interface
+ operational_inverse_transform_formula
+ processAt
+ processAt_f
+ renewalUpdateStrong_of_structure
+ renewal_reward_theorem_distribution
+ renewal_reward_theorem_expectation
+ sampleMean
+ secondMoment
+ smul_uncertain
+ smul_uncertain_f
+ smul_uncertain_of_meas
+ standardNormalUncertainDistribution
+ sub_uncertain
+ sub_uncertain_f
+ uncertainDE_existence_interface
+ uncertainDE_uniqueness_interface
+ uncertainDistribution
+ uncertainExpectedValue
+ uncertainProgramming_solver_correct
+ uncertain_chebyshev
+ uncertain_markov
+ uncertain_mean_LLN
+ uncertain_strong_LLN
+ uncertain_weak_LLN
+ union_with_null_event_eq
+ variance_eq_secondMoment_sub_sq
+ variance_via_inverse_interface
+ zigzagDistribution
+ zigzagDistribution_continuous
+ zigzagDistribution_le_one
+ zigzagDistribution_mem_Icc
+ zigzagDistribution_nonneg
+ zigzagDistribution_strictMonoOn_core
+ zigzagDistribution_tendsto_atBot
+ zigzagDistribution_tendsto_atTop
+ zigzagInverse
+ zigzag_left
+ zigzag_right
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
There was a problem hiding this comment.
Pull request overview
This PR introduces an initial Lean scaffold for formalizing Liu’s uncertainty theory in Mathlib, split into core definitions, distribution primitives, and process-level interfaces.
Changes:
- Add foundational structures for uncertain spaces/variables plus expectation/variance and convergence interface layers.
- Add a distribution layer with several example distribution families and “regularity/statistics/formula” interfaces.
- Add a process layer with uncertain processes, renewal/Euler scheme interface scaffolding, and Liu-process interfaces; add aggregator/root modules.
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 14 comments.
Show a summary per file
| File | Description |
|---|---|
| Mathlib/Uncertainty/base_core.lean | Core definitions: uncertain spaces/variables, axioms, expectation/variance, convergence and limit-theory interfaces. |
| Mathlib/Uncertainty/base_distribution.lean | Distribution families (linear/zigzag/normal/lognormal) plus regularity/statistics/formula interface classes. |
| Mathlib/Uncertainty/base_process.lean | Process-level interfaces: uncertain processes, renewal/Euler/Ito/wellposedness scaffolding, Liu-process definitions. |
| Mathlib/Uncertainty/base.lean | Aggregator importing core/distribution/process modules. |
| Mathlib/Uncertainty/uncertainty.lean | Intended “root” module for the uncertainty theory library. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| instance (priority := 90) mixedLLNStrong_of_structure | ||
| (U : UncertainSpace) (C : ChanceSpace) | ||
| [AlgebraicUncertainSpace U] [ExpectationStructure U] | ||
| [MixedLLNStructure U C] : | ||
| MixedLLNStrongAssumption U C where | ||
| mixed_lln_statement := MixedLLNStructure.mixed_lln_statement (U := U) (C := C) | ||
| mixed_lln_axiom := MixedLLNStructure.mixed_lln_axiom (U := U) (C := C) | ||
|
|
||
| instance (priority := 100) mixedLLN_of_strongAssumption | ||
| (U : UncertainSpace) (C : ChanceSpace) | ||
| [AlgebraicUncertainSpace U] [ExpectationStructure U] | ||
| [MixedLLNStrongAssumption U C] : | ||
| MixedLLNStructure U C where | ||
| mixed_lln_statement := | ||
| MixedLLNStrongAssumption.mixed_lln_statement (U := U) (C := C) | ||
| mixed_lln_axiom := | ||
| MixedLLNStrongAssumption.mixed_lln_axiom (U := U) (C := C) | ||
|
|
There was a problem hiding this comment.
These two instances create a typeclass cycle (MixedLLNStructure → MixedLLNStrongAssumption → MixedLLNStructure), which can cause nontermination/timeout in typeclass search. Usually only the “strong assumptions ⇒ structure” direction should be an instance, and the reverse should be an explicit constructor/lemma (or avoided entirely).
There was a problem hiding this comment.
@copilot open a new pull request to apply changes based on this feedback
There was a problem hiding this comment.
@copilot open a new pull request to apply changes based on this feedback
There was a problem hiding this comment.
@copilot open a new pull request to apply changes based on this feedback
| instance (priority := 90) renewalUpdateStrong_of_structure | ||
| (U : UncertainSpace) [AlgebraicUncertainSpace U] [ExpectationStructure U] | ||
| [RenewalUpdateTheoryStructure U] : | ||
| RenewalUpdateStrongAssumption U where | ||
| elementary_renewal_distribution_statement := | ||
| RenewalUpdateTheoryStructure.elementary_renewal_distribution_statement (U := U) | ||
| elementary_renewal_expectation_statement := | ||
| RenewalUpdateTheoryStructure.elementary_renewal_expectation_statement (U := U) | ||
| renewal_reward_distribution_statement := | ||
| RenewalUpdateTheoryStructure.renewal_reward_distribution_statement (U := U) | ||
| renewal_reward_expectation_statement := | ||
| RenewalUpdateTheoryStructure.renewal_reward_expectation_statement (U := U) | ||
| elementary_renewal_distribution_axiom := | ||
| RenewalUpdateTheoryStructure.elementary_renewal_distribution_axiom (U := U) | ||
| elementary_renewal_expectation_axiom := | ||
| RenewalUpdateTheoryStructure.elementary_renewal_expectation_axiom (U := U) | ||
| renewal_reward_distribution_axiom := | ||
| RenewalUpdateTheoryStructure.renewal_reward_distribution_axiom (U := U) | ||
| renewal_reward_expectation_axiom := | ||
| RenewalUpdateTheoryStructure.renewal_reward_expectation_axiom (U := U) | ||
|
|
||
| instance (priority := 100) renewalUpdate_of_strongAssumption | ||
| (U : UncertainSpace) [AlgebraicUncertainSpace U] [ExpectationStructure U] | ||
| [RenewalUpdateStrongAssumption U] : | ||
| RenewalUpdateTheoryStructure U where | ||
| elementary_renewal_distribution_statement := | ||
| RenewalUpdateStrongAssumption.elementary_renewal_distribution_statement (U := U) | ||
| elementary_renewal_expectation_statement := | ||
| RenewalUpdateStrongAssumption.elementary_renewal_expectation_statement (U := U) | ||
| renewal_reward_distribution_statement := | ||
| RenewalUpdateStrongAssumption.renewal_reward_distribution_statement (U := U) | ||
| renewal_reward_expectation_statement := | ||
| RenewalUpdateStrongAssumption.renewal_reward_expectation_statement (U := U) | ||
| elementary_renewal_distribution_axiom := | ||
| RenewalUpdateStrongAssumption.elementary_renewal_distribution_axiom (U := U) | ||
| elementary_renewal_expectation_axiom := | ||
| RenewalUpdateStrongAssumption.elementary_renewal_expectation_axiom (U := U) | ||
| renewal_reward_distribution_axiom := | ||
| RenewalUpdateStrongAssumption.renewal_reward_distribution_axiom (U := U) | ||
| renewal_reward_expectation_axiom := | ||
| RenewalUpdateStrongAssumption.renewal_reward_expectation_axiom (U := U) |
There was a problem hiding this comment.
These instances create a typeclass cycle (RenewalUpdateTheoryStructure ↔ RenewalUpdateStrongAssumption), which can cause typeclass search loops. Prefer a single instance direction (typically “strong assumptions ⇒ structure”) and make the other direction an explicit definition/lemma if you really need it.
There was a problem hiding this comment.
@copilot open a new pull request to apply changes based on this feedback
There was a problem hiding this comment.
def renewalUpdateStrong_of_structure
Mathlib/Uncertainty/base_core.lean
Outdated
| /-! | ||
| # Uncertainty theory basics | ||
|
|
||
| This module formalizes the foundational concepts of uncertainty theory, | ||
| including uncertain spaces, variables, and basic axioms. | ||
|
|
||
| ## Main definitions | ||
|
|
||
| * `UncertainSpace`: A measurable space with a σ-algebra and measure. | ||
| * `UncertainVariable`: A measurable function from an uncertain space to ℝ. | ||
| * `BookAxiomSet`: The four fundamental axioms of uncertainty theory. | ||
|
|
||
| ## References | ||
|
|
||
| * [1] Liu, B. (2026). *Uncertainty Theory* (5th ed.). Uncertainty Theory Laboratory. | ||
| Retrieved from https://cloud.tsinghua.edu.cn/d/df71e9ec330e49e59c9c/ | ||
| * [2] Liu, B. (2015). *Uncertainty Theory* (4th ed.). Springer Berlin, Heidelberg. | ||
| https://doi.org/10.1007/978-3-662-44354-5 | ||
|
|
||
| Authors: Prof. Dr. Fei Gao <[email protected]> | ||
| Date: 2026-03-02 | ||
|
|
||
| Copyright (c) 2026 Prof. Dr. Fei Gao. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| -/ |
There was a problem hiding this comment.
Mathlib files conventionally start with a non-doc /- ... -/ copyright header (separate from the module docstring). Here the copyright/authors/license text is embedded inside the /-! module doc, which will not match Mathlib style and may confuse tooling that expects the standard header block.
There was a problem hiding this comment.
@copilot open a new pull request to apply changes based on this feedback
There was a problem hiding this comment.
@copilot open a new pull request to apply changes based on this feedback
Co-authored-by: Copilot <[email protected]>
Co-authored-by: Copilot <[email protected]>
Co-authored-by: Copilot <[email protected]>
Co-authored-by: Copilot <[email protected]>
Co-authored-by: Copilot <[email protected]>
Co-authored-by: Copilot <[email protected]>
Co-authored-by: Copilot <[email protected]>
Co-authored-by: Copilot <[email protected]>
| instance (priority := 90) renewalUpdateStrong_of_structure | ||
| (U : UncertainSpace) [AlgebraicUncertainSpace U] [ExpectationStructure U] | ||
| [RenewalUpdateTheoryStructure U] : | ||
| RenewalUpdateStrongAssumption U where | ||
| elementary_renewal_distribution_statement := | ||
| RenewalUpdateTheoryStructure.elementary_renewal_distribution_statement (U := U) | ||
| elementary_renewal_expectation_statement := | ||
| RenewalUpdateTheoryStructure.elementary_renewal_expectation_statement (U := U) | ||
| renewal_reward_distribution_statement := | ||
| RenewalUpdateTheoryStructure.renewal_reward_distribution_statement (U := U) | ||
| renewal_reward_expectation_statement := | ||
| RenewalUpdateTheoryStructure.renewal_reward_expectation_statement (U := U) | ||
| elementary_renewal_distribution_axiom := | ||
| RenewalUpdateTheoryStructure.elementary_renewal_distribution_axiom (U := U) | ||
| elementary_renewal_expectation_axiom := | ||
| RenewalUpdateTheoryStructure.elementary_renewal_expectation_axiom (U := U) | ||
| renewal_reward_distribution_axiom := | ||
| RenewalUpdateTheoryStructure.renewal_reward_distribution_axiom (U := U) | ||
| renewal_reward_expectation_axiom := | ||
| RenewalUpdateTheoryStructure.renewal_reward_expectation_axiom (U := U) | ||
|
|
||
| instance (priority := 100) renewalUpdate_of_strongAssumption | ||
| (U : UncertainSpace) [AlgebraicUncertainSpace U] [ExpectationStructure U] | ||
| [RenewalUpdateStrongAssumption U] : | ||
| RenewalUpdateTheoryStructure U where | ||
| elementary_renewal_distribution_statement := | ||
| RenewalUpdateStrongAssumption.elementary_renewal_distribution_statement (U := U) | ||
| elementary_renewal_expectation_statement := | ||
| RenewalUpdateStrongAssumption.elementary_renewal_expectation_statement (U := U) | ||
| renewal_reward_distribution_statement := | ||
| RenewalUpdateStrongAssumption.renewal_reward_distribution_statement (U := U) | ||
| renewal_reward_expectation_statement := | ||
| RenewalUpdateStrongAssumption.renewal_reward_expectation_statement (U := U) | ||
| elementary_renewal_distribution_axiom := | ||
| RenewalUpdateStrongAssumption.elementary_renewal_distribution_axiom (U := U) | ||
| elementary_renewal_expectation_axiom := | ||
| RenewalUpdateStrongAssumption.elementary_renewal_expectation_axiom (U := U) | ||
| renewal_reward_distribution_axiom := | ||
| RenewalUpdateStrongAssumption.renewal_reward_distribution_axiom (U := U) | ||
| renewal_reward_expectation_axiom := | ||
| RenewalUpdateStrongAssumption.renewal_reward_expectation_axiom (U := U) |
There was a problem hiding this comment.
def renewalUpdateStrong_of_structure
