RibbonPassageScaling.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Positive affine rescaling of the physical one-step passage. A mesh v becomes ell * v; its normalized sausage mass is multiplied by ell ^ dimension κ, exactly as in the width-rescaled ribbon statement.

def OAI.SLEExactGauge.RibbonPassageScaling.affine line 19
Source documentation
Translate and dilate the physical coordinates without changing the curve parameter.
```
def affine (a : ℂ) (ell : ℝ) (z : ℂ) : ℂ := a + (ell : ℂ) * z
```
theorem OAI.SLEExactGauge.RibbonPassageScaling.affine_dist line 21
theorem OAI.SLEExactGauge.RibbonPassageScaling.affine_bijective line 26
theorem OAI.SLEExactGauge.RibbonPassageScaling.affine_volume line 40
Source documentation
Planar area scales by the square of the physical length scale, also for sets for which no measurability has been assumed.
```
theorem affine_volume (a : ℂ) {ell : ℝ} (hell : 0 ≤ ell) (S : Set ℂ) :
    volume (affine a ell '' S) = ENNReal.ofReal (ell ^ 2) * volume S := by
…
```
Mentions: OAI.SLEExactGauge.RibbonPassageScaling.affine
theorem OAI.SLEExactGauge.RibbonPassageScaling.sourceSausageSet_affine line 50
Source documentation
The full sausage, including its intersection with a physical middle strip, scales exactly under a positive affine map.
```
theorem sourceSausageSet_affine
    (a : ℂ) {ell : ℝ} (hell : 0 < ell) (γ : ℝ≥0 → ℂ) (s t : ℝ≥0) (v : ℝ) :
    sourceSausageSet (fun u => affine a ell (γ u)) s t (ell * v) =
      affine a ell '' sourceSausageSet γ s t v := by
…
```
Mentions: OAI.SLEExactGauge.sourceSausageSet, OAI.SLEExactGauge.RibbonPassageScaling.affine
theorem OAI.SLEExactGauge.RibbonPassageScaling.segmentSausageCharge_affine line 65

theorem OAI.SLEExactGauge.RibbonPassageScaling.affine_mass_threshold_iff line 88

Source documentation

The prescribed mass threshold scales by ell^d.

theorem affine_mass_threshold_iff
    (κ : ℝ) (a : ℂ) {ell : ℝ} (hell : 0 < ell)
    (γ : ℝ≥0 → ℂ) (s t : ℝ≥0) {v : ℝ} (hv : 0 < v) (R : Set ℂ) (c : ℝ) :
    ENNReal.ofReal (c * ell ^ dimension κ) ≤
        segmentSausageCharge κ (fun u => affine a ell (γ u)) s t (ell * v)
          (affine a ell '' R) ↔
      ENNReal.ofReal c ≤ segmentSausageCharge κ γ s t v R := by
…

Mentions: OAI.SLEExactGauge.dimension, OAI.SLEExactGauge.segmentSausageCharge, OAI.SLEExactGauge.RibbonPassageScaling.affine

theorem OAI.SLEExactGauge.RibbonPassageScaling.firstFrontTime_affine line 102
Source documentation
Pulling back the longitudinal coordinate leaves the actual first-front clock unchanged. Spatial rescaling does not change curve order.
```
theorem firstFrontTime_affine
    (a : ℂ) (ell : ℝ) (γ : ℝ≥0 → ℂ) (p p' : ℂ → ℝ)
    (hp : ∀ z, p' (affine a ell z) = p z) :
    firstFrontTime (fun t => p' (affine a ell (γ t))) 1 =
      firstFrontTime (fun t => p (γ t)) 1 := by
…
```
Mentions: OAI.SLEExactGauge.RibbonPassageScaling.affine

theorem OAI.SLEExactGauge.RibbonPassageScaling.frontSuccess_affine_iff line 113

Source documentation

Affine scaling preserves all actual front-success conditions, including whole-prefix containment and the terminal offset.

theorem frontSuccess_affine_iff
    {Ω : Type*} (η : ℕ → Ω → ℝ≥0 → ℂ) (p p' : ℕ → ℂ → ℝ)
    (σ : Ω → ℝ≥0) (V : ℕ → Set ℂ) (b : ℕ → ℂ) (ε : ℝ)
    (a : ℂ) {ell : ℝ} (hell : 0 < ell) (n : ℕ)
    (hp : ∀ z, p' n (affine a ell z) = p n z) :
    FrontSuccess (fun j ω t => affine a ell (η j ω t)) p' σ
        (fun j => affine a ell '' V j) (fun j => affine a ell (b j)) (ell * ε) n =
      FrontSuccess η p σ V b ε n := by
…

Mentions: OAI.SLEExactGauge.RibbonPassageScaling.affine

theorem OAI.SLEExactGauge.RibbonPassageScaling.frontSuccess_mass_probability_affine line 142

Source documentation

The complete one-step event has the same probability after simultaneous spatial, mesh and mass rescaling. This is a deterministic event identity; the trace law need not itself have been scaled.

theorem frontSuccess_mass_probability_affine
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (η : ℕ → Ω → ℝ≥0 → ℂ) (p p' : ℕ → ℂ → ℝ)
    (σ : Ω → ℝ≥0) (V : ℕ → Set ℂ) (b : ℕ → ℂ) (ε : ℝ)
    (a : ℂ) {ell : ℝ} (hell : 0 < ell) (n : ℕ)
    (hp : ∀ z, p' n (affine a ell z) = p n z)
    (κ : ℝ) (R : Set ℂ) {v : ℝ} (hv : 0 < v) (c : ℝ) :
    P {ω | ω ∈ FrontSuccess (fun j ω t => affine a ell (η j ω t)) p' σ
          (fun j => affine a ell '' V j) (fun j => affine a ell (b j)) (ell * ε) n ∧
        ENNReal.ofReal (c * ell ^ dimension κ) ≤
          segmentSausageCharge κ (fun t => affine a ell (η n ω t)) (σ ω)
            (frontTime (fun t => p' n (affine a ell (η n ω t))) 1)
…

Mentions: OAI.SLEExactGauge.RibbonPassageScaling.affine, OAI.SLEExactGauge.dimension, OAI.SLEExactGauge.segmentSausageCharge