Coarse-graining support: Support.CoarseGraining.ResponseIdentities.AverageFormulas.CanonicalBasic

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

Average formulas (part 3) -- ScalarCanonicalMaximizer basic API

ScalarCanonicalMaximizer namespace: responseJ_eq, first/second variation, energy, linear response, polarization, averagePairing, together with the GradientBasisData and FluxBasisData structures and their nonempty constructors.

theorem HCPolySupport.ScalarCanonicalMaximizer.responseJ_eq {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) : ResponseJ U p q a = volumeAverage U (scalarResponseIntegrand U a p q v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)

theorem HCPolySupport.ScalarCanonicalMaximizer.firstVariation {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) (w : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a v.toAHarmonicFunctionMeanZero.toAHarmonicFunction) (hw_int : weakFluxIntegrable U a w) (hresp_v : MeasureTheory.IntegrableOn (scalarResponseIntegrand U a p q v.toAHarmonicFunctionMeanZero.toAHarmonicFunction) U MeasureTheory.volume) (hlin : MeasureTheory.IntegrableOn (scalarFirstVariationIntegrand U a p q v.toAHarmonicFunctionMeanZero.toAHarmonicFunction w) U MeasureTheory.volume) (henergy : MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand a w) U MeasureTheory.volume) : volumeAverage U (scalarFirstVariationIntegrand U a p q v.toAHarmonicFunctionMeanZero.toAHarmonicFunction w) = 0

theorem HCPolySupport.ScalarCanonicalMaximizer.secondVariationLine {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) (w : AHarmonicFunction a U) (t : ℝ) (hu_int : weakFluxIntegrable U a v.toAHarmonicFunctionMeanZero.toAHarmonicFunction) (hw_int : weakFluxIntegrable U a w) (hresp_v : MeasureTheory.IntegrableOn (scalarResponseIntegrand U a p q v.toAHarmonicFunctionMeanZero.toAHarmonicFunction) U MeasureTheory.volume) (hlin : MeasureTheory.IntegrableOn (scalarFirstVariationIntegrand U a p q v.toAHarmonicFunctionMeanZero.toAHarmonicFunction w) U MeasureTheory.volume) (henergy : MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand a w) U MeasureTheory.volume) : volumeAverage U (scalarResponseIntegrand U a p q (scalarPerturbation v.toAHarmonicFunctionMeanZero.toAHarmonicFunction w t hu_int hw_int)) = ResponseJ U p q a - t ^ 2 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a w)

theorem HCPolySupport.ScalarCanonicalMaximizer.secondVariation {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) (w : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a v.toAHarmonicFunctionMeanZero.toAHarmonicFunction) (hw_int : weakFluxIntegrable U a w) (hresp_v : MeasureTheory.IntegrableOn (scalarResponseIntegrand U a p q v.toAHarmonicFunctionMeanZero.toAHarmonicFunction) U MeasureTheory.volume) (hlin : MeasureTheory.IntegrableOn (scalarFirstVariationIntegrand U a p q v.toAHarmonicFunctionMeanZero.toAHarmonicFunction w) U MeasureTheory.volume) (henergy : MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand a w) U MeasureTheory.volume) : volumeAverage U (scalarResponseIntegrand U a p q (scalarPerturbation v.toAHarmonicFunctionMeanZero.toAHarmonicFunction w 1 hu_int hw_int)) = ResponseJ U p q a - 1 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a w)

theorem HCPolySupport.ScalarCanonicalMaximizer.energy {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) (hu_int : ∀ (φ : H10Function U), MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x)) (φ.grad x)) U MeasureTheory.volume) (hresp_v : MeasureTheory.IntegrableOn (scalarResponseIntegrand U a p q v.toAHarmonicFunctionMeanZero.toAHarmonicFunction) U MeasureTheory.volume) (hlin_self : MeasureTheory.IntegrableOn (scalarFirstVariationIntegrand U a p q v.toAHarmonicFunctionMeanZero.toAHarmonicFunction v.toAHarmonicFunctionMeanZero.toAHarmonicFunction) U MeasureTheory.volume) (henergy : MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand a v.toAHarmonicFunctionMeanZero.toAHarmonicFunction) U MeasureTheory.volume) : ResponseJ U p q a = 1 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)

