OAI/Analysis/Steinitz/HeatEnergy.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Survival-energy estimates and simultaneous diagonal separation.

  1. lemma OAI.GaussianKernel.pdf_scale line 14
  2. lemma OAI.GaussianKernel.density_scale line 27
  3. lemma OAI.GaussianKernel.chainWeight_scale line 32
  4. lemma OAI.GaussianKernel.pi_smul line 43
  5. lemma OAI.GaussianKernel.pathMass_scale line 50
  6. lemma OAI.HeatL2.energy_smul line 90
  7. lemma OAI.HeatL2.supported_smul line 99
  8. lemma OAI.HeatL2.form_le_norm line 104
  9. lemma OAI.HeatL2.normalized_energy_lt line 112
  10. lemma OAI.HeatL2.exists_supported_energy_lt line 128
  11. lemma OAI.HeatL2.exists_energy_lt_of_exp_le line 149
  12. lemma OAI.HeatL2.compressed_norm_le_of_energy line 165
  13. lemma OAI.HeatL2.compressed_norm_mono_symbol line 175
  14. lemma OAI.HeatL2.compressed_norm_mono_domain line 191
  15. lemma OAI.HeatL2.compressed_norm_rpow line 203
  16. lemma OAI.HeatL2.heat_form_pos line 230
  17. lemma OAI.HeatL2.compressed_norm_pos_of_supported line 252
  18. lemma OAI.HeatL2.oneLp_norm_sq line 262
  19. lemma OAI.HeatL2.compressed_norm_pos line 272
  20. lemma OAI.EuclideanSteinitz.functional_eq_sum line 297
  21. lemma OAI.EuclideanSteinitz.simultaneous_approx line 308
  22. lemma OAI.HeatL2.mixture_gaussian_energy_le line 418
  23. lemma OAI.HeatL2.mixture_diagonal_energy_le line 438
  24. def OAI.HeatL2.Diagonal.coordSymbol line 458
  25. lemma OAI.HeatL2.Diagonal.coordSymbol_nonneg line 460
  26. lemma OAI.HeatL2.Diagonal.coordSymbol_continuous line 462
  27. lemma OAI.HeatL2.Diagonal.symbol_single line 466
  28. def OAI.HeatL2.Diagonal.Bound line 474
  29. lemma OAI.HeatL2.Diagonal.exists_unit_of_bound line 479
  30. lemma OAI.HeatL2.Diagonal.symbol_mean line 489
  31. lemma OAI.HeatL2.Diagonal.coord_mixture_energy_le line 500
  32. lemma OAI.HeatL2.Diagonal.simultaneous_coordinate_energy line 511
  33. lemma OAI.HeatL2.Diagonal.symbol_mono line 598
  34. lemma OAI.HeatL2.Diagonal.bound_of_positive line 604
  35. lemma OAI.HeatL2.Diagonal.Bound.mono_const line 625
  36. lemma OAI.GaussianAR.scaled_kernel_norm_of_survival line 644
  37. lemma OAI.GaussianAR.decay_sqrt_bound line 679
  38. lemma OAI.GaussianAR.dilated_bound_of_survival line 684