OAI/Geometry/SurfaceImmersion/Correction/CombinedMeanGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact mean identity, support and global smoothness for the combined mean.

  1. lemma OAI.ClosedSurfaceR4.SmallModes.seedMeanError_zero_outside line 12
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.combinedSeedMean_tsupport line 32
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.combinedSeedMean_smooth line 56
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.combined_seed_mean_identity line 71