Documentation

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

Densities #

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

Path densities for the coefficient perturbation a + t h #

Along the canonical perturbation path t ↦ perturbCoeffOn U a h t the doubled energy density of a fixed doubled field expands exactly in t:

E_t(X)(x) = E_0(X)(x) + t · L(X)(x) + t² · Q(X)(x)

with the linear density L(X) = -(h X₁)·(bfA(a) X)₂ and the quadratic density Q(X) = ½ (h X₁)·s⁻¹(h X₁). This module defines the two densities, proves the a.e. expansion from the pointwise algebra in PointwiseExpansion, and establishes the L¹ integrability needed to pass to averaged values.

source
theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.volumeAverage_congr_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → ℝ} (hfg : f =ᵐ[HCPolySupport.volumeMeasureOn U] g) :
HCPolySupport.volumeAverage U f = HCPolySupport.volumeAverage U g

Averages only see the a.e. class of the integrand.

The canonical path through the frozen perturbation #

source
theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.perturbCoeffOn_toCoeffField_apply {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (t : ℝ) (x : HCPolySupport.Vec d) :
(Frozen.Section24.perturbCoeffOn U a h t).toCoeffField x = a.toCoeffField x + t • ↑↑h x

The frozen perturbation body evaluated at a point.

source
theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.perturbCoeffOn_zero_aeeq {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) :
(Frozen.Section24.perturbCoeffOn U a h 0).AEEq a

At t = 0 the canonical path starts at the base field, up to a null set.

The linear and quadratic path densities #

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

Linear-response density of a doubled field along the path: the exact cross term -(h X₁) · (bfA(a) X)₂ produced by the shear conjugation.

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

    Quadratic-response density of a doubled field along the path: ½ (h X₁) · s⁻¹ (h X₁).

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

      Averaged linear-response term.

      Equations
      Instances For
        source
        noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Path.pathQuadraticTerm {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (hField : HCPolySupport.CoeffField d) (X : HCPolySupport.Book.Ch02.DoubledField d) :
        ℝ

        Averaged quadratic-response term.

        Equations
        Instances For

          The exact pointwise and a.e. expansions along the path #

          source
          theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockEnergyDensityAt_perturbCoeffOn {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (t : ℝ) {x : HCPolySupport.Vec d} (hx : HCPolySupport.symmPart (↑↑h x) = 0) (X : HCPolySupport.BlockVec d) :
          HCPolySupport.Book.Ch02.blockEnergyDensityAt (Frozen.Section24.perturbCoeffOn U a h t) X x = HCPolySupport.Book.Ch02.blockEnergyDensityAt a X x + t * -HCPolySupport.vecDot (HCPolySupport.matVecMul (↑↑h x) X.1) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockMatrixField a x) X).2 + t ^ 2 * (1 / 2 * HCPolySupport.vecDot (HCPolySupport.matVecMul (↑↑h x) X.1) (HCPolySupport.matVecMul (HCPolySupport.symmPart (a.toCoeffField x))⁻¹ (HCPolySupport.matVecMul (↑↑h x) X.1)))

          Exact expansion of the doubled energy density along the canonical path at a point where the perturbation is skew.

          source
          theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockEnergyDensity_expansion_ae {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (t : ℝ) (X : HCPolySupport.Book.Ch02.DoubledField d) :
          (fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.blockEnergyDensityAt (Frozen.Section24.perturbCoeffOn U a h t) (X.eval x) x) =ᵐ[HCPolySupport.volumeMeasureOn U.carrier] fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.blockEnergyDensityAt a (X.eval x) x + t * pathLinearDensity a (↑↑h) X x + t ^ 2 * pathQuadraticDensity a (↑↑h) X x

          The a.e. exact expansion of the doubled energy density of a doubled field along the canonical path.

          Square integrability of the block image of an L² doubled field #

          source
          theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.memVectorL2_blockMatrixField_snd {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) {X : HCPolySupport.Book.Ch02.DoubledField d} (hpot : HCPolySupport.MemVectorL2 U.carrier X.potential) (hflux : HCPolySupport.MemVectorL2 U.carrier X.flux) :
          HCPolySupport.MemVectorL2 U.carrier fun (x : HCPolySupport.Vec d) => (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockMatrixField a x) (X.eval x)).2

          The second block component of bfA(a) X is vector L² when the doubled field has vector L² components.

          source
          theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.memVectorL2_blockMatrixField_fst {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) {X : HCPolySupport.Book.Ch02.DoubledField d} (hpot : HCPolySupport.MemVectorL2 U.carrier X.potential) (hflux : HCPolySupport.MemVectorL2 U.carrier X.flux) :
          HCPolySupport.MemVectorL2 U.carrier fun (x : HCPolySupport.Vec d) => (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockMatrixField a x) (X.eval x)).1

          The first block component of bfA(a) X is vector L² when the doubled field has vector L² components.

          source
          theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.memVectorL2_matVecMul_symmPartInv {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 U.carrier f) :
          HCPolySupport.MemVectorL2 U.carrier fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (HCPolySupport.symmPart (a.toCoeffField x))⁻¹ (f x)

          Applying the a.e. inverse of the symmetric part preserves vector L².

          Memberships from mu-admissibility #

          source
          theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.memVectorL2_potential_of_isDoubledMuAdmissible {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {P : HCPolySupport.BlockVec d} {X : HCPolySupport.Book.Ch02.DoubledField d} (hX : HCPolySupport.Book.Ch02.IsDoubledMuAdmissible U P X) :
          HCPolySupport.MemVectorL2 U.carrier X.potential

          The potential component of a mu-admissible doubled field is vector L².

          source
          theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.memVectorL2_flux_of_isDoubledMuAdmissible {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {P : HCPolySupport.BlockVec d} {X : HCPolySupport.Book.Ch02.DoubledField d} (hX : HCPolySupport.Book.Ch02.IsDoubledMuAdmissible U P X) :
          HCPolySupport.MemVectorL2 U.carrier X.flux

          The flux component of a mu-admissible doubled field is vector L².

          Integrability of the densities #

          source
          theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.integrableOn_blockEnergyDensity {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) {X : HCPolySupport.Book.Ch02.DoubledField d} (hpot : HCPolySupport.MemVectorL2 U.carrier X.potential) (hflux : HCPolySupport.MemVectorL2 U.carrier X.flux) :
          MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.blockEnergyDensityAt a (X.eval x) x) U.carrier MeasureTheory.volume

          The base doubled energy density of an L² doubled field is integrable.

          source
          theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.integrableOn_pathLinearDensity {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) {X : HCPolySupport.Book.Ch02.DoubledField d} (hpot : HCPolySupport.MemVectorL2 U.carrier X.potential) (hflux : HCPolySupport.MemVectorL2 U.carrier X.flux) :
          MeasureTheory.IntegrableOn (pathLinearDensity a (↑h) X) U.carrier MeasureTheory.volume

          The linear path density is integrable for L² doubled fields and L∞ perturbations.

          source
          theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.integrableOn_pathQuadraticDensity {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) {X : HCPolySupport.Book.Ch02.DoubledField d} (hpot : HCPolySupport.MemVectorL2 U.carrier X.potential) :
          MeasureTheory.IntegrableOn (pathQuadraticDensity a (↑h) X) U.carrier MeasureTheory.volume

          The quadratic path density is integrable for L² doubled fields and L∞ perturbations.