ShrinkingProfileDomains.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The contracted profile domains exhaust the interior cell

theorem OAI.PolycyclicRecognition.eventually_mem_shrinking_cell line 15

Source documentation

Inverse dilation of a fixed interior point remains in the cell when its scalar tends to one. No boundary regularity is required.

theorem eventually_mem_shrinking_cell
    {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    {cell : Set W} {w : W} (hw : w ∈ interior cell)
    {δ : ℕ → ℝ} (hδ : Tendsto δ atTop (𝓝 0)) (c : ℝ) :
    ∀ᶠ j in atTop, w ∈ (fun v => (1 - c * δ j) • v) '' cell := by
…

theorem OAI.PolycyclicRecognition.eventually_affine_of_shrinking_cells line 32

Source documentation

Affine identities on contracted cells therefore give the eventual interior identities used by the boundary and Haar diagonal arguments.

theorem eventually_affine_of_shrinking_cells
    {V W Y : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    [Add Y] (q : V → W) (cell : Set W) (f : ℕ → V → Y)
    (A : W → Y) (b : ℕ → Y) {δ : ℕ → ℝ}
    (hδ : Tendsto δ atTop (𝓝 0)) (c : ℝ)
    (haff : ∀ j z, q z ∈ (fun w => (1 - c * δ j) • w) '' cell →
      f j z = A (q z) + b j) :
    ∀ z, q z ∈ interior cell → ∀ᶠ j in atTop, f j z = A (q z) + b j := by
…

theorem OAI.PolycyclicRecognition.eventually_affine_of_shrinking_interiors line 45

Source documentation

The same exhaustion holds when each row is known affine only on the open contracted cell, as in the local affinity theorem.

theorem eventually_affine_of_shrinking_interiors
    {V W Y : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    [Add Y] (q : V → W) (cell : Set W) (f : ℕ → V → Y)
    (A : W → Y) (b : ℕ → Y) {δ : ℕ → ℝ}
    (hδ : Tendsto δ atTop (𝓝 0)) (c : ℝ)
    (haff : ∀ j z, q z ∈ (fun w => (1 - c * δ j) • w) '' interior cell →
      f j z = A (q z) + b j) :
    ∀ z, q z ∈ interior cell → ∀ᶠ j in atTop, f j z = A (q z) + b j := by
…