theorem HCPolySupport.ScalarCanonicalMaximizer.linearResponseSq {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (hInt : ResponseLinearIntegrabilityData U a) (w : AHarmonicFunction a U) : ((volumeAverage U fun (x : Vec d) => vecDot q (w.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (a x) (w.toH1.grad x))) ^ 2 ≤ volumeAverage U (scalarVariationEnergyIntegrand a w) * (2 * ResponseJ U p q a)

theorem HCPolySupport.ScalarCanonicalMaximizer.linearResponseSqOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (w : AHarmonicFunction a U) : ((volumeAverage U fun (x : Vec d) => vecDot q (w.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (a x) (w.toH1.grad x))) ^ 2 ≤ volumeAverage U (scalarVariationEnergyIntegrand a w) * (2 * ResponseJ U p q a)

theorem HCPolySupport.ScalarCanonicalMaximizer.linearResponse {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (hInt : ResponseLinearIntegrabilityData U a) (w : AHarmonicFunction a U) : |(volumeAverage U fun (x : Vec d) => vecDot q (w.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (a x) (w.toH1.grad x))| ≤ √(volumeAverage U (scalarVariationEnergyIntegrand a w)) * √(2 * ResponseJ U p q a)

theorem HCPolySupport.ScalarCanonicalMaximizer.linearResponseOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (v : ScalarCanonicalMaximizer U p q a) (hEll : IsEllipticFieldOn lam Lam U a) (w : AHarmonicFunction a U) : |(volumeAverage U fun (x : Vec d) => vecDot q (w.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (a x) (w.toH1.grad x))| ≤ √(volumeAverage U (scalarVariationEnergyIntegrand a w)) * √(2 * ResponseJ U p q a)

theorem HCPolySupport.ScalarCanonicalMaximizer.polarization {d : ℕ} {U : Set (Vec d)} {p q p' q' : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) (v' : ScalarCanonicalMaximizer U p' q' a) (hInt : ResponseLinearIntegrabilityData U a) : (volumeAverage U fun (x : Vec d) => vecDot (v'.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) (matVecMul (symmPart (a x)) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x))) = ResponseJ U p q a + ResponseJ U p' q' a - ResponseJ U (p - p') (q - q') a

theorem HCPolySupport.ScalarCanonicalMaximizer.polarizationOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q p' q' : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (v : ScalarCanonicalMaximizer U p q a) (v' : ScalarCanonicalMaximizer U p' q' a) (hEll : IsEllipticFieldOn lam Lam U a) : (volumeAverage U fun (x : Vec d) => vecDot (v'.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x) (matVecMul (symmPart (a x)) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x))) = ResponseJ U p q a + ResponseJ U p' q' a - ResponseJ U (p - p') (q - q') a

theorem HCPolySupport.ScalarCanonicalMaximizer.averagePairing {d : ℕ} {U : Set (Vec d)} {p q p' q' : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) (v' : ScalarCanonicalMaximizer U p' q' a) (hInt : ResponseLinearIntegrabilityData U a) : ((volumeAverage U fun (x : Vec d) => vecDot q' (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p' (matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x))) = ResponseJ U p q a + ResponseJ U p' q' a - ResponseJ U (p - p') (q - q') a

theorem HCPolySupport.ScalarCanonicalMaximizer.averagePairingOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {p q p' q' : Vec d} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (v : ScalarCanonicalMaximizer U p q a) (v' : ScalarCanonicalMaximizer U p' q' a) (hEll : IsEllipticFieldOn lam Lam U a) : ((volumeAverage U fun (x : Vec d) => vecDot q' (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p' (matVecMul (a x) (v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad x))) = ResponseJ U p q a + ResponseJ U p' q' a - ResponseJ U (p - p') (q - q') a

structure HCPolySupport.ScalarCanonicalMaximizer.GradientBasisData {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Type

A family of canonical scalar response maximizers for loads p = 0 and q = eᵢ.

• grad (i : Fin d) : ScalarCanonicalMaximizer U 0 (Pi.single i 1) a

  The canonical maximizer for zero p load and the ith coordinate vector as q load.

structure HCPolySupport.ScalarCanonicalMaximizer.FluxBasisData {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Type

A family of canonical scalar response maximizers for loads p = eᵢ and q = 0.

• flux (i : Fin d) : ScalarCanonicalMaximizer U (Pi.single i 1) 0 a

  The canonical maximizer for the ith coordinate vector as p load and zero q load.

noncomputable def HCPolySupport.ScalarCanonicalMaximizer.GradientBasisData.ofNonempty {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (h : ∀ (i : Fin d), Nonempty (ScalarCanonicalMaximizer U 0 (Pi.single i 1) a)) : GradientBasisData U a

A chosen family of canonical maximizers for the coordinate q loads, from their nonemptiness.

Equations

• HCPolySupport.ScalarCanonicalMaximizer.GradientBasisData.ofNonempty h = { grad := fun (i : Fin d) => Classical.choice ⋯ }

theorem HCPolySupport.ScalarCanonicalMaximizer.GradientBasisData.nonempty_of_forall_nonempty {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (h : ∀ (i : Fin d), Nonempty (ScalarCanonicalMaximizer U 0 (Pi.single i 1) a)) : Nonempty (GradientBasisData U a)

theorem HCPolySupport.ScalarCanonicalMaximizer.GradientBasisData.nonempty_of_forall_exists_firstVariation_eq_zero_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (hex : ∀ (i : Fin d), ∃ (u : AHarmonicFunction a U), ∀ (w : AHarmonicFunction a U), volumeAverage U (scalarFirstVariationIntegrand U a 0 (Pi.single i 1) u w) = 0) : Nonempty (GradientBasisData U a)

theorem HCPolySupport.ScalarCanonicalMaximizer.GradientBasisData.nonempty_of_forall_exists_firstVariation_integral_eq_zero_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (hex : ∀ (i : Fin d), ∃ (u : AHarmonicFunction a U), ∀ (w : AHarmonicFunction a U), ∫ (x : Vec d) in U, scalarFirstVariationIntegrand U a 0 (Pi.single i 1) u w x = 0) : Nonempty (GradientBasisData U a)

noncomputable def HCPolySupport.ScalarCanonicalMaximizer.FluxBasisData.ofNonempty {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (h : ∀ (i : Fin d), Nonempty (ScalarCanonicalMaximizer U (Pi.single i 1) 0 a)) : FluxBasisData U a

A chosen family of canonical maximizers for the coordinate p loads, from their nonemptiness.

Equations

• HCPolySupport.ScalarCanonicalMaximizer.FluxBasisData.ofNonempty h = { flux := fun (i : Fin d) => Classical.choice ⋯ }

theorem HCPolySupport.ScalarCanonicalMaximizer.FluxBasisData.nonempty_of_forall_nonempty {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (h : ∀ (i : Fin d), Nonempty (ScalarCanonicalMaximizer U (Pi.single i 1) 0 a)) : Nonempty (FluxBasisData U a)

theorem HCPolySupport.ScalarCanonicalMaximizer.FluxBasisData.nonempty_of_forall_exists_firstVariation_eq_zero_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (hex : ∀ (i : Fin d), ∃ (u : AHarmonicFunction a U), ∀ (w : AHarmonicFunction a U), volumeAverage U (scalarFirstVariationIntegrand U a (Pi.single i 1) 0 u w) = 0) : Nonempty (FluxBasisData U a)

theorem HCPolySupport.ScalarCanonicalMaximizer.FluxBasisData.nonempty_of_forall_exists_firstVariation_integral_eq_zero_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (hex : ∀ (i : Fin d), ∃ (u : AHarmonicFunction a U), ∀ (w : AHarmonicFunction a U), ∫ (x : Vec d) in U, scalarFirstVariationIntegrand U a (Pi.single i 1) 0 u w x = 0) : Nonempty (FluxBasisData U a)