Let bracketMeasure earn its name: E[(M_b − M_a)²] = ⟨M⟩((a,b]×Ω)

[raphaelrrcoelho]

context

ItoIntegralAgainstMartingale.bracketMeasure T hBmeas φ is defined as φ²·trim_T and called the bracket d⟨M⟩ of M = φ●B. The repo constructs no quadratic variation of M, so as of 2026-08-16 the name is motivation, not a theorem — the docstrings and docs/leaps.md were corrected to say exactly that rather than assert the identification.

The prose is now honest. The better fix is to make the name earned.

the statement

The unconditional identity is already within reach:

theorem norm_sq_increment_eq_bracket (T : ℝ≥0) (hBmeas : ∀ t, Measurable (B t))
    (φ : Lp ℝ 2 (trimMeasure_T (μ := μ) T hBmeas)) {a b : ℝ≥0} (hab : a ≤ b) (hbT : b ≤ T) :
    ‖itoProcessCLM hB T b hBmeas φ - itoProcessCLM hB T a hBmeas φ‖ ^ 2
      = ((bracketMeasure (μ := μ) T hBmeas φ) (Set.Ioc a b ×ˢ Set.univ)).toReal

i.e. 𝔼[(M_b − M_a)²] = ⟨M⟩((a,b] × Ω) — the defining property of the bracket at the level the tower can currently state it.

why it should be short

Every piece exists.

• M_b − M_a = itoIntegralCLM_T (bandRestrict T a b hBmeas φ) — this is the hband step inside itoIntegralAgainst_elementary; extract it as its own theorem itoIntegralCLM_T_bandRestrict first, it is wanted twice.
• itoIntegralCLM_T_norm turns that into ‖bandRestrict …‖.
• coeFn_bandRestrict says bandRestrict is 1_{(a,b]}·φ, so its L²(trim_T) norm² is ∫_{(a,b]×univ} φ² d(trim_T), which is bracketMeasure ((a,b]×univ) by withDensity_apply.

The work is the eLpNorm ↔ ∫⁻ ↔ toReal plumbing, not the mathematics. LpMulIsometry.enorm_sq_toReal and lintegral_sqWeight are the relevant helpers.

scope note

This is the unconditional second moment. The conditional identity 𝔼[(M_b − M_a)² | 𝓕_a] = 𝔼[⟨M⟩_b − ⟨M⟩_a | 𝓕_a] is the one a from-scratch construction of ∫ dM would have needed, and the design doc records that the tower does not have it. This issue does not close that; it delivers the unconditional version, which is what makes the name defensible.

acceptance criteria

• itoIntegralCLM_T_bandRestrict extracted, and itoIntegralAgainst_elementary refactored to consume it.
• The identity above, stated and proved.
• Docstring in ItoIntegralAgainstMartingale and the docs/leaps.md paragraph updated: the identification is no longer 'motivation' but is still the unconditional form.
• Axioms-clean; lake build MathFin && lake lint green; ledger re-verified.

Found in the 2026-08-16 coherence pass over the chain-rule tower.