OAI/Probability/SLELocalization/IntegratedMeshSimple.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Integrated Mesh Simple estimates.

  1. lemma OAI.SLEExactGauge.layer_set_measurable line 16
  2. theorem OAI.SLEExactGauge.conformalRadiusLayer line 35
  3. lemma OAI.SLEExactGauge.Layer.DiskPair.radius_le_omitted line 102
  4. lemma OAI.SLEExactGauge.Layer.DiskPair.radius_le_infDist line 124
  5. lemma OAI.SLEExactGauge.Layer.complexJacobian line 134
  6. theorem OAI.SLEExactGauge.Layer.physical_boundary_layer line 139
  7. def OAI.SLEExactGauge.Mesh.halfPlaneGreen line 185
  8. lemma OAI.SLEExactGauge.Mesh.hasDerivAt_log_norm line 187
  9. lemma OAI.SLEExactGauge.Mesh.green_eq_difference line 197
  10. lemma OAI.SLEExactGauge.Mesh.difference_velocity line 202
  11. lemma OAI.SLEExactGauge.Mesh.green_velocity line 207
  12. theorem OAI.SLEExactGauge.Mesh.green_decrease line 223
  13. def OAI.SLEExactGauge.Layer.halfToDisk line 282
  14. def OAI.SLEExactGauge.Layer.diskToHalf line 284
  15. lemma OAI.SLEExactGauge.Layer.half_den_ne line 286
  16. lemma OAI.SLEExactGauge.Layer.disk_den_ne line 293
  17. lemma OAI.SLEExactGauge.Layer.halfToDisk_maps line 298
  18. lemma OAI.SLEExactGauge.Layer.diskToHalf_im line 308
  19. lemma OAI.SLEExactGauge.Layer.diskToHalf_maps line 315
  20. lemma OAI.SLEExactGauge.Layer.disk_half_inverse line 321
  21. lemma OAI.SLEExactGauge.Layer.half_disk_inverse line 330
  22. lemma OAI.SLEExactGauge.Layer.halfToDisk_differentiable line 339
  23. lemma OAI.SLEExactGauge.Layer.diskToHalf_differentiable line 343
  24. lemma OAI.SLEExactGauge.Layer.green_disk_eq line 348
  25. theorem OAI.SLEExactGauge.Layer.halfPlane_boundary_layer line 356
  26. lemma OAI.SLEExactGauge.Mesh.green_nonneg line 403
  27. lemma OAI.SLEExactGauge.Mesh.green_continuousAt line 417
  28. def OAI.SLEExactGauge.Mesh.poissonFactor line 424
  29. lemma OAI.SLEExactGauge.Mesh.poissonFactor_continuousOn line 427
  30. lemma OAI.SLEExactGauge.Mesh.uniformization_injective line 436
  31. lemma OAI.SLEExactGauge.Mesh.pair_integral line 443
  32. lemma OAI.SLEExactGauge.Mesh.pair_integral_le line 481
  33. theorem OAI.SLEExactGauge.Mesh.loewner_boundary_layer line 490
  34. lemma OAI.SLEExactGauge.PhysicalStop.ofReal_cap_le line 519
  35. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.first_eq_source line 539
  36. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.first_le_poisson line 565
  37. lemma OAI.SLEExactGauge.Mesh.poissonFactor_pos line 605
  38. lemma OAI.SLEExactGauge.Mesh.overlap_lintegral_bound line 616
  39. lemma OAI.SLEExactGauge.Mesh.approached_in_boundary_layer line 660
  40. lemma OAI.SLEExactGauge.Mesh.green_symm line 668
  41. def OAI.SLEExactGauge.Mesh.laterGreen line 676
  42. lemma OAI.SLEExactGauge.Mesh.laterGreen_row line 680
  43. lemma OAI.SLEExactGauge.Mesh.supported_pair_lintegral line 713
  44. lemma OAI.SLEExactGauge.Mesh.asynchronous_pair_bound line 730
  45. lemma OAI.SLEExactGauge.Mesh.norm_integral_sq_le_pairs line 770
  46. lemma OAI.SLEExactGauge.Mesh.bracket_le_pair_integral line 784
  47. lemma OAI.SLEExactGauge.Mesh.symmetric_kernel_integral line 803
  48. theorem OAI.SLEExactGauge.Mesh.asynchronous_bracket_bound line 824
  49. theorem OAI.SLEExactGauge.Mesh.asynchronous_bracket_bound_with_kernel line 859