OAI/Geometry/NearbyLagrangian/TransportCutoffs.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic and spatial cutoffs with uniform small-step data.

  1. lemma OAI.NearbyLagrangian.Transport.smoothTransition_derivative_bound line 17
  2. def OAI.NearbyLagrangian.Transport.logCutoff line 39
  3. lemma OAI.NearbyLagrangian.Transport.logCutoff_range line 43
  4. lemma OAI.NearbyLagrangian.Transport.logCutoff_one line 49
  5. lemma OAI.NearbyLagrangian.Transport.logCutoff_zero line 57
  6. lemma OAI.NearbyLagrangian.Transport.contDiff_logCutoff line 65
  7. lemma OAI.NearbyLagrangian.Transport.hasCompactSupport_logCutoff line 82
  8. lemma OAI.NearbyLagrangian.Transport.fderiv_logCutoff line 89
  9. lemma OAI.NearbyLagrangian.Transport.norm_fderiv_logCutoff_le line 111
  10. theorem OAI.NearbyLagrangian.Transport.exists_logarithmic_cutoff line 125
  11. theorem OAI.NearbyLagrangian.Transport.exists_logarithmic_cutoff_finite line 151
  12. theorem OAI.NearbyLagrangian.Transport.exists_spatial_cutoff line 204
  13. theorem OAI.NearbyLagrangian.Transport.exists_shift_buffer line 223
  14. lemma OAI.NearbyLagrangian.Transport.cutoff_cover_of_projected_support line 237
  15. theorem OAI.NearbyLagrangian.Transport.exists_displacement_cutoff line 248
  16. lemma OAI.NearbyLagrangian.Transport.product_cutoff_shift_mem line 264
  17. lemma OAI.NearbyLagrangian.Transport.base_mem_iff_of_compact_support line 287
  18. theorem OAI.NearbyLagrangian.Transport.exists_uniform_spatial_data line 319
  19. theorem OAI.NearbyLagrangian.Transport.exists_stepData_of_mixed line 333