RampLocalLaw.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Averaging the sharp local law to a ramp cutoff

theorem OAI.JointDickman.intervalIntegrable_strict_cutoff line 12
theorem OAI.JointDickman.highExclusiveCell_intervalIntegrable line 23

theorem OAI.JointDickman.rampCellMass_eq_average line 45

Source documentation

The linear ramp is exactly an average of sharp high cutoffs.

theorem rampCellMass_eq_average {C E A : Type*} [Fintype E] [DecidableEq A]
    (v : E → ℝ) (cell : C → E → Option A) (location : E → ℝ)
    (c : C) (a : A) {lo hi : ℝ} (hlohi : lo < hi) :
    optionCellMass (fun e => v e * averagingRamp lo hi (location e)) (cell c) a =
      (∫ t in lo..hi, highExclusiveCell v cell (fun e => location e ≤ t) c a) / (hi - lo) := by
…

Mentions: OAI.JointDickman.optionCellMass, OAI.JointDickman.averagingRamp, OAI.JointDickman.highExclusiveCell

theorem OAI.JointDickman.rampCellMass_local_error line 73

Source documentation

Averaging a pointwise local error keeps the same error constant.

theorem rampCellMass_local_error {C E A : Type*} [Fintype E] [DecidableEq A]
    (v : E → ℝ) (cell : C → E → Option A) (location : E → ℝ)
    (c : C) (a : A) {lo hi ε : ℝ} (hlohi : lo < hi) (profile : ℝ → ℝ)
    (hprofile : IntervalIntegrable profile volume lo hi)
    (herror : ∀ t ∈ Set.Icc lo hi,
      |highExclusiveCell v cell (fun e => location e ≤ t) c a - profile t| ≤ ε) :
    |optionCellMass (fun e => v e * averagingRamp lo hi (location e)) (cell c) a -
      (∫ t in lo..hi, profile t) / (hi - lo)| ≤ ε := by
…

Mentions: OAI.JointDickman.highExclusiveCell, OAI.JointDickman.optionCellMass, OAI.JointDickman.averagingRamp