ResponsePairing

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

The response pairing defining D_h

This module builds the canonical bilinear pairing used internally to construct the matrix and proves that its value agrees with every choice of maximizing representatives in the source statement.

noncomputable def Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.adjointResponseGradient {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) : HCPolySupport.BlockVec d → HCPolySupport.Vec d → HCPolySupport.Vec d

The canonical response gradient for the transposed coefficient.

Equations

• Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.adjointResponseGradient U a P = (HCPolySupport.Book.Ch02.canonicalMaximizer ⋯ P.1 P.2).toSolution.toH1.grad

noncomputable def Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.primalResponseGradient {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) : HCPolySupport.BlockVec d → HCPolySupport.Vec d → HCPolySupport.Vec d

The canonical response gradient for the primal coefficient.

Equations

• Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.primalResponseGradient U a P = (HCPolySupport.Book.Ch02.canonicalMaximizer ⋯ P.1 (-P.2)).toSolution.toH1.grad

noncomputable def Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.pairing {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (P Q : HCPolySupport.BlockVec d) : ℝ

The averaged perturbation pairing of adjoint and primal response gradients.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.quadraticForm {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (P : HCPolySupport.BlockVec d) : ℝ

The diagonal quadratic form of the response-gradient perturbation pairing.

Equations

• Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.quadraticForm U a h P = Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.pairing U a h P P

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.adjointResponseGradient_add {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (X Y : HCPolySupport.BlockVec d) : adjointResponseGradient U a (X + Y) =ᵐ[HCPolySupport.volumeMeasureOn U.carrier] fun (x : HCPolySupport.Vec d) => adjointResponseGradient U a X x + adjointResponseGradient U a Y x

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.adjointResponseGradient_smul {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (c : ℝ) (X : HCPolySupport.BlockVec d) : adjointResponseGradient U a (c • X) =ᵐ[HCPolySupport.volumeMeasureOn U.carrier] fun (x : HCPolySupport.Vec d) => c • adjointResponseGradient U a X x

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.primalResponseGradient_add {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (X Y : HCPolySupport.BlockVec d) : primalResponseGradient U a (X + Y) =ᵐ[HCPolySupport.volumeMeasureOn U.carrier] fun (x : HCPolySupport.Vec d) => primalResponseGradient U a X x + primalResponseGradient U a Y x

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.primalResponseGradient_smul {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (c : ℝ) (X : HCPolySupport.BlockVec d) : primalResponseGradient U a (c • X) =ᵐ[HCPolySupport.volumeMeasureOn U.carrier] fun (x : HCPolySupport.Vec d) => c • primalResponseGradient U a X x

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.pairing_integrable {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (P Q : HCPolySupport.BlockVec d) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (adjointResponseGradient U a P x) (HCPolySupport.matVecMul (↑h x) (primalResponseGradient U a Q x))) U.carrier MeasureTheory.volume

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.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

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.average_eq_of_isResponseMaximizers {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (p q : HCPolySupport.Vec d) (vAdj : HCPolySupport.Book.Ch02.Solution U a.transpose) (v : HCPolySupport.Book.Ch02.Solution U a) (hvAdj : HCPolySupport.Book.Ch02.IsResponseMaximizer U a.transpose p q vAdj) (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer U a p (-q) v) : (HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot ((HCPolySupport.Book.Ch02.canonicalMaximizer ⋯ p q).toSolution.toH1.grad x) (HCPolySupport.matVecMul (↑h x) ((HCPolySupport.Book.Ch02.canonicalMaximizer ⋯ p (-q)).toSolution.toH1.grad x))) = HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (vAdj.toH1.grad x) (HCPolySupport.matVecMul (↑h x) (v.toH1.grad x))

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.pairing_add_left {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (X Y Z : HCPolySupport.BlockVec d) : pairing U a h (X + Y) Z = pairing U a h X Z + pairing U a h Y Z

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.pairing_smul_left {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (c : ℝ) (X Y : HCPolySupport.BlockVec d) : pairing U a h (c • X) Y = c * pairing U a h X Y

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.pairing_add_right {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (X Y Z : HCPolySupport.BlockVec d) : pairing U a h X (Y + Z) = pairing U a h X Y + pairing U a h X Z

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.pairing_smul_right {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (c : ℝ) (X Y : HCPolySupport.BlockVec d) : pairing U a h X (c • Y) = c * pairing U a h X Y