OAI/Geometry/SurfaceImmersion/Atlas/WeightedComplexMixedJets.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Two-scale evaluation: the output is measured at the slow scale, while only the explicit jet excess contributes short-scale loss.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.slotLoss line 14
  2. theorem OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.compact_complex_mixed_bound line 17