OAI/Geometry/NearbyLagrangian/SmoothCore.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Core smoothing, controlled linear cutoffs and exponential scales.

  1. def OAI.NearbyLagrangian.CoreSmoothing.coreBump line 17
  2. def OAI.NearbyLagrangian.CoreSmoothing.smoothCore line 19
  3. lemma OAI.NearbyLagrangian.CoreSmoothing.smoothCore_eq_zero line 23
  4. lemma OAI.NearbyLagrangian.CoreSmoothing.smoothCore_eq line 30
  5. theorem OAI.NearbyLagrangian.CoreSmoothing.contMDiff_smoothCore line 36
  6. lemma OAI.NearbyLagrangian.CoreSmoothing.contMDiffAt_vertical line 54
  7. theorem OAI.NearbyLagrangian.CoreSmoothing.exists_core_bound line 68
  8. def OAI.NearbyLagrangian.Cutoff.cutoffLinear line 93
  9. def OAI.NearbyLagrangian.Cutoff.family line 96
  10. lemma OAI.NearbyLagrangian.Cutoff.differentiableAt_cutoffLinear line 99
  11. theorem OAI.NearbyLagrangian.Cutoff.contDiff_cutoffLinear line 109
  12. theorem OAI.NearbyLagrangian.Cutoff.contDiff_cutoffLinear_joint line 125
  13. lemma OAI.NearbyLagrangian.Cutoff.norm_fderiv_radialCutoff line 142
  14. theorem OAI.NearbyLagrangian.Cutoff.norm_fderiv_cutoffLinear_le line 155
  15. lemma OAI.NearbyLagrangian.Cutoff.fderiv_family_core line 181
  16. lemma OAI.NearbyLagrangian.Cutoff.fderiv_eq_of_eq_outside line 192
  17. theorem OAI.NearbyLagrangian.Cutoff.no_inner_critical line 199
  18. theorem OAI.NearbyLagrangian.Cutoff.no_outer_critical line 211
  19. theorem OAI.NearbyLagrangian.Cutoff.critical_iff line 238
  20. theorem OAI.NearbyLagrangian.Cutoff.family_eq_outside line 289
  21. def OAI.NearbyLagrangian.Cutoff.betaBump line 298
  22. def OAI.NearbyLagrangian.Cutoff.beta line 300
  23. lemma OAI.NearbyLagrangian.Cutoff.contDiff_beta line 302
  24. lemma OAI.NearbyLagrangian.Cutoff.beta_mem_Icc line 304
  25. lemma OAI.NearbyLagrangian.Cutoff.beta_eq_one line 307
  26. lemma OAI.NearbyLagrangian.Cutoff.beta_eq_zero line 311
  27. def OAI.NearbyLagrangian.Cutoff.cutoffControl line 315
  28. lemma OAI.NearbyLagrangian.Cutoff.beta_control_bddAbove line 318
  29. lemma OAI.NearbyLagrangian.Cutoff.beta_le_control line 334
  30. lemma OAI.NearbyLagrangian.Cutoff.one_le_beta_control line 338
  31. def OAI.NearbyLagrangian.Scales.exponentialScale line 348
  32. lemma OAI.NearbyLagrangian.Scales.exponentialScale_pos line 351
  33. theorem OAI.NearbyLagrangian.Scales.exists_source_scales line 354
  34. theorem OAI.NearbyLagrangian.Scales.contMDiff_exponentialScale line 394
  35. theorem OAI.NearbyLagrangian.Scales.mfderiv_exponentialScale line 399