OAI/Probability/InvariantIsing/Haar/HaarLogBarrier.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The pointwise minimum inequality for a logarithmic heat-gradient barrier.

  1. def OAI.InvariantIsing.haarLogBarrier line 11
  2. lemma OAI.InvariantIsing.haarLogBarrier_eval line 14
  3. lemma OAI.InvariantIsing.haarLogBarrier_laplacian line 20
  4. lemma OAI.InvariantIsing.haarLogBarrier_gamma line 30
  5. lemma OAI.InvariantIsing.haarLogBarrier_min_derivative_lower line 39