OAI/Geometry/RCD/Sobolev/SupportedWeakSourceBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported tests for the vanishing viscosity term

  1. theorem OAI.RegularPointCoordinates.supported_test_slope_integrable line 14
  2. theorem OAI.RegularPointCoordinates.supported_weak_source_test_bound line 23
  3. theorem OAI.RegularPointCoordinates.supported_weak_source_vanishes line 36