OAI/Probability/SLELocalization/WeightedEnergy.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Rectangle Energy estimates.

  1. lemma OAI.SLEExactGauge.RectangleEnergy.integral_mul_square_le line 14
  2. lemma OAI.SLEExactGauge.RectangleEnergy.continuousOn_memLp_two_Ioc line 31
  3. lemma OAI.SLEExactGauge.RectangleEnergy.weighted_interval_energy line 36
  4. def OAI.SLEExactGauge.RectangleEnergy.radialTruncation line 82
  5. lemma OAI.SLEExactGauge.RectangleEnergy.radialTruncation_source line 85
  6. lemma OAI.SLEExactGauge.RectangleEnergy.radialTruncation_bounds line 94
  7. lemma OAI.SLEExactGauge.RectangleEnergy.radialTruncation_continuous line 99
  8. lemma OAI.SLEExactGauge.RectangleEnergy.radialTruncation_zero line 105
  9. lemma OAI.SLEExactGauge.RectangleEnergy.radialTruncation_top line 109
  10. lemma OAI.SLEExactGauge.RectangleEnergy.radialTruncation_middle line 118
  11. lemma OAI.SLEExactGauge.RectangleEnergy.log_normSq_fderiv_le line 128
  12. lemma OAI.SLEExactGauge.RectangleEnergy.radialTruncation_fderiv_bound line 155
  13. lemma OAI.SLEExactGauge.RectangleEnergy.radialTruncation_lipschitz line 190
  14. lemma OAI.SLEExactGauge.RectangleEnergy.radialTruncation_along_C1_AC line 221
  15. lemma OAI.SLEExactGauge.RectangleEnergy.radialTruncation_along_C1_FTC line 227
  16. lemma OAI.SLEExactGauge.RectangleEnergy.radialTruncation_directional_deriv line 233
  17. lemma OAI.SLEExactGauge.RectangleEnergy.acl_interval_energy line 278
  18. lemma OAI.SLEExactGauge.RectangleEnergy.weighted_acl_interval_energy line 289
  19. lemma OAI.SLEExactGauge.RectangleEnergy.lipschitzOn_deriv_memLp line 331
  20. lemma OAI.SLEExactGauge.RectangleEnergy.lipschitzOn_weighted_deriv_memLp line 340
  21. lemma OAI.SLEExactGauge.RectangleEnergy.truncated_curve_weighted_energy line 349
  22. lemma OAI.SLEExactGauge.RectangleEnergy.mean_difference_square_le line 360
  23. lemma OAI.SLEExactGauge.RectangleEnergy.acl_oscillation_energy line 387
  24. lemma OAI.SLEExactGauge.RectangleEnergy.acl_congr line 415
  25. lemma OAI.SLEExactGauge.RectangleEnergy.acl_of_interior line 429
  26. lemma OAI.SLEExactGauge.RectangleEnergy.boundary_zero_energy line 453
  27. lemma OAI.SLEExactGauge.Layer.compact_parameter_derivative line 476
  28. lemma OAI.SLEExactGauge.Layer.rotated_trace line 502
  29. lemma OAI.SLEExactGauge.Layer.laplacian_eq_hessian line 523
  30. lemma OAI.SLEExactGauge.Layer.path_second line 529
  31. def OAI.SLEExactGauge.Layer.circleMean line 537
  32. def OAI.SLEExactGauge.Layer.circleDMean line 540
  33. def OAI.SLEExactGauge.Layer.circleDDMean line 543
  34. lemma OAI.SLEExactGauge.Layer.radial_norm line 547
  35. lemma OAI.SLEExactGauge.Layer.radial_mem line 550
  36. lemma OAI.SLEExactGauge.Layer.radial_continuous line 554
  37. lemma OAI.SLEExactGauge.Layer.radial_interval_maps line 557
  38. lemma OAI.SLEExactGauge.Layer.circle_means_derivatives line 563
  39. lemma OAI.SLEExactGauge.Layer.circle_laplacian_continuous line 611
  40. lemma OAI.SLEExactGauge.Layer.circle_angular_laplacian line 623
  41. lemma OAI.SLEExactGauge.Layer.weighted_circle_derivative line 687
  42. lemma OAI.SLEExactGauge.Layer.compact_parameter_continuousAt line 694
  43. lemma OAI.SLEExactGauge.Layer.laplacian_continuousOn line 714
  44. def OAI.SLEExactGauge.Layer.circleLMean line 725
  45. lemma OAI.SLEExactGauge.Layer.circle_lmean_continuous line 728
  46. lemma OAI.SLEExactGauge.Layer.polar_symm_circle line 754
  47. lemma OAI.SLEExactGauge.Layer.polar_disk_lintegral_le line 759
  48. lemma OAI.SLEExactGauge.RectangleEnergy.polar_annulus_lintegral_le line 810