Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section24.Sensitivity.Provider.Path.PairingBounds

PairingBounds #

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

Domination of the response densities by the doubled energy density #

The linear response term ℓ is the diagonal of the bilinear pairing

B(X, Y) = -⨍ (h X₁) · (bfA(a) Y)₂,

and the quadratic term q is a second quadratic form in the same variable. Both are dominated pointwise by the doubled energy density of the base coefficient, with a free Young parameter in the bilinear estimate. Working with the energy rather than with an L² norm is what keeps the whole continuity argument inside the doubled functional.

Averaging helpers #

source
theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.volumeAverage_mono_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g U MeasureTheory.volume) (hfg : f ≤ᵐ[HCPolySupport.volumeMeasureOn U] g) :
HCPolySupport.volumeAverage U f ≤ HCPolySupport.volumeAverage U g
source
theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.volumeAverage_neg {d : ℕ} {U : Set (HCPolySupport.Vec d)} (f : HCPolySupport.Vec d → ℝ) :
(HCPolySupport.volumeAverage U fun (x : HCPolySupport.Vec d) => -f x) = -HCPolySupport.volumeAverage U f
source
theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.abs_volumeAverage_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g U MeasureTheory.volume) (hfg : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |f x| ≤ g x) :
|HCPolySupport.volumeAverage U f| ≤ HCPolySupport.volumeAverage U g

The bilinear response pairing #

source
noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinearPairingDensity {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (hField : HCPolySupport.CoeffField d) (X Y : HCPolySupport.Book.Ch02.DoubledField d) :
HCPolySupport.Vec d → ℝ

Density of the bilinear response pairing -(h X₁) · (bfA(a) Y)₂, whose diagonal is the linear response density.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinearPairing {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (hField : HCPolySupport.CoeffField d) (X Y : HCPolySupport.Book.Ch02.DoubledField d) :
    ℝ

    Averaged bilinear response pairing.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinearTerm_eq_pairing {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (hField : HCPolySupport.CoeffField d) (X : HCPolySupport.Book.Ch02.DoubledField d) :
      pathLinearTerm a hField X = pathLinearPairing a hField X X
      source
      theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.integrableOn_pathLinearPairingDensity {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) {X Y : HCPolySupport.Book.Ch02.DoubledField d} (hXpot : HCPolySupport.MemVectorL2 U.carrier X.potential) (hYpot : HCPolySupport.MemVectorL2 U.carrier Y.potential) (hYflux : HCPolySupport.MemVectorL2 U.carrier Y.flux) :
      MeasureTheory.IntegrableOn (pathLinearPairingDensity a (↑h) X Y) U.carrier MeasureTheory.volume

      Pointwise domination by the energy density #

      source
      noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinearConstL {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) :
      ℝ

      The response constants attached to the base coefficient and the L∞ perturbation.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinearConstR {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) :
        ℝ

        The coefficient-dependent constant for the right path pairing estimate.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Path.pathQuadConst {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) :
          ℝ

          The coefficient-dependent constant for the quadratic path pairing estimate.

          Equations
          Instances For
            source
            theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinearConstL_nonneg {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) :
            0 ≤ pathLinearConstL a h
            source
            theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinearConstR_nonneg {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) :
            0 ≤ pathLinearConstR a
            source
            theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathQuadConst_nonneg {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) :
            0 ≤ pathQuadConst a h
            source
            theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockEnergyDensityAt_nonneg {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) {x : HCPolySupport.Vec d} (hx : HCPolySupport.IsEllipticMatrix a.lam a.Lam (a.toCoeffField x)) (Z : HCPolySupport.BlockVec d) :
            0 ≤ HCPolySupport.Book.Ch02.blockEnergyDensityAt a Z x

            The energy density is nonnegative wherever the coefficient is elliptic.

            source
            theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.abs_pathLinearPairingDensity_le {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (X Y : HCPolySupport.Book.Ch02.DoubledField d) {x : HCPolySupport.Vec d} (hx : HCPolySupport.IsEllipticMatrix a.lam a.Lam (a.toCoeffField x)) (hb : ∀ (i j : Fin d), |↑h x i j| ≤ lInfEntryBound h) {η : ℝ} (hη : 0 < η) :
            |pathLinearPairingDensity a (↑h) X Y x| ≤ η * pathLinearConstL a h * HCPolySupport.Book.Ch02.blockEnergyDensityAt a (X.eval x) x + η⁻¹ * pathLinearConstR a * HCPolySupport.Book.Ch02.blockEnergyDensityAt a (Y.eval x) x

            Young estimate for the bilinear response pairing. Both slots are controlled by the doubled energy density, with a free positive parameter.

            source
            theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathQuadraticDensity_le {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (X : HCPolySupport.Book.Ch02.DoubledField d) {x : HCPolySupport.Vec d} (hx : HCPolySupport.IsEllipticMatrix a.lam a.Lam (a.toCoeffField x)) (hb : ∀ (i j : Fin d), |↑h x i j| ≤ lInfEntryBound h) :
            pathQuadraticDensity a (↑h) X x ≤ pathQuadConst a h * HCPolySupport.Book.Ch02.blockEnergyDensityAt a (X.eval x) x

            The quadratic response density is dominated by the energy density.

            Averaged domination #

            source
            theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.doubledMuValue_nonneg {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (X : HCPolySupport.Book.Ch02.DoubledField d) :
            0 ≤ HCPolySupport.Book.Ch02.doubledMuValue U a X

            The doubled energy value of any doubled field is nonnegative.

            source
            theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.abs_pathLinearPairing_le {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) {X Y : HCPolySupport.Book.Ch02.DoubledField d} (hXpot : HCPolySupport.MemVectorL2 U.carrier X.potential) (hXflux : HCPolySupport.MemVectorL2 U.carrier X.flux) (hYpot : HCPolySupport.MemVectorL2 U.carrier Y.potential) (hYflux : HCPolySupport.MemVectorL2 U.carrier Y.flux) {η : ℝ} (hη : 0 < η) :
            |pathLinearPairing a (↑h) X Y| ≤ η * pathLinearConstL a h * HCPolySupport.Book.Ch02.doubledMuValue U a X + η⁻¹ * pathLinearConstR a * HCPolySupport.Book.Ch02.doubledMuValue U a Y

            Averaged Young estimate for the bilinear response pairing.

            source
            theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathQuadraticTerm_le {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) {X : HCPolySupport.Book.Ch02.DoubledField d} (hXpot : HCPolySupport.MemVectorL2 U.carrier X.potential) (hXflux : HCPolySupport.MemVectorL2 U.carrier X.flux) :
            pathQuadraticTerm a (↑h) X ≤ pathQuadConst a h * HCPolySupport.Book.Ch02.doubledMuValue U a X

            Averaged domination of the quadratic response term.

            source
            theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.abs_pathLinearTerm_le {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) {X : HCPolySupport.Book.Ch02.DoubledField d} (hXpot : HCPolySupport.MemVectorL2 U.carrier X.potential) (hXflux : HCPolySupport.MemVectorL2 U.carrier X.flux) :
            |pathLinearTerm a (↑h) X| ≤ (pathLinearConstL a h + pathLinearConstR a) * HCPolySupport.Book.Ch02.doubledMuValue U a X

            The linear response term is dominated by the doubled energy value.