CutoffStaircase.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Joining a coordinate to a staircase outside a core

These are the differential and periodicity calculations for the actual cutoff modification u + χ (P ∘ u - u) in finite transfer. They apply to ordinary real branches and hence also to compatible periodic branches.

def OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase line 19

theorem OAI.CircleDomainRigidity.FiniteTransfer.hasFDerivAt_cutoffStaircase line 24

Source documentation

The modified differential has the original gradient multiplier and one error term supported on the cutoff transition.

theorem hasFDerivAt_cutoffStaircase {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {u χ : E → ℝ} {P : ℝ → ℝ} {x : E} {du dχ : E →L[ℝ] ℝ} {p : ℝ}
    (hu : HasFDerivAt u du x) (hχ : HasFDerivAt χ dχ x) (hP : HasDerivAt P p (u x)) :
    HasFDerivAt (cutoffStaircase u χ P)
      ((1 - χ x + χ x * p) • du + (P (u x) - u x) • dχ) x := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase

theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiff_cutoffStaircase line 38

Source documentation

Smooth input coordinates, staircase and cutoff give a smooth modification.

theorem contDiff_cutoffStaircase {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {n : ℕ∞} {u χ : E → ℝ} {P : ℝ → ℝ}
    (hu : ContDiff ℝ n u) (hχ : ContDiff ℝ n χ) (hP : ContDiff ℝ n P) :
    ContDiff ℝ n (cutoffStaircase u χ P) :=
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase

theorem OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase_of_zero line 45
Source documentation
The original coordinate is retained exactly where the cutoff is zero.
```
theorem cutoffStaircase_of_zero {X : Type*} {u χ : X → ℝ} {P : ℝ → ℝ} {x : X}
    (hχ : χ x = 0) : cutoffStaircase u χ P x = u x := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase
theorem OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase_of_one line 50
Source documentation
The staircase is used exactly where the cutoff is one.
```
theorem cutoffStaircase_of_one {X : Type*} {u χ : X → ℝ} {P : ℝ → ℝ} {x : X}
    (hχ : χ x = 1) : cutoffStaircase u χ P x = P (u x) := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase
theorem OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase_period line 56
Source documentation
A staircase with unit additive period preserves the coordinate's additive deck-transformation law under an invariant cutoff.
```
theorem cutoffStaircase_period {X : Type*} {u χ : X → ℝ} {P : ℝ → ℝ}
    (T : X → X) (hu : ∀ x, u (T x) = u x + 1) (hχ : ∀ x, χ (T x) = χ x)
    (hP : ∀ t, P (t + 1) = P t + 1) (x : X) :
    cutoffStaircase u χ P (T x) = cutoffStaircase u χ P x + 1 := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase

theorem OAI.CircleDomainRigidity.FiniteTransfer.abs_cutoffStaircase_sub_le line 64

Source documentation

The cutoff does not enlarge the staircase's uniform displacement.

theorem abs_cutoffStaircase_sub_le {X : Type*} {u χ : X → ℝ} {P : ℝ → ℝ}
    {x : X} {h : ℝ} (hχ0 : 0 ≤ χ x) (hχ1 : χ x ≤ 1)
    (hP : |P (u x) - u x| ≤ h) :
    |cutoffStaircase u χ P x - u x| ≤ h := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase

theorem OAI.CircleDomainRigidity.FiniteTransfer.cutoff_multiplier_nonneg line 77
Source documentation
The leading differential multiplier is nonnegative for a monotone staircase and a cutoff taking values in [0,1].
```
theorem cutoff_multiplier_nonneg {P : ℝ → ℝ} (hP : Monotone P)
    {χ x : ℝ} (hχ0 : 0 ≤ χ) (hχ1 : χ ≤ 1) :
    0 ≤ 1 - χ + χ * deriv P x :=
…
```