CondensingIteration.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

The closed-convex image iteration

Starting from a closed convex invariant set C, the actual successor set is the closure of the convex hull of its image under g. All boundedness claims come from containment in C. No boundedness-preservation property of an arbitrary continuous map is used.

def OAI.Tingley.condensingStep line 27
Source documentation
The literal closed-convex image operator used in the condensing argument.
```
def condensingStep (g : E → E) (H : Set E) : Set E :=
…
```
def OAI.Tingley.condensingSequence line 31
Source documentation
The iteration begins at C and takes actual closed-convex images.
```
def condensingSequence (C : Set E) (g : E → E) : ℕ → Set E
  | 0 => C
  | n + 1 => condensingStep g (condensingSequence C g n)
```
Mentions: OAI.Tingley.condensingStep
theorem OAI.Tingley.condensingSequence_zero line 35
theorem OAI.Tingley.condensingSequence_succ line 38
theorem OAI.Tingley.condensingStep_mono line 41
theorem OAI.Tingley.image_subset_condensingStep line 45
theorem OAI.Tingley.condensingStep_subset line 49
theorem OAI.Tingley.condensingSequence_succ_subset line 57
theorem OAI.Tingley.condensingSequence_antitone line 64
theorem OAI.Tingley.condensingSequence_subset line 69
theorem OAI.Tingley.condensingSequence_image_subset_succ line 75
Source documentation
Every image point belongs to the next set, before using antitonicity.
```
theorem condensingSequence_image_subset_succ (C : Set E) (g : E → E) (n : ℕ) :
    g '' condensingSequence C g n ⊆ condensingSequence C g (n + 1) :=
…
```
Mentions: OAI.Tingley.condensingSequence
theorem OAI.Tingley.condensingSequence_nonempty line 79
theorem OAI.Tingley.condensingSequence_isClosed line 87
theorem OAI.Tingley.condensingSequence_convex line 93
theorem OAI.Tingley.condensingSequence_isBounded line 99
theorem OAI.Tingley.condensingSequence_mapsTo line 105
theorem OAI.Tingley.condensingSequence_image_subset line 112
theorem OAI.Tingley.condensingSequence_image_isBounded line 118

theorem OAI.Tingley.condensingSequence_chi_succ_eq line 125

Source documentation

The hull step leaves the actual Kuratowski measure of its bounded image unchanged.

theorem condensingSequence_chi_succ_eq {C : Set E} {g : E → E}
    (hclosed : IsClosed C) (hconv : Convex ℝ C) (hmap : MapsTo g C C)
    (hbounded : Bornology.IsBounded C) (n : ℕ) :
    chi (condensingSequence C g (n + 1)) = chi (g '' condensingSequence C g n) := by
…

Mentions: OAI.Tingley.chi, OAI.Tingley.condensingSequence

theorem OAI.Tingley.condensingSequence_chi_succ_le line 132

theorem OAI.Tingley.condensingSequence_chi_le line 141

Source documentation

Geometric decay allows γ = 0; no division by the contraction factor occurs.

theorem condensingSequence_chi_le {C : Set E} {g : E → E}
    (hclosed : IsClosed C) (hconv : Convex ℝ C) (hmap : MapsTo g C C)
    (hbounded : Bornology.IsBounded C) {γ : ℝ} (hγ0 : 0 ≤ γ)
    (hχ : ∀ H : Set E, H ⊆ C → chi (g '' H) ≤ γ * chi H) (n : ℕ) :
    chi (condensingSequence C g n) ≤ γ ^ n * chi C := by
…

Mentions: OAI.Tingley.chi, OAI.Tingley.condensingSequence

theorem OAI.Tingley.condensingSequence_chi_nonneg line 155

theorem OAI.Tingley.condensingSequence_chi_tendsto_zero line 162

Source documentation

The actual sequence has Kuratowski measure tending to zero for 0 ≤ γ < 1.

theorem condensingSequence_chi_tendsto_zero {C : Set E} {g : E → E}
    (hclosed : IsClosed C) (hconv : Convex ℝ C) (hmap : MapsTo g C C)
    (hbounded : Bornology.IsBounded C) {γ : ℝ} (hγ0 : 0 ≤ γ) (hγ1 : γ < 1)
    (hχ : ∀ H : Set E, H ⊆ C → chi (g '' H) ≤ γ * chi H) :
    Tendsto (fun n => chi (condensingSequence C g n)) atTop (𝓝 0) := by
…

Mentions: OAI.Tingley.chi, OAI.Tingley.condensingSequence