StaircaseMean.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Mean derivative of a randomly shifted staircase

A smooth degree-one lift has average derivative one over a full period. For a uniform shift of the level grid this gives the derivative expectation. Iterated integration gives the corresponding product identity for two independent shifts.

theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_shifted_deriv_eq_period line 19

Source documentation

FTC computes the integral of the shifted derivative over one period.

theorem integral_shifted_deriv_eq_period {P : ℝ → ℝ} {h : ℝ}
    (hP : ContDiff ℝ 1 P) (hperiod : ∀ x, P (x + h) = P x + h) (x : ℝ) :
    (∫ θ in (0 : ℝ)..h, deriv P (x - θ)) = h := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.average_shifted_deriv_eq_one line 30

Source documentation

The normalized uniform-shift mean is exactly one.

theorem average_shifted_deriv_eq_one {P : ℝ → ℝ} {h : ℝ}
    (hh : 0 < h) (hP : ContDiff ℝ 1 P)
    (hperiod : ∀ x, P (x + h) = P x + h) (x : ℝ) :
    (∫ θ in (0 : ℝ)..h, deriv P (x - θ)) / h = 1 := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_cutoff_multiplier line 38

Source documentation

Joining the original coordinate to a shifted staircase by a cutoff preserves the mean derivative multiplier.

theorem integral_cutoff_multiplier {P : ℝ → ℝ} {h : ℝ}
    (hP : ContDiff ℝ 1 P) (hperiod : ∀ x, P (x + h) = P x + h)
    (x χ : ℝ) :
    (∫ θ in (0 : ℝ)..h, (1 - χ) + χ * deriv P (x - θ)) = h := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_independent_cutoff_multipliers line 51

Source documentation

Two independent shifts have product mean one, by iterated integration.

theorem integral_independent_cutoff_multipliers
    {P Q : ℝ → ℝ} {h : ℝ}
    (hP : ContDiff ℝ 1 P) (hQ : ContDiff ℝ 1 Q)
    (hperiodP : ∀ x, P (x + h) = P x + h)
    (hperiodQ : ∀ x, Q (x + h) = Q x + h) (x y χ ψ : ℝ) :
    (∫ θ in (0 : ℝ)..h, ∫ φ in (0 : ℝ)..h,
      ((1 - χ) + χ * deriv P (x - θ)) *
        ((1 - ψ) + ψ * deriv Q (y - φ))) = h ^ 2 := by
…