OAI/Geometry/PrescribedPotential/QuasilinearLowResiduals.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Quasilinear Low Residuals.

  1. lemma OAI.HigherJet.norm_iteratedFDeriv_add_le line 25
  2. lemma OAI.HigherJet.low_coefficient_bounds line 34
  3. lemma OAI.HigherJet.frozen_equation_jet_norm line 68
  4. lemma OAI.HigherJet.quasilinear_low_residuals line 87