OAI/Analysis/Triangular/Energy/Cutoff.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularUniversal.radialCutoff line 11

    Source documentation

    A comparison density, equal to one on the competitor disk. It adds no spacing or local-count hypothesis to the density-only LP argument.

    def radialCutoff (R T : ℝ) (x : Plane) : ℝ :=
…

    Mentions: OAI.TriangularUniversal.Plane

  2. lemma OAI.TriangularUniversal.radialCutoff_nonneg line 14
  3. lemma OAI.TriangularUniversal.radialCutoff_le_one line 15
  4. lemma OAI.TriangularUniversal.radialCutoff_continuous line 17
  5. lemma OAI.TriangularUniversal.radialCutoff_eq_one line 20
  6. lemma OAI.TriangularUniversal.radialCutoff_eq_zero line 24
  7. lemma OAI.TriangularUniversal.radialCutoff_compactSupport line 29
  8. lemma OAI.TriangularUniversal.radialCutoff_integrable line 37
  9. lemma OAI.TriangularUniversal.clip_lipschitz line 40
  10. lemma OAI.TriangularUniversal.radialCutoff_lipschitz line 44
  11. lemma OAI.TriangularUniversal.radialCutoff_sub_bound line 62
  12. lemma OAI.TriangularUniversal.plane_disk_volume line 68
  13. lemma OAI.TriangularUniversal.radialCutoff_integral_bound line 73
  14. def OAI.TriangularUniversal.cutoffConvolution line 89
  15. def OAI.TriangularUniversal.firstMoment line 92
  16. lemma OAI.TriangularUniversal.cutoffConvolution_integrable line 94
  17. lemma OAI.TriangularUniversal.cutoffConvolution_error line 103
  18. lemma OAI.TriangularUniversal.cutoffConvolution_re_bounds line 133
  19. def OAI.TriangularUniversal.cutoffMeasure line 147
  20. lemma OAI.TriangularUniversal.cutoffMeasure_finite line 150
  21. lemma OAI.TriangularUniversal.integral_cutoffMeasure line 156
  22. lemma OAI.TriangularUniversal.cutoffMeasure_mass line 163
  23. lemma OAI.TriangularUniversal.cutoffConvolution_eq_integral line 170