OAI/Geometry/RCD/Heat/HeatBochnerForm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weak Bochner with ordinary bounded Sobolev tests

The energy density is already Sobolev. Strong heat convergence in that space and L² convergence of the mixed pairing remove the smoothed weight.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_bochner_sobolev_test line 20