OAI/Probability/SKSupport/Density/DensityHeat.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ZeroTemperatureSK.Heat.heatKernel line 12
2. lemma OAI.ZeroTemperatureSK.Heat.heatKernel_formula line 14
3. lemma OAI.ZeroTemperatureSK.Heat.heatKernel_pos line 18
4. lemma OAI.ZeroTemperatureSK.Heat.varianceHeat_kernel line 21
5. lemma OAI.ZeroTemperatureSK.Heat.heatKernel_complete_square line 31
6. lemma OAI.ZeroTemperatureSK.Heat.varianceHeat_gaussian_weight line 55
7. lemma OAI.ZeroTemperatureSK.Heat.exp_varianceLogHeat_one line 68
8. lemma OAI.ZeroTemperatureSK.Heat.exp_half_log line 73
9. lemma OAI.ZeroTemperatureSK.Heat.varianceHeat_gaussian_forwardCorrection line 79
10. lemma OAI.ZeroTemperatureSK.Heat.heatKernel_uniform_lower line 98
11. lemma OAI.ZeroTemperatureSK.Heat.integrable_weighted_heatKernel line 119
12. lemma OAI.ZeroTemperatureSK.Heat.varianceHeat_exp_eq_exp_log line 135
13. lemma OAI.ZeroTemperatureSK.Heat.varianceTilted_lower_window line 146