OAI/Geometry/NearbyLagrangian/RadialBlending.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Radial interpolation without new critical points outside a bounded set.

  1. def OAI.NearbyLagrangian.InfinityRestore.blend line 15
  2. lemma OAI.NearbyLagrangian.InfinityRestore.fderiv_blend line 17
  3. lemma OAI.NearbyLagrangian.InfinityRestore.norm_fderiv_blend_sub_le line 31
  4. lemma OAI.NearbyLagrangian.InfinityRestore.fderiv_ne_zero_of_error_lt line 65
  5. def OAI.NearbyLagrangian.InfinityRestore.unitBump line 74
  6. def OAI.NearbyLagrangian.InfinityRestore.radialCutoff line 76
  7. lemma OAI.NearbyLagrangian.InfinityRestore.contDiff_radialCutoff line 78
  8. lemma OAI.NearbyLagrangian.InfinityRestore.radialCutoff_mem_Icc line 81
  9. lemma OAI.NearbyLagrangian.InfinityRestore.radialCutoff_eq_zero line 86
  10. lemma OAI.NearbyLagrangian.InfinityRestore.radialCutoff_eq_one line 95
  11. lemma OAI.NearbyLagrangian.InfinityRestore.exists_unitBump_derivative_bound line 106
  12. lemma OAI.NearbyLagrangian.InfinityRestore.norm_fderiv_radialCutoff_le line 116
  13. lemma OAI.NearbyLagrangian.InfinityRestore.blend_radial_eq_inner line 145
  14. lemma OAI.NearbyLagrangian.InfinityRestore.blend_radial_eq_outer line 149
  15. lemma OAI.NearbyLagrangian.InfinityRestore.blend_radial_inner_eventuallyEq line 153
  16. lemma OAI.NearbyLagrangian.InfinityRestore.blend_radial_outer_eventuallyEq line 158
  17. lemma OAI.NearbyLagrangian.InfinityRestore.contDiff_blend_radial line 163
  18. lemma OAI.NearbyLagrangian.InfinityRestore.critical_radius_bound line 176
  19. lemma OAI.NearbyLagrangian.InfinityRestore.annulus_error_estimate line 184
  20. lemma OAI.NearbyLagrangian.InfinityRestore.blend_radial_annulus_noncritical line 199
  21. lemma OAI.NearbyLagrangian.InfinityRestore.blend_radial_noncritical_outside line 228
  22. theorem OAI.NearbyLagrangian.InfinityRestore.blend_radial_preserves_critical line 252
  23. lemma OAI.NearbyLagrangian.InfinityRestore.exists_restoration_radius line 276