VectorPairing

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The L² pairing bound on the supremum-norm carrier

The ambient carrier Vec d = Fin d → ℝ is normed by the supremum norm, so it is not an inner-product space and the Cauchy-Schwarz inequality is not available on VectorL2 U directly. What is true, and what the energy estimates need, is the same bound with the dimensional factor d:

  |∫_U ⟨F, G⟩| ≤ d ‖F‖_{L²(U)} ‖G‖_{L²(U)} .

The factor enters once, in the pointwise step |⟨x, y⟩| ≤ d ‖x‖ ‖y‖, and is the exact price of measuring a d-term sum by the largest of its factors. No Hilbert carrier is introduced.

Main results

• abs_vecDot_le_dim_mul — the pointwise bound.
• abs_setIntegral_vecDot_le — the integrated bound.
• vecNormSq_matVecMul_le_of_entry_bound — a matrix with entries bounded by delta moves the Euclidean square by at most (d · delta)².

References

• ABK26, the energy estimates of Section 5.1.

1. The pointwise bound

theorem Algsuperdiff.Section5.Support.abs_vecDot_le_dim_mul {d : ℕ} (x y : HCPolySupport.Vec d) : |HCPolySupport.vecDot x y| ≤ ↑d * (‖x‖ * ‖y‖)

The pairing is bounded by d times the product of the supremum norms.

2. The integrated bound

theorem Algsuperdiff.Section5.Support.abs_setIntegral_vecDot_le {d : ℕ} (U : Set (HCPolySupport.Vec d)) {F G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : HCPolySupport.MemVectorL2 U F) (hG : HCPolySupport.MemVectorL2 U G) : |∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (F x) (G x)| ≤ ↑d * (√(∫ (x : HCPolySupport.Vec d) in U, ‖F x‖ ^ 2) * √(∫ (x : HCPolySupport.Vec d) in U, ‖G x‖ ^ 2))

The L² pairing bound on the supremum-norm carrier.

3. A matrix perturbation moves the Euclidean square by (d · delta)²

theorem Algsuperdiff.Section5.Support.norm_matVecMul_le_of_entry_bound {d : ℕ} {A : HCPolySupport.Mat d} {delta : ℝ} (hdelta : 0 ≤ delta) (hA : ∀ (i j : Fin d), |A i j| ≤ delta) (xi : HCPolySupport.Vec d) : ‖HCPolySupport.matVecMul A xi‖ ≤ ↑d * delta * ‖xi‖

An entrywise bound on a matrix bounds its action.