OAI/Geometry/CubicTorus/Estimates/BVOneDimensionalHat.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.intervalSmoothHat line 15
  2. lemma OAI.CubicTorus.primitive_contDiff line 18
  3. lemma OAI.CubicTorus.intervalSmoothHat_contDiff line 27
  4. lemma OAI.CubicTorus.intervalSmoothHat_hasDerivAt line 32
  5. lemma OAI.CubicTorus.intervalSmoothHat_eq_integral line 42
  6. lemma OAI.CubicTorus.intervalSmoothHat_nonneg line 49
  7. lemma OAI.CubicTorus.intervalSmoothHat_le_one line 55
  8. lemma OAI.CubicTorus.intervalSmoothHat_support line 62
  9. def OAI.CubicTorus.partitionSmoothTest line 95
  10. lemma OAI.CubicTorus.intervalSmoothHat_sum line 98
  11. lemma OAI.CubicTorus.partitionSmoothTest_contDiff line 105
  12. lemma OAI.CubicTorus.partitionSmoothTest_deriv line 111
  13. lemma OAI.CubicTorus.partitionSmoothTest_bound line 123
  14. lemma OAI.CubicTorus.partitionSmoothTest_support line 139
  15. lemma OAI.CubicTorus.bounded_mul_shift_integrable line 155
  16. lemma OAI.CubicTorus.partitionSmoothTest_flux line 168
  17. lemma OAI.CubicTorus.binary_tendsto_eventually_constant line 201
  18. lemma OAI.CubicTorus.binary_bv_side_constants line 215
  19. lemma OAI.CubicTorus.binary_bv_punctured_continuity line 232
  20. theorem OAI.CubicTorus.binary_bv_finite_discontinuities line 255
  21. lemma OAI.CubicTorus.eVariationOn_le_of_pointwise_tendsto line 266
  22. lemma OAI.CubicTorus.locally_constant_not_mixed_closure line 278
  23. theorem OAI.CubicTorus.binary_bv_finite_mixed_boundary line 291
  24. theorem OAI.CubicTorus.smoothed_variation_of_dual_bound line 330
  25. def OAI.CubicTorus.angularMollifier line 366
  26. lemma OAI.CubicTorus.angularMollifier_radius_tendsto line 372
  27. lemma OAI.CubicTorus.angularMollifier_support line 380
  28. lemma OAI.CubicTorus.angular_smoothing_ae_tendsto line 390
  29. theorem OAI.CubicTorus.boundedVariationOn_good_set_of_dual_bound line 414
  30. theorem OAI.CubicTorus.totallyBounded_moving_blowupCharacteristic line 445
  31. theorem OAI.CubicTorus.isMinimizerAt_moving_blowup_limit line 477
  32. lemma OAI.CubicTorus.integral_closedBall_affine_scaling line 532
  33. lemma OAI.CubicTorus.local_affine_integral_le line 553
  34. lemma OAI.CubicTorus.localL1_affine_tendsto line 568
  35. lemma OAI.CubicTorus.blowupCharacteristic_affine line 582
  36. lemma OAI.CubicTorus.finiteMeasure_real_closed_lower line 599
  37. lemma OAI.CubicTorus.finiteMeasure_real_open_upper line 617
  38. lemma OAI.CubicTorus.blowupNormalMeasure_ball line 634
  39. lemma OAI.CubicTorus.blowupNormalMeasure_ball_tendsto line 656
  40. theorem OAI.CubicTorus.blowup_limit_ball_mass line 673
  41. lemma OAI.CubicTorus.normalBall_measure_of_real line 710
  42. lemma OAI.CubicTorus.norm_sq_lt_iff line 715
  43. theorem OAI.CubicTorus.squaredRadius_distribution line 722
  44. lemma OAI.CubicTorus.smoothTransition_deriv_pos line 792
  45. def OAI.CubicTorus.radialBalance line 810
  46. lemma OAI.CubicTorus.continuous_radialBalance line 813
  47. lemma OAI.CubicTorus.integral_radialBalance line 818
  48. lemma OAI.CubicTorus.radialBalance_zero line 829
  49. lemma OAI.CubicTorus.quadraticMass_radialBalance line 833
  50. lemma OAI.CubicTorus.integrable_radialTangency line 852
  51. lemma OAI.CubicTorus.integrable_radialBalanceNorm line 872
  52. lemma OAI.CubicTorus.tangentialDivergence_radialBalance line 890
  53. theorem OAI.CubicTorus.stationary_quadraticMass_radial_tangent line 897