OAI/NumberTheory/JointDickman/Amplification/RampDensityIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The averaged profile is the integral of the ramp-weighted density

  1. theorem OAI.JointDickman.clippedIntervalIntegral_eq_indicator line 13
  2. theorem OAI.JointDickman.indicator_density_rectangle_integrable line 31
  3. theorem OAI.JointDickman.rampIntervalIntegral_eq_density line 47

    Source documentation

    Fubini converts the average of sharp tails to the desired weighted Lebesgue integral. Only ordinary continuity of the density is needed.

    theorem rampIntervalIntegral_eq_density (f : ℝ → ℝ) (hf : Continuous f)
    {lo hi a b : ℝ} (hlohi : lo < hi) (hab : a ≤ b) :
    rampIntervalIntegral f lo hi a b 0 =
      ∫ s in a..b, averagingRamp lo hi s * f s := by
…

    Mentions: OAI.JointDickman.rampIntervalIntegral, OAI.JointDickman.averagingRamp