OAI/Geometry/Immersion/ClosedSurface/WeightedBounds.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound line 17
  2. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.mono_order line 20
  3. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.mono_const line 24
  4. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.norm_le line 28
  5. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.deriv_le line 32
  6. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.shrink_scale line 38
  7. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.add line 43
  8. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.linear line 56
  9. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.fderivWithin line 67
  10. lemma OAI.ClosedSurfaceR4.WeightedEstimates.sum_choose_real line 77
  11. lemma OAI.ClosedSurfaceR4.WeightedEstimates.weighted_binomial_bound line 81
  12. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.bilinear line 107
  13. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.const_smul line 128
  14. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.neg line 140
  15. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.sub line 145
  16. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.clm_apply line 151
  17. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.clm_apply_const line 168
  18. def OAI.ClosedSurfaceR4.WeightedEstimates.firstOrder line 183
  19. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.firstOrder line 186
  20. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.comp line 206
  21. lemma OAI.ClosedSurfaceR4.WeightedEstimates.compact_coefficient_bound line 237
  22. lemma OAI.ClosedSurfaceR4.WeightedEstimates.smooth_compact_weighted_bound line 262
  23. lemma OAI.ClosedSurfaceR4.WeightedEstimates.contDiffOn_firstOrder line 275
  24. def OAI.ClosedSurfaceR4.WeightedEstimates.scaledHierarchy line 283
  25. lemma OAI.ClosedSurfaceR4.WeightedEstimates.contDiffOn_scaledHierarchy line 288
  26. lemma OAI.ClosedSurfaceR4.WeightedEstimates.weighted_scaledHierarchy line 298
  27. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.congr line 333
  28. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.mul line 339
  29. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.const_mul line 356
  30. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.directional line 368
  31. lemma OAI.ClosedSurfaceR4.WeightedEstimates.iteratedFDerivWithin_pi_smooth line 380
  32. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.pi line 394
  33. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.component line 405
  34. lemma OAI.ClosedSurfaceR4.WeightedEstimates.weightedBound_zero line 416
  35. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.finset_sum line 421
  36. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.dot line 437
  37. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.complex_smul_pi line 451