Coarse-graining support: Support.CoarseGraining.ResponseIdentities.Existence

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.AHarmonicGradientHilbert.memVectorL2_const {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (p : Vec d) : MemVectorL2 U fun (x : Vec d) => p

noncomputable def HCPolySupport.AHarmonicGradientHilbert.responseFunctionalCLM {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) : ↥(Space M hEll) →L[ℝ] ℝ

The linear response functional F ↦ ∫_U q·F - p·aF on the closed A-harmonic-gradient Hilbert space.

Equations

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

theorem HCPolySupport.AHarmonicGradientHilbert.responseFunctionalCLM_apply_eq_integral {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (p q : Vec d) (z : ↥(Space M hEll)) : (responseFunctionalCLM M hEll p q) z = ∫ (x : Vec d) in U, vecDot q (↑↑(vectorField z) x) - vecDot p (matVecMul (a x) (↑↑(vectorField z) x))

noncomputable def HCPolySupport.AHarmonicGradientHilbert.responseStationaryGradient {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (M : PotentialSolenoidalL2Data U) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) : ↥(Space M hEll)

The Hilbert-space stationary point for the scalar response functional.

Equations

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

theorem HCPolySupport.AHarmonicGradientHilbert.responseStationaryGradient_firstVariation {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {M : PotentialSolenoidalL2Data U} (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (w : ↥(Space M hEll)) : ((symmCoeffBilin M hEll) (responseStationaryGradient M hne hEll p q)) w = (responseFunctionalCLM M hEll p q) w

noncomputable def HCPolySupport.AHarmonicGradientHilbert.responseStationaryAHarmonicFunction {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hne : U.Nonempty) (hHodge : HodgeConverseCriterion U) (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) : AHarmonicFunction a U

Recover the Hilbert stationary point as a concrete A-harmonic function using the Hodge converse.

Equations

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

theorem HCPolySupport.AHarmonicGradientHilbert.responseStationaryAHarmonicFunction_firstVariation_integral_eq_zero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hne : U.Nonempty) (hHodge : HodgeConverseCriterion U) (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (w : AHarmonicFunction a U) : ∫ (x : Vec d) in U, scalarFirstVariationIntegrand U a p q (responseStationaryAHarmonicFunction hne ⋯ hEll p q) w x = 0

theorem HCPolySupport.ScalarCanonicalMaximizer.nonempty_of_hodgeConverseCriterion_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hne : U.Nonempty) (hHodge : HodgeConverseCriterion U) (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) : Nonempty (ScalarCanonicalMaximizer U p q a)

theorem HCPolySupport.ScalarCanonicalMaximizer.nonempty_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hne : U.Nonempty) (hU : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) : Nonempty (ScalarCanonicalMaximizer U p q a)

theorem HCPolySupport.ScalarCanonicalMaximizer.volumeAverage_cubeSet_eq_openCubeSet_of_triadicCube {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : volumeAverage (cubeSet Q) f = volumeAverage (openCubeSet Q) f

theorem HCPolySupport.ScalarCanonicalMaximizer.isResponseMaximizer_toCubeSet_of_openCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {p q : Vec d} (v : ScalarCanonicalMaximizer (openCubeSet Q) p q a) : IsResponseMaximizer (cubeSet Q) p q a v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toCubeSet

noncomputable def HCPolySupport.ScalarCanonicalMaximizer.toCubeSetOfOpenCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {p q : Vec d} (v : ScalarCanonicalMaximizer (openCubeSet Q) p q a) : ScalarCanonicalMaximizer (cubeSet Q) p q a

Transport of a canonical maximizer from an open triadic cube to its half-open cube, using equality up to a null boundary.

Equations

• v.toCubeSetOfOpenCubeSet = HCPolySupport.ScalarCanonicalMaximizer.ofIsResponseMaximizer v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toCubeSet ⋯

theorem HCPolySupport.ScalarCanonicalMaximizer.nonempty_cubeSet_of_isEllipticFieldOn_openCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (p q : Vec d) : Nonempty (ScalarCanonicalMaximizer (cubeSet Q) p q a)

theorem HCPolySupport.ScalarCanonicalMaximizer.GradientBasisData.nonempty_of_hodgeConverseCriterion_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hne : U.Nonempty) (hHodge : HodgeConverseCriterion U) (hEll : IsEllipticFieldOn lam Lam U a) : Nonempty (GradientBasisData U a)

theorem HCPolySupport.ScalarCanonicalMaximizer.GradientBasisData.nonempty_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hne : U.Nonempty) (hU : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U a) : Nonempty (GradientBasisData U a)

theorem HCPolySupport.ScalarCanonicalMaximizer.FluxBasisData.nonempty_of_hodgeConverseCriterion_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hne : U.Nonempty) (hHodge : HodgeConverseCriterion U) (hEll : IsEllipticFieldOn lam Lam U a) : Nonempty (FluxBasisData U a)

theorem HCPolySupport.ScalarCanonicalMaximizer.FluxBasisData.nonempty_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hne : U.Nonempty) (hU : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U a) : Nonempty (FluxBasisData U a)