OAI/Geometry/RCD/Heat/FisherBochnerIdentity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact identity between Fisher variation and logarithmic Bochner

Every cancellation uses an actual bounded Sobolev test. Both Laplacian sources may be unbounded L² functions.

  1. theorem OAI.RegularPointCoordinates.shifted_product_coe line 20
  2. theorem OAI.RegularPointCoordinates.fisher_bochner_identity line 34