OAI/Geometry/SurfaceImmersion/Correction/PositiveSmoothingAtlas.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Every smoothing atlas admits nonnegative square-partition weights with exactly the same supports and outer cutoffs. This makes the associated primitive amplitudes positive on their open nonzero loci.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveWeightNormalizer line 20
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveWeightNormalizer_pos line 23
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveWeightNormalizer_smooth line 37
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveWeight line 41
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveWeight_smooth line 44
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveWeight_nonneg line 54
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveWeight_pos_iff line 57
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveWeight_ne_zero_iff line 63
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveWeight_tsupport line 71
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveWeight_partition line 78
  11. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveAtlas line 91

    Source documentation

    The centers and outer functions are unchanged. Only the square partition is normalized, retaining every support exactly.

    def positiveAtlas : SmoothingAtlas M where
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas

  12. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveAtlas_weight_nonneg line 104
  13. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positiveAtlas_weight_tsupport line 107