OAI/Geometry/SurfaceImmersion/Primitive/CircularFlatBump.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Flat cutoffs for the actual circular disks in primitive preparation. Their centers and radii are smooth parameters.

  1. def OAI.ClosedSurfaceR4.PhaseGeometry.circularRadiusSquared line 16
  2. def OAI.ClosedSurfaceR4.PhaseGeometry.circularFlatBump line 18
  3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularRadiusSquared_smooth line 21
  4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularFlatBump_joint_smooth line 26
  5. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularFlatBump_smooth line 32
  6. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularFlatBump_nonneg line 36
  7. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularFlatBump_zero_iff line 39
  8. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularFlatBump_pos_iff line 43
  9. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularFlatBump_support line 53
  10. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularRadiusSquared_le_norm line 59
  11. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularFlatBump_hasCompactSupport line 72
  12. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularRadiusSquared_derivative line 82
  13. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularRadiusSquared_boundary_regular line 97
  14. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularFlatBump_spatial_derivative line 110
  15. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularFlatBump_spatial_derivative_continuous line 119
  16. lemma OAI.ClosedSurfaceR4.PhaseGeometry.compact_parameter_nearby line 126
  17. theorem OAI.ClosedSurfaceR4.PhaseGeometry.circularFlatBump_compact_C1 line 143

    Source documentation

    Moving a center or radius changes its actual flat cutoff by an arbitrarily small amount in C¹ on any fixed compact coordinate set.

    theorem circularFlatBump_compact_C1 {K : Set Base} (hK : IsCompact K)
    (q : Base × ℝ) {eps : ℝ} (heps : 0 < eps) :
    ∃ delta : ℝ, 0 < delta ∧ ∀ q' : Base × ℝ, ‖q'-q‖ < delta → ∀ p ∈ K,
      |circularFlatBump q'.1 q'.2 p - circularFlatBump q.1 q.2 p| < eps ∧
      ‖fderiv ℝ (circularFlatBump q'.1 q'.2) p -
        fderiv ℝ (circularFlatBump q.1 q.2) p‖ < eps := by
…

    Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.circularFlatBump