context
Foundations/MarketCompleteness.lean hypothesises PricesGainsAtZero Q (:173) rather than deriving
it, and keeps that honest with two proved facts:
pricesGainsAtZero_self (:180), that μ itself satisfies it, so nothing downstream is vacuous;pricesGainsAtZero_of_gains_martingale (:198), that the textbook condition (the gains process is a
Q-martingale started at 0) implies it.
the two are never composed. pricesGainsAtZero_self is proved directly from the centering theorem
integral_itoIntegralCLM_T, so the second guard's hypothesis triple is never exhibited as inhabited.
both guards are individually non-trivial, but the file never shows that the textbook condition holds for
any measure at all.
task
prove pricesGainsAtZero_self through the guard, with V φ := itoProcessCLM hB T · hBmeas φ. then
the second guard becomes load-bearing and the composition is exhibited.
the real cost, and the reason it was deferred: the repo has a bundled Martingale only for
itoSimpleProcess. for a general integrand there is only the pointwise
itoIntegralProcessGen_isMartingale. so this needs the general-integrand itô integral process bundled
as a Martingale, which is a small but genuine addition to ItoIntegralProcessGeneral.
that bundle is worth having independently. it is the object every "the gains process is a martingale"
statement wants to be stated on.
acceptance criteria
pointers
MathFin/Foundations/MarketCompleteness.lean:173-210,
Foundations/ItoIntegralProcessGeneral.lean (itoIntegralProcessGen_isMartingale,
integral_itoIntegralCLM_T, itoProcessCLM_zero_time),
Foundations/ItoIntegralProcessMartingale.lean (the simple-process bundle to model it on).
context
Foundations/MarketCompleteness.leanhypothesisesPricesGainsAtZero Q(:173) rather than derivingit, and keeps that honest with two proved facts:
pricesGainsAtZero_self(:180), thatμitself satisfies it, so nothing downstream is vacuous;pricesGainsAtZero_of_gains_martingale(:198), that the textbook condition (the gains process is aQ-martingale started at0) implies it.the two are never composed.
pricesGainsAtZero_selfis proved directly from the centering theoremintegral_itoIntegralCLM_T, so the second guard's hypothesis triple is never exhibited as inhabited.both guards are individually non-trivial, but the file never shows that the textbook condition holds for
any measure at all.
task
prove
pricesGainsAtZero_selfthrough the guard, withV φ := itoProcessCLM hB T · hBmeas φ. thenthe second guard becomes load-bearing and the composition is exhibited.
the real cost, and the reason it was deferred: the repo has a bundled
Martingaleonly foritoSimpleProcess. for a general integrand there is only the pointwiseitoIntegralProcessGen_isMartingale. so this needs the general-integrand itô integral process bundledas a
Martingale, which is a small but genuine addition toItoIntegralProcessGeneral.that bundle is worth having independently. it is the object every "the gains process is a martingale"
statement wants to be stated on.
acceptance criteria
Martingale.pricesGainsAtZero_selfderived viapricesGainsAtZero_of_gains_martingale.lake build MathFin && lake lintgreen; ledger re-verified.pointers
MathFin/Foundations/MarketCompleteness.lean:173-210,Foundations/ItoIntegralProcessGeneral.lean(itoIntegralProcessGen_isMartingale,integral_itoIntegralCLM_T,itoProcessCLM_zero_time),Foundations/ItoIntegralProcessMartingale.lean(the simple-process bundle to model it on).