Revision #3171 → #3684 · back to history
modifiedMartingale (informal)e1d80f7ceaa7
| Field | From #3171 | To #3684 |
|---|
| note | The Mathlib definition `Martingale f ℱ μ := StronglyAdapted ℱ f ∧ ∀ i ≤ j, μ[f j | ℱ i] =ᵐ[μ] f i` directly captures the informal idea that the conditional expectation of the next value equals the present value. | Verified: `MeasureTheory.Martingale` in `Mathlib.Probability.Martingale.Basic` directly captures the informal conditional-expectation martingale property. |
modifiedConditional expectatione995a26056c9
| Field | From #3171 | To #3684 |
|---|
| note | Mathlib's `condExp` is the general conditional expectation with respect to a sub-σ-algebra used to state the martingale property. | Verified: `MeasureTheory.condExp` is Mathlib's conditional expectation with respect to a sub-σ-algebra. |
modifiedDiscrete-time martingale6b8660f1625c
| Field | From #3171 | To #3684 |
|---|
| note | Mathlib's `Martingale` is defined for any `Preorder ι`, specializing to the discrete-time case when `ι = ℕ`. | `MeasureTheory.Martingale` is defined over any `Preorder ι`, specializing to the discrete case `ι = ℕ`. |
modifiedMartingale with respect to another sequencee8382c57c88b
| Field | From #3171 | To #3684 |
|---|
| note | Mathlib defines martingales relative to a filtration rather than another process directly; the notion is recoverable by combining `Martingale` with `Filtration.natural` of the reference process, but is not packaged as a single decl. | Mathlib phrases martingales via a filtration; combining `Martingale` with `Filtration.natural` of the reference process recovers this but there is no single packaged decl. |
modifiedContinuous-time martingale with respect to a process5bb3a8bd300b
| Field | From #3171 | To #3684 |
|---|
| note | Same as the discrete case: `Martingale` over a continuous index `ι` together with `Filtration.natural` of the conditioning process expresses this, but it is not a dedicated decl. | `Martingale` over continuous `ι` together with `Filtration.natural` expresses this but is not packaged as its own decl. |
modifiedGeneral martingale (Banach-space valued)bd357090ea5b
| Field | From #3171 | To #3684 |
|---|
| note | `Martingale` is defined with values in any `E` that is a `NormedAddCommGroup`/`NormedSpace ℝ E`/`CompleteSpace`, i.e. Banach-space valued, on any `Preorder ι`. | `MeasureTheory.Martingale` is defined for values in any `NormedAddCommGroup`/`NormedSpace ℝ E`/`CompleteSpace`, i.e. Banach-valued. |
modifiedFiltrationb0e90e8227c5
| Field | From #3171 | To #3684 |
|---|
| note | `MeasureTheory.Filtration ι m` is a monotone family of sub-σ-algebras of `m`, exactly the filtration used in the martingale definition. | Verified: `MeasureTheory.Filtration` is a monotone family of sub-σ-algebras. |
modifiedAdapted processe0bb8ecd6d26
| Field | From #3171 | To #3684 |
|---|
| note | `MeasureTheory.Adapted ℱ f` states that each `f i` is `ℱ i`-strongly measurable, matching the informal adaptedness condition. | Verified: `MeasureTheory.Adapted ℱ f` requires each `f i` to be `ℱ i`-strongly measurable. |
modifiedL^p integrability of process09720453ca98
| Field | From #3171 | To #3684 |
|---|
| mathlib.module | Mathlib.MeasureTheory.Function.LpSpace | Mathlib.MeasureTheory.Function.LpSeminorm.Defs |
| note | `MemLp f p μ` expresses membership in `L^p(Ω;E)`, used in Mathlib's martingale definition via `Integrable` (the `p = 1` case). | Verified: `MeasureTheory.MemLp f p μ` expresses `L^p` membership; the martingale definition uses the `p = 1` case via `Integrable`. |
modifiedUnbiased random walk9514a13528e7
| Field | From #3171 | To #3684 |
|---|
| note | No declaration constructing the unbiased random walk and proving it is a martingale was found in Mathlib. | No decl constructs the unbiased random walk and proves it is a martingale. |
modifiedGambler's fortune in a fair game29288bc7413e
| Field | From #3171 | To #3684 |
|---|
| note | No Mathlib decl formalizes the gambler-fortune fair-game example as a martingale. | No Mathlib decl formalizes the fair-game gambler-fortune example. |
modifiedSquared-fortune martingaleb0d0ed7c5782
| Field | From #3171 | To #3684 |
|---|
| note | The martingale `X_n^2 − n` for a fair-coin walk is not formalized as a named decl. | The `X_n^2 − n` martingale is not formalized as a named decl. |
modifiedPólya's urn38b28acc0690
| Field | From #3171 | To #3684 |
|---|
| note | Pólya's urn process is not formalized in `Mathlib/Probability`. | Pólya's urn is not formalized in `Mathlib/Probability`. |
modifiedLikelihood-ratio martingale83a8bb0767a3
| Field | From #3171 | To #3684 |
|---|
| note | No Mathlib decl establishes the sequence of likelihood ratios as a martingale. | No Mathlib decl establishes the likelihood-ratio process as a martingale. |
modifiedDoob martingalef8c0a9524d52
| Field | From #3171 | To #3684 |
|---|
| note | `martingale_condExp` proves that `fun i => μ[f | ℱ i]` is a martingale, which is precisely the Doob martingale construction. | Verified: `martingale_condExp` shows `fun i => μ[f | ℱ i]` is a martingale — the Doob martingale. |
modifiedEcological community species counte9578d3aae55
| Field | From #3171 | To #3684 |
|---|
| note | This ecological application is not formalized. | The ecological application is not formalized. |
modifiedCompensated Poisson process6600615e3c32
| Field | From #3171 | To #3684 |
|---|
| note | No Poisson-process construction or compensated-Poisson martingale was found in Mathlib. | No Poisson-process construction or compensated Poisson martingale is in Mathlib. |
modifiedWald's martingale5def4a086458
| Field | From #3171 | To #3684 |
|---|
| note | Wald's martingale (the moment-generating-function product martingale) is not formalized. | Wald's martingale is not formalized. |
modifiedDiscounted asset price under risk-neutral measuredec179ebf66c
| Field | From #3171 | To #3684 |
|---|
| note | Mathematical-finance asset-pricing martingale is not formalized in Mathlib. | The asset-pricing martingale is not formalized in Mathlib. |
modifiedMulti-dimensional martingale29c3b884c077
| Field | From #3171 | To #3684 |
|---|
| note | `Martingale` is parameterized by an arbitrary Banach space `E`, so the multi-dimensional case `E = ℝ^d` is a specialization. | `Martingale` is parameterized by a Banach space `E`, so `E = ℝ^d` is a specialization. |
modifiedHarmonic function of Brownian motion is a martingalec8eb98c9c61e
| Field | From #3171 | To #3684 |
|---|
| note | Brownian motion is not yet formalized in Mathlib, so the harmonic-function martingale statement is unavailable. | Brownian motion is not yet formalized in Mathlib, so this result is unavailable. |
modifiedDiscrete-time submartingaled408e9ff0809
| Field | From #3171 | To #3684 |
|---|
| note | `Submartingale f ℱ μ` is defined for any `Preorder ι`, specializing to `ι = ℕ` for the discrete-time case. | Verified: `MeasureTheory.Submartingale` is defined over any `Preorder ι`. |
modifiedContinuous-time submartingale7eb59e8454f5
| Field | From #3171 | To #3684 |
|---|
| note | Same `Submartingale` decl handles continuous time when `ι` is e.g. `ℝ≥0` or `ℝ`. | Same `Submartingale` decl handles continuous time. |
modifiedDiscrete-time supermartingale87df769aae7b
| Field | From #3171 | To #3684 |
|---|
| note | `Supermartingale f ℱ μ` is defined for any `Preorder ι`; the discrete case is `ι = ℕ`. | Verified: `MeasureTheory.Supermartingale` over any `Preorder ι`. |
modifiedMartingale iff sub- and supermartingale4b33b0e91c41
| Field | From #3171 | To #3684 |
|---|
| note | `martingale_iff` states `Martingale f ℱ μ ↔ Supermartingale f ℱ μ ∧ Submartingale f ℱ μ`. | Verified: `martingale_iff : Martingale f ℱ μ ↔ Supermartingale f ℱ μ ∧ Submartingale f ℱ μ`. |
modifiedBiased coin gambler — martingale case9491d597f7a3
| Field | From #3171 | To #3684 |
|---|
| note | Not formalized as a named example in Mathlib. | Not formalized as a named example. |
modifiedBiased coin gambler — supermartingale case2c9053c4807d
| Field | From #3171 | To #3684 |
|---|
| note | Not formalized as a named example in Mathlib. | Not formalized as a named example. |
modifiedBiased coin gambler — submartingale case040afcdbbc5d
| Field | From #3171 | To #3684 |
|---|
| note | Not formalized as a named example in Mathlib. | Not formalized as a named example. |
modifiedConvex function of a martingale is a submartingalebae1d4532f63
| Field | From #3171 | To #3684 |
|---|
| note | No `ConvexOn`-of-martingale-is-submartingale decl was located in `Mathlib/Probability`. | No dedicated `ConvexOn`-of-martingale-is-submartingale decl found in `Mathlib/Probability`. |
modifiedStopping time4b92372bc62a
| Field | From #3171 | To #3684 |
|---|
| note | `IsStoppingTime f τ` is defined as the condition that `{ω | τ ω ≤ i}` is `f i`-measurable for every `i`. | Verified: `IsStoppingTime f τ` requires `{ω | τ ω ≤ i}` to be `f i`-measurable for every `i`. |
modifiedStopped martingale is a martingale3cd2f09bcdcb
| Field | From #3171 | To #3684 |
|---|
| note | Only `Submartingale.stoppedProcess` is provided; the martingale (and supermartingale) versions are not stated as their own decls, though they follow via `martingale_iff` and negation. | Only the submartingale form is a dedicated decl; the martingale/supermartingale versions follow via `martingale_iff` but are not stated as their own lemmas. |
modifiedOptional stopping theorem74f21d9431b4
| Field | From #3171 | To #3684 |
|---|
| note | This iff-form of Doob's optional stopping theorem characterizes submartingales via monotonicity of expected stopped values over bounded stopping times. | Verified: this iff-form of Doob's optional stopping theorem characterizes submartingales via monotonicity of expected stopped values over bounded stopping times. |
modifiedGeneral martingale problem (A, μ)5410a12b6550
| Field | From #3171 | To #3684 |
|---|
| note | The Stroock–Varadhan martingale problem formulation is not formalized in Mathlib. | The Stroock–Varadhan martingale problem is not formalized in Mathlib. |
modifiedMartingale problem ↔ SDE correspondence55084ee8624c
| Field | From #3171 | To #3684 |
|---|
| note | SDEs and the martingale-problem/SDE correspondence are not formalized in Mathlib. | SDEs and the martingale-problem/SDE correspondence are not formalized. |
modifiedFundamental theorem of asset pricing507b07242ca3
| Field | From #3171 | To #3684 |
|---|
| note | Mathematical-finance results including the fundamental theorem of asset pricing are not formalized in Mathlib. | Mathematical-finance results including FTAP are not formalized. |
modifiedRisk-neutral pricinga4af6a2c8a1b
| Field | From #3171 | To #3684 |
|---|
| note | Risk-neutral valuation under an equivalent martingale measure is not formalized. | Risk-neutral valuation is not formalized. |
modifiedGirsanov theorema9b8208b157f
| Field | From #3171 | To #3684 |
|---|
| note | Girsanov's theorem (change of measure under a Brownian drift) is not formalized in Mathlib. | Girsanov's theorem is not formalized in Mathlib. |
addedStopped process645041f873c3
addedLocal martingale1339103e6db1
addedJensen's inequality (for convex functions and expectations)dfc928778775
addedStandard Brownian motionf2514519ef6d
addedPoisson processe356367742e5
addedMoment-generating function14a0cdc8d556
addedSkorokhod space46ed943071e3