OAI/Probability/SLE/Gauge/RibbonMiddleMass.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual source middle strips of an embedded ribbon are disjoint, measurable spatial regions. Their stopped passage masses can therefore be charged to one whole-trace sausage at the common prescribed mesh.

  1. def OAI.SLEExactGauge.RibbonCoordinates.middleStrip line 18
  2. theorem OAI.SLEExactGauge.RibbonCoordinates.middleStrip_open line 21
  3. theorem OAI.SLEExactGauge.RibbonCoordinates.middleStrip_subset_closedRibbon line 26
  4. theorem OAI.SLEExactGauge.RibbonCoordinates.physicalMiddleRegion_eq_image_middleStrip line 31
  5. theorem OAI.SLEExactGauge.RibbonCoordinates.middleStrip_pairwise_disjoint line 40
  6. theorem OAI.SLEExactGauge.RibbonCoordinates.physical_middle_regions_pairwise_disjoint line 55
  7. theorem OAI.SLEExactGauge.RibbonCoordinates.isOpen_embedded_middle_region line 68
  8. theorem OAI.SLEExactGauge.RibbonCoordinates.segmentSausageCharge_le_whole line 82
  9. theorem OAI.SLEExactGauge.RibbonCoordinates.whole_sausage_charge_from_ribbon_steps line 92

    Source documentation

    Exactly the source middle strips are counted, even if their sausages also meet other parts of the curve. Spatial disjointness alone suffices.

    theorem whole_sausage_charge_from_ribbon_steps
    (hpublished : PublishedPlanarDiskOpenness)
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon) (hiP : InjOn P closedRibbon)
    {ε : ℝ} (hε : ε ≤ 1) (I : Finset ℕ)
    (κ : ℝ) (γ : ℝ≥0 → ℂ) (s t : ℕ → ℝ≥0) (v b : ℝ) (A : Set ℂ)
    (hregions : ∀ i ∈ I, physicalMiddleRegion P closedRibbon i ε ⊆ A)
    (hmass : ∀ i ∈ I, ENNReal.ofReal b ≤
      segmentSausageCharge κ γ (s i) (t i) v (physicalMiddleRegion P closedRibbon i ε)) :
    (I.card : ℝ≥0∞) * ENNReal.ofReal b ≤ wholeSausageCharge κ γ v A := by
…

    Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.RibbonCoordinates.closedRibbon, OAI.SLEExactGauge.RibbonCoordinates.physicalMiddleRegion, OAI.SLEExactGauge.segmentSausageCharge, OAI.SLEExactGauge.wholeSausageCharge

  10. theorem OAI.SLEExactGauge.RibbonCoordinates.dense_ribbon_mass_from_steps line 121