LogarithmicEnergyTransfer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Returning from logarithmic measure to the original short-average variable

theorem OAI.JointDickman.schwartz_logarithmic_energy_le line 12

Source documentation

On a positive block the Jacobian costs at most the upper endpoint.

theorem schwartz_logarithmic_energy_le (P : 𝓢(ℝ, ℂ)) {X Y : ℝ}
    (hX : 0 < X) (hXY : X ≤ Y) (δ : ℝ) :
    (∫ x in X..Y, ‖P (Real.log x + δ)‖ ^ 2) ≤
      Y * ∫ v : ℝ, ‖P v‖ ^ 2 := by
…