OAI/Probability/SLE/Geometry/NormalizedMarkedState.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual marked point in a unit-modulus restarted chart. Its physical scale is exactly the original conformal radius, including the inverse-map derivative factor used in the dense experiment.

  1. def OAI.SLEExactGauge.unitMarkedState line 16
  2. lemma OAI.SLEExactGauge.unitMarkedState_norm line 18
  3. lemma OAI.SLEExactGauge.unitMarkedState_im line 22
  4. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.inverse_derivative_identity line 25
  5. lemma OAI.SLEExactGauge.normalizedInverse_derivative line 39
  6. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.normalized_marked_state line 50

    Source documentation

    All hypotheses of the uniform conformal dense experiment are supplied by the actual live marked state and its normalized inverse chart.

    theorem IsCapacityTwoWitness.normalized_marked_state
    {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness U γ G F) (hU : Continuous U)
    (T : ℝ≥0) (z : ℂ) (hz : z ∈ survivingDomain γ T) :
    let q := G T z - (U T : ℂ)
…

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.survivingDomain