OAI/Geometry/BallPacking/Holder/KernelSchauder.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HigherDimensionalBallPacking.Rigidity.smoothCauchyKernel_second_directional line 13
  2. lemma OAI.HigherDimensionalBallPacking.Rigidity.smoothCauchyKernel_second_norm line 51
  3. lemma OAI.HigherDimensionalBallPacking.Rigidity.second_directional_eq line 96
  4. lemma OAI.HigherDimensionalBallPacking.Rigidity.norm_second_jet line 103
  5. lemma OAI.HigherDimensionalBallPacking.Rigidity.second_directional_norm_le line 107
  6. lemma OAI.HigherDimensionalBallPacking.Rigidity.norm_first_smul_le line 117
  7. lemma OAI.HigherDimensionalBallPacking.Rigidity.norm_second_smul_le line 126
  8. lemma OAI.HigherDimensionalBallPacking.Rigidity.norm_first_rescale line 138
  9. lemma OAI.HigherDimensionalBallPacking.Rigidity.norm_second_rescale line 146
  10. def OAI.HigherDimensionalBallPacking.Rigidity.schauderBump line 159
  11. def OAI.HigherDimensionalBallPacking.Rigidity.scaledSchauderBump line 165
  12. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledSchauderBump_smooth line 167
  13. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledSchauderBump_compact line 170
  14. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledSchauderBump_range line 174
  15. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledSchauderBump_tsupport line 177
  16. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledSchauderBump_eventually_one line 190
  17. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledSchauderBump_homogeneous_bounds line 201
  18. lemma OAI.HigherDimensionalBallPacking.Rigidity.smoothCauchyKernel_first_opNorm line 238
  19. lemma OAI.HigherDimensionalBallPacking.Rigidity.smoothCauchyKernel_second_opNorm line 243
  20. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoff_smoothCauchyKernel_jet_bounds line 253
  21. def OAI.HigherDimensionalBallPacking.Rigidity.schauderNearWeight line 318
  22. def OAI.HigherDimensionalBallPacking.Rigidity.schauderFarWeight line 321
  23. lemma OAI.HigherDimensionalBallPacking.Rigidity.schauderNearWeight_nonneg line 324
  24. lemma OAI.HigherDimensionalBallPacking.Rigidity.schauderFarWeight_nonneg line 327
  25. lemma OAI.HigherDimensionalBallPacking.Rigidity.schauderNearWeight_integrable line 332
  26. lemma OAI.HigherDimensionalBallPacking.Rigidity.schauderFarWeight_integrable line 341
  27. def OAI.HigherDimensionalBallPacking.Rigidity.scaledSchauderWeight line 358
  28. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledSchauderWeight_integrable line 361
  29. lemma OAI.HigherDimensionalBallPacking.Rigidity.integral_scaledSchauderWeight line 365
  30. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledNearWeight_value line 373
  31. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledFarWeight_value line 388
  32. lemma OAI.HigherDimensionalBallPacking.Rigidity.compact_kernel_convolution_direction line 411
  33. lemma OAI.HigherDimensionalBallPacking.Rigidity.compact_kernel_convolution_derivative_lipschitz line 419
  34. lemma OAI.HigherDimensionalBallPacking.Rigidity.compact_convolution_split_fderiv line 449
  35. lemma OAI.HigherDimensionalBallPacking.Rigidity.compact_convolution_split_derivative_bound line 469