Staircase.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Smooth periodic staircases

An explicit degree-one smooth staircase with spacing h and transition half-width δ. The transition in the cell [nh,(n+1)h] is centered at (n+1/2)h. The floor jumps cancel because the transition is flat near the cell endpoints.

def OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase line 27
Source documentation
A smooth staircase with transitions near the half-shifted h lattice.
```
def smoothStaircase (h δ x : ℝ) : ℝ :=
…
```
theorem OAI.CircleDomainRigidity.FiniteTransfer.cell_lower line 31
theorem OAI.CircleDomainRigidity.FiniteTransfer.cell_upper line 36
theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase_lower line 41
theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase_upper line 47
theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase_add_period line 54
Source documentation
The staircase is a degree-one lift with period increment h.
```
theorem smoothStaircase_add_period {h : ℝ} (hh : 0 < h) (δ x : ℝ) :
    smoothStaircase h δ (x + h) = smoothStaircase h δ x + h := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase
theorem OAI.CircleDomainRigidity.FiniteTransfer.abs_smoothStaircase_sub_le line 64
Source documentation
Uniform displacement is bounded by one grid spacing.
```
theorem abs_smoothStaircase_sub_le {h : ℝ} (hh : 0 < h) (δ x : ℝ) :
    |smoothStaircase h δ x - x| ≤ h := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase
theorem OAI.CircleDomainRigidity.FiniteTransfer.monotone_smoothStaircase line 74
Source documentation
Positive transition width gives a monotone staircase.
```
theorem monotone_smoothStaircase {h δ : ℝ} (hh : 0 < h) (hδ : 0 < δ) :
    Monotone (smoothStaircase h δ) := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase
theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase_eq_near_lattice line 92
Source documentation
Around a cell boundary the floor jump cancels the completed transition, so the staircase is identically the lattice value.
```
private theorem smoothStaircase_eq_near_lattice {h δ x : ℝ}
    (hh : 0 < h) (hδ : 0 < δ) (hδh : δ < h / 4) (n : ℤ)
    (hl : h * n - h / 4 < x) (hu : x < h * n + h / 4) :
    smoothStaircase h δ x = h * n := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase
theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase_eventually_eq_lattice line 120
theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase_eventually_eq_cell line 127
theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiff_smoothStaircase line 143
Source documentation
The apparent jumps of the floor formula cancel; the staircase is smooth at lattice points as well as inside every cell.
```
theorem contDiff_smoothStaircase {h δ : ℝ}
    (hh : 0 < h) (hδ : 0 < δ) (hδh : δ < h / 4) :
    ContDiff ℝ ∞ (smoothStaircase h δ) := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase
theorem OAI.CircleDomainRigidity.FiniteTransfer.transition_hasDerivAt_zero_of_nonpos line 160
theorem OAI.CircleDomainRigidity.FiniteTransfer.transition_hasDerivAt_zero_of_one_le line 170
theorem OAI.CircleDomainRigidity.FiniteTransfer.deriv_smoothStaircase_nonneg line 181
Source documentation
The derivative of the monotone lift is everywhere nonnegative.
```
theorem deriv_smoothStaircase_nonneg {h δ : ℝ} (hh : 0 < h) (hδ : 0 < δ) (x : ℝ) :
    0 ≤ deriv (smoothStaircase h δ) x :=
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase
theorem OAI.CircleDomainRigidity.FiniteTransfer.deriv_smoothStaircase_eq_zero line 187
Source documentation
The derivative is supported in the open δ-bands about the half-shifted lattice. The assertion includes the endpoints of each band.
```
theorem deriv_smoothStaircase_eq_zero {h δ x : ℝ}
    (hh : 0 < h) (hδ : 0 < δ) (hδh : δ < h / 4)
    (hfar : ∀ n : ℤ, δ ≤ |x - h * ((n : ℝ) + 1 / 2)|) :
    deriv (smoothStaircase h δ) x = 0 := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase