OAI/Geometry/SurfaceImmersion/Primitive/LocalPeriodicFamilies.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Smooth periodic coefficient families on the actual open geometric domain. Values outside that domain are fixed at zero, so equality only needs checking inside.

  1. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.smoothFamilies line 16
  2. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family line 27
  3. instance OAI.ClosedSurfaceR4.LocalPeriodicExpansion.(instance at line 28) line 28
  4. instance OAI.ClosedSurfaceR4.LocalPeriodicExpansion.(instance at line 29) line 29
  5. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.val line 34
  6. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.smooth line 35
  7. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.outside line 38
  8. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.ext line 40
  9. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.zero_apply line 47
  10. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.add_apply line 48
  11. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.sub_apply line 50
  12. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.neg_apply line 52
  13. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.smul_apply line 54
  14. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.sum_apply line 56
  15. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.ofLocal line 64

    Source documentation

    Restrict a locally smooth family to the admissible domain.

    def ofLocal (F : A → C(Period, E))
    (hF : ContDiffOn ℝ ∞ (fun z : A × ℝ => F z.1 (z.2 : Period)) ((O : Set A) ×ˢ Set.univ)) :
    Family O E :=
…

    Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family

  16. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.ofLocal_apply line 71
  17. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.angle line 78
  18. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.slow line 81
  19. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.angle_hasDerivAt line 84
  20. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.slow_apply line 89
  21. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.inner line 94
  22. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.inner_apply line 99
  23. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.constant line 102
  24. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.constant_apply line 106
  25. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.primitive line 112
  26. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.primitive_angle line 115
  27. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.primitive_mean_zero line 128
  28. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.slow_mean_zero line 137