OAI/Analysis/LipschitzHilbert/Estimates/EndpointWeightBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Endpoint variation bounds in the inverse-fourth-power form used by the source amplitude motion argument.

  1. theorem OAI.LipschitzHilbert.endpoint_variation_le_add line 13
  2. theorem OAI.LipschitzHilbert.boundary_weight_variation_fourth line 33