OAI/Geometry/PrescribedPotential/IntegerBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Integer Bounds.

  1. def OAI.SobolevChart.raiseZero line 21
  2. def OAI.SobolevChart.raiseDeriv line 26
  3. lemma OAI.SobolevChart.realize_raiseZero line 33
  4. lemma OAI.SobolevChart.realize_raiseDeriv line 37
  5. lemma OAI.SobolevChart.schwartzCoord_raise_one line 41
  6. lemma OAI.SobolevChart.coreBound_raise_one line 59
  7. lemma OAI.SobolevChart.coreBound_of_words_integer line 93
  8. theorem OAI.GlobalElliptic.chartTransport_integer_bound line 118
  9. theorem OAI.FrozenPoisson.ParameterRegularity.schwartzLocal_integer_bound line 132