OAI/Geometry/CubicTorus/Estimates/HolderNear.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.forced_cmc_linearized_holder_gradient line 13
  2. lemma OAI.CubicTorus.compact_probability_average_integrable line 57
  3. lemma OAI.CubicTorus.compact_probability_average_uniform line 64
  4. lemma OAI.CubicTorus.vector_graphSmooth_eq_convolution line 85
  5. lemma OAI.CubicTorus.test_kernel_support line 106
  6. lemma OAI.CubicTorus.PlaneWeakGradient.smooth_hasFDerivAt line 128
  7. lemma OAI.CubicTorus.PlaneWeakGradient.compact_hasFDerivAt line 191
  8. lemma OAI.CubicTorus.PlaneWeakGradient.continuous_hasFDerivAt line 209
  9. lemma OAI.CubicTorus.linear_cmc_source_holder line 255
  10. theorem OAI.CubicTorus.PlaneWeakGradient.holder_C1 line 333
  11. theorem OAI.CubicTorus.LinearCMCEquation.directional_holder_C1 line 368
  12. lemma OAI.CubicTorus.LinearCMCEquation.mono line 439
  13. lemma OAI.CubicTorus.LinearCMCEquation.congr line 443
  14. def OAI.CubicTorus.HolderNear line 472
  15. lemma OAI.CubicTorus.HolderNear.continuousAt line 481
  16. lemma OAI.CubicTorus.HolderNear.eventually line 494
  17. lemma OAI.CubicTorus.HolderNear.contDiffAt_zero line 506
  18. lemma OAI.CubicTorus.HolderNear.congr line 511
  19. lemma OAI.CubicTorus.ContDiffAt.holderNear line 523
  20. lemma OAI.CubicTorus.HolderNear.prodMk line 531
  21. lemma OAI.CubicTorus.ContDiffAt.comp_holderNear line 561
  22. def OAI.CubicTorus.HolderJet line 590
  23. lemma OAI.CubicTorus.HolderJet.congr line 598
  24. lemma OAI.CubicTorus.HolderJet.holderNear line 605
  25. lemma OAI.CubicTorus.HolderJet.pred line 610
  26. lemma OAI.CubicTorus.HolderJet.of_le line 615
  27. lemma OAI.CubicTorus.HolderJet.contDiffAt line 623
  28. lemma OAI.CubicTorus.ContDiffAt.holderJet line 633
  29. lemma OAI.CubicTorus.HolderJet.eventually line 654
  30. lemma OAI.CubicTorus.HolderJet.clm_comp line 660
  31. lemma OAI.CubicTorus.HolderJet.prodMk line 670
  32. lemma OAI.CubicTorus.HolderJet.smooth_comp line 682
  33. lemma OAI.CubicTorus.HolderJet.const line 696
  34. lemma OAI.CubicTorus.HolderJet.add line 699
  35. lemma OAI.CubicTorus.HolderJet.sub line 703
  36. lemma OAI.CubicTorus.HolderJet.clm_apply line 707
  37. theorem OAI.CubicTorus.WeakCMCGraph.directional_C1 line 723
  38. lemma OAI.CubicTorus.plane_decompose line 781
  39. theorem OAI.CubicTorus.WeakCMCGraph.local_C2 line 786
  40. lemma OAI.CubicTorus.HolderJet.plane_clm line 830
  41. lemma OAI.CubicTorus.HolderJet.directional line 849
  42. lemma OAI.CubicTorus.HolderJet.of_directionals line 853
  43. lemma OAI.CubicTorus.HolderJet.gradient line 859