PrescribedPublishedMain.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The first paper's prescribed moment gauge, from precisely named published inputs. The angular mixing estimate is proved internally.

theorem OAI.SLEExactGauge.RegularSLEPresentation.prescribed_main_of_published_inputs line 20
Source documentation
The exact prescribed gauge gives positive finite mass to every positive-time compact trace segment and finite expected mass of the whole trace in bounded disks. Published inputs: Duren (1983), section 2.3 (the disk univalent-growth estimate), and Rohde--Schramm (2005), Theorem 5.1 (trace generation under the driver law).
```
theorem RegularSLEPresentation.prescribed_main_of_published_inputs
    {Ω : Type} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {κ : ℝ} {γ : Ω → ℝ≥0 → ℂ} (a : RegularSLEPresentation P κ γ)
    (hκ : 0<κ) (hκ8 : κ<8) (hγ : ∀ t, Measurable (fun ω => γ ω t))
    (hgrowth : PublishedDiskUnivalentGrowth)
    (htrace : PublishedTraceGeneration
      ((P.comap (Subtype.val : a.samples → Ω)).map (sourceDriverPath a.B a.continuous_B))
      κ (fun t p => p t))
    (W : Target.WienerLaw) (hW : Target.IsWiener W) :
    MainConclusion P (Target.gauge κ W) γ := by
…
```
Mentions: OAI.SLEExactGauge.RegularSLEPresentation, OAI.SLEExactGauge.PublishedDiskUnivalentGrowth, OAI.SLEExactGauge.PublishedTraceGeneration, OAI.SLEExactGauge.sourceDriverPath, OAI.SLEExactGauge.Target.WienerLaw, OAI.SLEExactGauge.Target.IsWiener, OAI.SLEExactGauge.MainConclusion, OAI.SLEExactGauge.Target.gauge
theorem OAI.SLEExactGauge.ordinary_prescribed_mainConclusion_of_published_inputs line 40
Source documentation
The first paper's full prescribed-gauge Hausdorff conclusion for ordinary chordal SLE, with only the cited published conformal and trace inputs.
```
theorem ordinary_prescribed_mainConclusion_of_published_inputs
    {Ω : Type} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0<κ) (hκ8 : κ<8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (hgrowth : PublishedDiskUnivalentGrowth)
    (htrace : PublishedTraceGeneration (ordinaryRegularDriverLaw hSLE) κ (fun t p => p t))
    (W : Target.WienerLaw) (hW : Target.IsWiener W) :
    MainConclusion P (Target.gauge κ W) γ :=
…
```
Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.PublishedDiskUnivalentGrowth, OAI.SLEExactGauge.PublishedTraceGeneration, OAI.SLEExactGauge.ordinaryRegularDriverLaw, OAI.SLEExactGauge.Target.WienerLaw, OAI.SLEExactGauge.Target.IsWiener, OAI.SLEExactGauge.MainConclusion, OAI.SLEExactGauge.Target.gauge