Squared Dual Pairing Bound from a Source Identity

This statement gives a squared dual pairing estimate from a latent source identity.

Let $Ω$ be a measurable space with measure $P$, let $μ$ be a probability measure on $\mathbb R^n$, and let $Z,F:Ω\to\mathbb R^n$. Assume:

1. $Z$ is measurable and map Z P = μ;
2. $F\in L^2(P)$;
3. $v\in\mathbb R^n$ and $h:\mathbb R^n\to\mathbb R$ is smooth with compact support;
4. the source identity holds:

Then

Here the derivative norm is expressed in Lean as ‖fderiv ℝ h x‖. The result is a general latent-space Cauchy–Schwarz bound and does not assume that $Z$ is invertible.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.Stein. Shown in its original module context. Proof omitted.

theorem compact_linear_pairing_sq_le_of_source_identity
    {Ω : Type*} [MeasurableSpace Ω] {n : ℕ}
    (P : Measure Ω) (mu : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
    (Z F : Ω → EuclideanSpace ℝ (Fin n)) (hZ : Measurable Z)
    (hmap : P.map Z = (mu : Measure (EuclideanSpace ℝ (Fin n))))
    (hF : MemLp F 2 P) (v : EuclideanSpace ℝ (Fin n))
    (h : EuclideanSpace ℝ (Fin n) → ℝ) (hh : ContDiff ℝ ∞ h) (hhc : HasCompactSupport h)
    (hid : (∫ x, ⟪x, v⟫ * h x ∂(mu : Measure (EuclideanSpace ℝ (Fin n)))) =
      ∫ w, ⟪F w, gradient h (Z w)⟫ ∂P) :
    (∫ x, ⟪x, v⟫ * h x ∂(mu : Measure (EuclideanSpace ℝ (Fin n)))) ^ 2 ≤
      (∫ w, ‖F w‖ ^ 2 ∂P) *
        ∫ x, ‖fderiv ℝ h x‖ ^ 2 ∂(mu : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Probability/Stein/SourceDualBound.

Source excerpt, lines 26–37 · Frozen source 408915f.