ShiftedStaircase.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The randomly shifted smooth staircase family

Translating the explicit staircase places its transition bands at θ + hℤ. The resulting family has the exact derivative mean required for uniform random shifts, and retains the displacement and period properties needed for periodic coordinate branches.

def OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase line 23
Source documentation
The smooth staircase whose transition centers form θ + hℤ.
```
def shiftedStaircase (h δ θ x : ℝ) : ℝ :=
…
```
theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiff_shiftedStaircase line 26
theorem OAI.CircleDomainRigidity.FiniteTransfer.monotone_shiftedStaircase line 34
theorem OAI.CircleDomainRigidity.FiniteTransfer.abs_shiftedStaircase_sub_le line 41
theorem OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase_add_period line 50
theorem OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase_add_nat_mul_period line 56
theorem OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase_add_one line 68
Source documentation
Choosing reciprocal-integer spacing preserves additive period one.
```
theorem shiftedStaircase_add_one {N : ℕ} (hN : 0 < N) (δ θ x : ℝ) :
    shiftedStaircase (1 / (N : ℝ)) δ θ (x + 1) =
      shiftedStaircase (1 / (N : ℝ)) δ θ x + 1 := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase
theorem OAI.CircleDomainRigidity.FiniteTransfer.deriv_shiftedStaircase line 77
Source documentation
Translation does not change the derivative multiplier.
```
theorem deriv_shiftedStaircase {h δ : ℝ}
    (hh : 0 < h) (hδ : 0 < δ) (hδh : δ < h / 4) (θ x : ℝ) :
    deriv (shiftedStaircase h δ θ) x =
      deriv (smoothStaircase h δ) ((x + h / 2) - θ) := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase, OAI.CircleDomainRigidity.FiniteTransfer.smoothStaircase
theorem OAI.CircleDomainRigidity.FiniteTransfer.deriv_shiftedStaircase_nonneg line 88
theorem OAI.CircleDomainRigidity.FiniteTransfer.deriv_shiftedStaircase_eq_zero line 95
Source documentation
Only the open δ-neighborhoods of the shifted lattice can support nonzero derivative, with zero derivative also at their endpoints.
```
theorem deriv_shiftedStaircase_eq_zero {h δ θ x : ℝ}
    (hh : 0 < h) (hδ : 0 < δ) (hδh : δ < h / 4)
    (hfar : ∀ n : ℤ, δ ≤ |x - (θ + h * n)|) :
    deriv (shiftedStaircase h δ θ) x = 0 := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase
theorem OAI.CircleDomainRigidity.FiniteTransfer.continuous_shiftedStaircase_deriv line 106
theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_shiftedStaircase_deriv line 116
Source documentation
Actual uniform shifts of the constructed staircase have derivative integral exactly h.
```
theorem integral_shiftedStaircase_deriv {h δ : ℝ}
    (hh : 0 < h) (hδ : 0 < δ) (hδh : δ < h / 4) (x : ℝ) :
    (∫ θ in (0 : ℝ)..h, deriv (shiftedStaircase h δ θ) x) = h := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase
theorem OAI.CircleDomainRigidity.FiniteTransfer.average_shiftedStaircase_deriv line 124
theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_shiftedStaircase_cutoff_multiplier line 131
Source documentation
A cutoff between the original coordinate and the actual shifted staircase preserves mean multiplier one.
```
theorem integral_shiftedStaircase_cutoff_multiplier {h δ : ℝ}
    (hh : 0 < h) (hδ : 0 < δ) (hδh : δ < h / 4) (x χ : ℝ) :
    (∫ θ in (0 : ℝ)..h, (1 - χ) + χ * deriv (shiftedStaircase h δ θ) x) = h := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase