OAI/Geometry/Perimeter/Regularity/EllipticOneScale.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.weak_curl_harmonic_comparison_norm line 11
  2. theorem OAI.RPISingularHarnack.vectorLp_integral_sq line 30
  3. theorem OAI.RPISingularHarnack.vectorLp_integrable_sq line 34
  4. theorem OAI.RPISingularHarnack.vectorLp_setIntegral_sq_le line 37
  5. theorem OAI.RPISingularHarnack.norm_sub_sq_le_two line 42
  6. theorem OAI.RPISingularHarnack.weak_field_one_scale line 49