ReturnMapNoncompactness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The return map contracts noncompactness on every subset

Finite scalar bins refine diameter covers after each piece is intersected with the given subset. A positive-error argument then passes to the exact Kuratowski infimum. Neither the subset nor its covering pieces need be compact.

theorem OAI.Tingley.finiteDiameterCover_image_of_scalar_bins line 21

Source documentation

A finite refinement by two bounded scalar observables.

theorem finiteDiameterCover_image_of_scalar_bins
    {X Y : Type*} [PseudoMetricSpace X] [PseudoMetricSpace Y]
    {C H : Set X} {g : X → Y} {p u : X → ℝ} {U a γ δ η : ℝ}
    (hHC : H ⊆ C) (hU : 0 ≤ U) (ha : 0 < a) (hγ : 0 ≤ γ)
    (hp : ∀ v ∈ C, p v ∈ Set.Icc 0 U)
    (hu : ∀ v ∈ C, u v ∈ Set.Icc 0 U)
    (hpair : ∀ v ∈ C, ∀ v' ∈ C,
      dist (g v) (g v') ≤ γ * dist v v' +
        (2 / a) * (|u v - u v'| + |p v - p v'|))
    (hc : FiniteDiameterCover H δ) (hη : 0 < η) :
    FiniteDiameterCover (g '' H) (γ * δ + 4 * η / a) := by
…

Mentions: OAI.Tingley.FiniteDiameterCover

theorem OAI.Tingley.chi_return_image_le line 60

Source documentation

The exact all-subsets contraction, including the empty subset. The scalar relations and the two-point estimate are supplied by the actual return map.

theorem chi_return_image_le
    {X : Type*} [PseudoMetricSpace X]
    {C : Set X} {g : X → X} {p s u r : X → ℝ} {t M : ℝ}
    (ht0 : 0 < t) (ht1 : t < 1) (hM : 0 < M)
    (hCne : C.Nonempty) (hCb : Bornology.IsBounded C)
    (_hgC : Set.MapsTo g C C)
    (hbounds : ∀ v ∈ C,
      (1 - t ≤ p v ∧ p v ≤ 1 + t) ∧
      (1 - t ≤ s v ∧ s v ≤ 1 + t) ∧
      (1 - t ≤ u v ∧ u v ≤ 1 + t) ∧
      (1 - t ≤ r v ∧ r v ≤ 1 + t))
    (hs : ∀ v ∈ C, s v = p v + M)
…