OAI/Geometry/RCD/Sobolev/BochnerMixedRecovery.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Removing the amplitude restriction from the Laplacian in mixed tests

Bounded Sobolev recovery converges strongly. With one bounded-gradient factor, both remaining products are L² pairings, so the product identity passes to an unbounded Sobolev Laplacian.

  1. theorem OAI.RegularPointCoordinates.mixed_bounded_test line 22
  2. theorem OAI.RegularPointCoordinates.weakLaplacian_mixed_identity_L2 line 59