OAI/Computability/MinUncut/Analysis/SmoothingRho.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.GaussianHermite.project_const_mul line 16
  2. lemma OAI.MinUncut.GaussianHermite.convolutionGradient_memLp line 22
  3. def OAI.MinUncut.GaussianHermite.smoothingRho line 28
  4. lemma OAI.MinUncut.GaussianHermite.smoothingRho_pos line 29
  5. lemma OAI.MinUncut.GaussianHermite.smoothingRho_rotation line 32
  6. lemma OAI.MinUncut.GaussianHermite.smoothingRho_lt_one line 39
  7. lemma OAI.MinUncut.Inner.gradient_as_convolutionGradient line 52
  8. lemma OAI.MinUncut.Inner.gradient_memLp line 61
  9. lemma OAI.MinUncut.Inner.spatialEnergy_sqrt_scale line 68
  10. lemma OAI.MinUncut.Inner.gradient_integral_energy line 74
  11. lemma OAI.MinUncut.Inner.smooth_energy_le_gradient line 87
  12. def OAI.MinUncut.Inner.gaussianProject line 96
  13. lemma OAI.MinUncut.Inner.gaussian_residual_energy line 100
  14. theorem OAI.MinUncut.Inner.exists_gaussian_cutoff line 114