ArcNullImage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

From simple-arc payment to null trace images

Distinct points of a connected open subset of a locally connected metric continuum can be joined there by a simple arc. The arc-existence hypothesis is the local arcwise-connectedness theorem used by Lorimer (1981), Locally compact Hjelmslev planes and rings, proof of Lemma 3.2, pp. 1002–1003, displayed (*), DOI 10.4153/CJM-1981-077-5. The null-image criterion derives the measure-theoretic conclusion from this topological hypothesis and the simple-arc payment inequality.

def OAI.CircleDomainRigidity.HasSimpleArcsInConnectedOpens line 22

theorem OAI.CircleDomainRigidity.null_image_of_simple_arc_payment line 30

Source documentation

The null-image criterion with the actual simple-arc payment premise. The input only supplies arcs; no oscillation or null-image conclusion is included in it.

theorem null_image_of_simple_arc_payment
    {X : Type*} [MetricSpace X] [SecondCountableTopology X] [LocallyConnectedSpace X]
    [MeasurableSpace X] [BorelSpace X] {μ : Measure X} [IsFiniteMeasure μ]
    [μ.OuterRegular] (harcs : HasSimpleArcsInConnectedOpens X)
    {F V : Set X} (hV : IsOpen V) (hF : μ (F ∩ V) = 0)
    (v : X → ℝ) {A : ℝ} (hA : 0 ≤ A)
    (hpay : ∀ x ∈ F ∩ V, ∀ y ∈ F ∩ V,
      ∀ γ : Path x y, Function.Injective γ → range γ ⊆ V →
        |v x - v y| ≤ A * μ.real (range γ)) :
    volume (v '' (F ∩ V)) = 0 := by
…

Mentions: OAI.CircleDomainRigidity.HasSimpleArcsInConnectedOpens