OAI/Probability/SLELocalization/SlitMaps.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Slit Maps estimates.

  1. def OAI.SLEExactGauge.SlitMaps.liftMap line 20
  2. lemma OAI.SLEExactGauge.SlitMaps.liftMap_apply line 24
  3. lemma OAI.SLEExactGauge.SlitMaps.tendsto_liftMap line 27
  4. def OAI.SLEExactGauge.SlitMaps.boundedHolomorphic line 48
  5. lemma OAI.SLEExactGauge.SlitMaps.boundedHolomorphic_equicontinuous line 51
  6. lemma OAI.SLEExactGauge.SlitMaps.boundedHolomorphic_closed line 95
  7. lemma OAI.SLEExactGauge.SlitMaps.boundedHolomorphic_compact line 112
  8. lemma OAI.SLEExactGauge.SlitMaps.lower_norm_of_sphere line 143
  9. theorem OAI.SLEExactGauge.SlitMaps.locallyUniform_nonvanishing line 162
  10. lemma OAI.SLEExactGauge.SlitMaps.locallyUniform_deriv_nonvanishing line 220
  11. lemma OAI.SLEExactGauge.SlitMaps.locallyUniform_injective line 232
  12. def OAI.SLEExactGauge.SlitMaps.markedEmbeddings line 264
  13. lemma OAI.SLEExactGauge.SlitMaps.derivative_continuousOn line 268
  14. lemma OAI.SLEExactGauge.SlitMaps.markedEmbeddings_closed line 279
  15. lemma OAI.SLEExactGauge.SlitMaps.markedEmbeddings_compact line 301
  16. theorem OAI.SLEExactGauge.SlitMaps.exists_injective_not_dense_image_deriv_ne_zero line 329
  17. lemma OAI.SLEExactGauge.SlitMaps.exists_mapsTo_unitBall_injOn_deriv_ne_zero line 386
  18. def OAI.SLEExactGauge.SlitMaps.IsDiskEmbedding line 425
  19. lemma OAI.SLEExactGauge.SlitMaps.IsDiskEmbedding.differentiableOn line 428
  20. lemma OAI.SLEExactGauge.SlitMaps.exists_diskEmbedding line 432
  21. def OAI.SLEExactGauge.SlitMaps.continuousRestriction line 447
  22. lemma OAI.SLEExactGauge.SlitMaps.continuousRestriction_apply line 450
  23. lemma OAI.SLEExactGauge.SlitMaps.lift_restriction_eqOn line 453
  24. lemma OAI.SLEExactGauge.SlitMaps.deriv_lift_restriction line 458
  25. lemma OAI.SLEExactGauge.SlitMaps.IsDiskEmbedding.restriction_mem line 465
  26. lemma OAI.SLEExactGauge.SlitMaps.markedEmbeddings_isDiskEmbedding line 479
  27. theorem OAI.SLEExactGauge.SlitMaps.exists_extremal_diskEmbedding line 496
  28. lemma OAI.SLEExactGauge.SlitMaps.diskAuto_comp_deriv line 516
  29. lemma OAI.SLEExactGauge.SlitMaps.square_root_boost_real line 521
  30. theorem OAI.SLEExactGauge.SlitMaps.exists_diskEmbedding_improved line 532
  31. theorem OAI.SLEExactGauge.SlitMaps.exists_biholomorphic_unitDisk line 621