L¹/H¹ martingale representation, and Clark–Ocone (the named integrand)

[raphaelrrcoelho]

context

Foundations/MartingaleRepresentation.lean is an L² theorem, and it is L² for a structural reason:
the proof is an orthogonal decomposition in a hilbert space. exists_itoIntegral_representation gives
F = 𝔼[F] + ∫₀ᵀ φ dB for F ∈ L²(𝓕ᴮ_T), with φ unique because an isometry is injective. two things
are missing and they are usually wanted together.

the L¹/H¹ statement. every L¹ martingale on the brownian filtration is M_0 + ∫φ dB with φ
only locally square-integrable. the hilbert argument does not reach it: there is no inner product to be
orthogonal in. the standard route is localization by stopping times against the L² theorem, plus
H¹-BMO duality for the H¹ refinement. this matters for pricing claims that are integrable but not
square-integrable, which is most of the ones with fat tails.

clark–ocone. the theorem above says a φ exists and is unique but never says what it is. clark–ocone
does: φ_t = 𝔼[D_t F | 𝓕_t], the conditional expectation of the malliavin derivative. that is the
formula that turns "a hedge exists" into "here is the hedge", and it is what a delta actually is.

the blocker

mathlib has no malliavin calculus. so clark–ocone is a build from the ground: the wiener chaos
decomposition or the derivative operator on cylinder functionals, its closability, and the duality with
the skorokhod integral. the L¹/H¹ half is nearer and does not need any of it.

worth noting the neighbouring gap: even without malliavin, the library cannot currently name the
integrand of the localized itô formula either (see #183 and docs/roadmap.md). the two are independent routes to the same missing capability,
naming a diffusion coefficient.

task

split as you like, but the natural order is L¹/H¹ first (localization against the existing L²
theorem), clark–ocone second (a malliavin build).

acceptance criteria

• L¹ representation on the brownian filtration, with the integrand in the locally-L² class.
• a full entry; axioms-clean; coverage row + audit + ledger updated.
• clark–ocone tracked separately once the malliavin prerequisites are scoped.

pointers

• MathFin/Foundations/MartingaleRepresentation.lean (the L² theorem to localize against),
  ItoIntegralProcessLocalMartingaleGeneral.lean (the localization machinery already in the tower).
• Foundations/ItoIntegralL2Dense.lean for the density argument the L² domain rests on.