context
three DRY items the martingale-representation reviews surfaced but left alone, because each is a change
to a file outside the program's scope. none is urgent; all three are the same failure mode, a general
fact living in an application file or inlined instead of consumed.
1. mulBddCLM should absorb the hand-rolled truncCLM
Foundations/ItoIntegralLocality.lean:155 defines mulBddCLM ν hg hgC, multiplication by a bounded
measurable function as an L² operator over an arbitrary measure, with its characterising a.e. identity
coeFn_mulBddCLM at :183. mathlib has no such operator.
Foundations/ItoIntegralProcessIsometry.lean:214 has truncCLM, a private hand-rolled special case:
multiplication by the indicator of a time band. it predates mulBddCLM and does the same work.
the blocker is DAG order. ItoIntegralLocality sits above ItoIntegralProcessIsometry, so mulBddCLM
has to move down before truncCLM can consume it. that move is the actual task; the deletion is two
lines after it.
2. inner_eq_integral_mul is public now, and should be consumed
Foundations/MartingaleRepresentation.lean:81 states ⟪f, g⟫_ℝ = ∫ ω, f ω * g ω ∂μ and was hoisted
public during the cleanup pass. the idiom it names is inlined as a bare rw [L2.inner_def] plus a
simp at, at least:
ItoIntegralL2.lean:196ItoIntegralL2Dense.lean:106ItoIntegralCLM.lean:579-581ItoIntegralCovariation.lean:78ItoIntegralProcessMartingale.lean:368WienerIntegralL2.lean:234-238, :431PoissonCompensatedIntegralOperator.lean:202
check each: some are rw ... at h on a hypothesis and may want the symmetric form, some may not be the
same idiom at all. and the same DAG problem applies, worse: MartingaleRepresentation is near the top of
the tower, so the lemma has to move down to ItoIntegralL2 or a shared L² prelude first.
3. ExpMartingaleQBrownian triplicates a five-step MGF block
Foundations/ExpMartingaleQBrownian.lean runs the same chain three times, at :114-125, :233-245 and
:346-358: integrableExpSet = univ from the gaussian, transfer along the MGF equality, interior is
univ, eqOn_complexMGF_of_mgf, Measure.ext_of_complexMGF_eq, rwa [Measure.map_id].
the shared content is one lemma: a real random variable whose Q-MGF equals the N(0,v) MGF has law
N(0,v). state it once as Measure.map X Q = gaussianReal 0 v from mgf X Q = mgf id (gaussianReal 0 v)
plus AEMeasurable X Q, and the three sites become one line each. this is pre-existing, not from the
representation program; it was found while checking whether the totality proof shared a root with it
(it does not, and that verdict stands).
acceptance criteria
pointers
MathFin/Foundations/ItoIntegralLocality.lean:155,183, ItoIntegralProcessIsometry.lean:212-241,
MartingaleRepresentation.lean:81, ExpMartingaleQBrownian.lean:114,233,346.
context
three DRY items the martingale-representation reviews surfaced but left alone, because each is a change
to a file outside the program's scope. none is urgent; all three are the same failure mode, a general
fact living in an application file or inlined instead of consumed.
1.
mulBddCLMshould absorb the hand-rolledtruncCLMFoundations/ItoIntegralLocality.lean:155definesmulBddCLM ν hg hgC, multiplication by a boundedmeasurable function as an
L²operator over an arbitrary measure, with its characterising a.e. identitycoeFn_mulBddCLMat:183. mathlib has no such operator.Foundations/ItoIntegralProcessIsometry.lean:214hastruncCLM, a private hand-rolled special case:multiplication by the indicator of a time band. it predates
mulBddCLMand does the same work.the blocker is DAG order.
ItoIntegralLocalitysits aboveItoIntegralProcessIsometry, somulBddCLMhas to move down before
truncCLMcan consume it. that move is the actual task; the deletion is twolines after it.
2.
inner_eq_integral_mulis public now, and should be consumedFoundations/MartingaleRepresentation.lean:81states⟪f, g⟫_ℝ = ∫ ω, f ω * g ω ∂μand was hoistedpublic during the cleanup pass. the idiom it names is inlined as a bare
rw [L2.inner_def]plus asimpat, at least:ItoIntegralL2.lean:196ItoIntegralL2Dense.lean:106ItoIntegralCLM.lean:579-581ItoIntegralCovariation.lean:78ItoIntegralProcessMartingale.lean:368WienerIntegralL2.lean:234-238,:431PoissonCompensatedIntegralOperator.lean:202check each: some are
rw ... at hon a hypothesis and may want the symmetric form, some may not be thesame idiom at all. and the same DAG problem applies, worse:
MartingaleRepresentationis near the top ofthe tower, so the lemma has to move down to
ItoIntegralL2or a sharedL²prelude first.3.
ExpMartingaleQBrowniantriplicates a five-step MGF blockFoundations/ExpMartingaleQBrownian.leanruns the same chain three times, at:114-125,:233-245and:346-358:integrableExpSet = univfrom the gaussian, transfer along the MGF equality,interiorisuniv,eqOn_complexMGF_of_mgf,Measure.ext_of_complexMGF_eq,rwa [Measure.map_id].the shared content is one lemma: a real random variable whose
Q-MGF equals theN(0,v)MGF has lawN(0,v). state it once asMeasure.map X Q = gaussianReal 0 vfrommgf X Q = mgf id (gaussianReal 0 v)plus
AEMeasurable X Q, and the three sites become one line each. this is pre-existing, not from therepresentation program; it was found while checking whether the totality proof shared a root with it
(it does not, and that verdict stands).
acceptance criteria
truncCLMdeleted, its call sites onmulBddCLM.inner_eq_integral_mulat a level where the tower can consume it, and consumed where it is thesame idiom.
lake build MathFin && lake lintgreen; ledger re-verified.pointers
MathFin/Foundations/ItoIntegralLocality.lean:155,183,ItoIntegralProcessIsometry.lean:212-241,MartingaleRepresentation.lean:81,ExpMartingaleQBrownian.lean:114,233,346.