SourceLineRescale.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact local measure scaling from normalized reference lines to physical intervals. Relative exceptional-set measure has no scale loss.

theorem OAI.LipschitzHilbert.source_line_rescale_measure line 15

Source documentation

The Jacobian cancels exactly against the interval length.

theorem source_line_rescale_measure (r u H : ℝ) (hr : 0 < r)
    (bad : Set ℝ) (hbad : MeasurableSet bad) :
    (volume.restrict (Ico (r*u) (r*(u+H)))) bad =
      ENNReal.ofReal r*(volume.restrict (Ico u (u+H)))
        ((fun x : ℝ => r*x) ⁻¹' bad) := by
…

theorem OAI.LipschitzHilbert.source_line_rescale_tail line 40

Source documentation

A normalized relative measure bound holds on its physical interval with exactly the same relative constant.

theorem source_line_rescale_tail (r u H δ : ℝ) (hr : 0 < r) (bad : Set ℝ) (hbad : MeasurableSet bad)
    (hsmall : (volume.restrict (Ico u (u+H))) ((fun x : ℝ => r*x) ⁻¹' bad) ≤
      ENNReal.ofReal δ*ENNReal.ofReal H) :
    (volume.restrict (Ico (r*u) (r*(u+H)))) bad ≤
      ENNReal.ofReal δ*ENNReal.ofReal (r*H) := by
…