OAI/Probability/SKSupport/Foundations/InvSqrtNegHalf.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.Smoothing.inv_sqrt_eq_neg_half line 21
  2. lemma OAI.ZeroTemperatureSK.Smoothing.intervalIntegrable_inv_sqrt line 25
  3. lemma OAI.ZeroTemperatureSK.Smoothing.integral_inv_sqrt line 32
  4. lemma OAI.ZeroTemperatureSK.Smoothing.intervalIntegrable_inv_sqrt_sub line 44
  5. lemma OAI.ZeroTemperatureSK.Smoothing.intervalIntegrable_inv_sqrt_sub' line 49
  6. lemma OAI.ZeroTemperatureSK.Smoothing.integral_inv_sqrt_sub line 54
  7. lemma OAI.ZeroTemperatureSK.Smoothing.integral_inv_sqrt_sub' line 58
  8. lemma OAI.ZeroTemperatureSK.Smoothing.sqrt_kernel_bound line 62
  9. lemma OAI.ZeroTemperatureSK.Smoothing.intervalIntegrable_sqrt_kernel line 82
  10. lemma OAI.ZeroTemperatureSK.Smoothing.integral_sqrt_kernel_le line 94
  11. def OAI.ZeroTemperatureSK.Smoothing.weightedValues line 111
  12. def OAI.ZeroTemperatureSK.Smoothing.weightedSize line 114
  13. lemma OAI.ZeroTemperatureSK.Smoothing.weightedValues_nonempty line 116
  14. lemma OAI.ZeroTemperatureSK.Smoothing.weightedValues_bddAbove line 121
  15. lemma OAI.ZeroTemperatureSK.Smoothing.weighted_le_size line 128
  16. lemma OAI.ZeroTemperatureSK.Smoothing.weightedSize_nonneg line 133
  17. lemma OAI.ZeroTemperatureSK.Smoothing.abs_le_weightedSize line 138
  18. lemma OAI.ZeroTemperatureSK.Smoothing.weightedSize_le line 144
  19. lemma OAI.ZeroTemperatureSK.Smoothing.weighted_absorption line 151