L2IntegralRepresentative.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Identifying a Bochner integral with its pointwise representative

Testing against L2 functions and Fubini identifies the actual integral. The explicit product integrability condition is supplied by compact support and the uniform bound in the heat application.

theorem OAI.RegularPointCoordinates.L2_integral_representative line 19