Coarse-graining support: Support.CoarseGraining.ResponseIdentities.Foundations.Maximizer

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

Response maximizer identities

ResponseLinearIntegrabilityData, IsResponseMaximizer, ScalarCanonicalMaximizer, and the basic coarse-graining identities (basic_cg_identities_first_variation_*, basic_cg_identities_sub_*).

structure HCPolySupport.ResponseLinearIntegrabilityData {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Prop

Integrability on U of weak fluxes, constant gradient and flux pairings, and symmetric coefficient cross energies for all a-harmonic functions.

• weakFlux (u : AHarmonicFunction a U) : weakFluxIntegrable U a u
• grad (q : Vec d) (u : AHarmonicFunction a U) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot q (u.toH1.grad x)) U MeasureTheory.volume
• flux (p : Vec d) (u : AHarmonicFunction a U) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot p (matVecMul (a x) (u.toH1.grad x))) U MeasureTheory.volume
• cross (u w : AHarmonicFunction a U) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (w.toH1.grad x) (matVecMul (symmPart (a x)) (u.toH1.grad x))) U MeasureTheory.volume

theorem HCPolySupport.ResponseLinearIntegrabilityData.of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) : ResponseLinearIntegrabilityData U a

theorem HCPolySupport.ResponseLinearIntegrabilityData.energy {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hInt : ResponseLinearIntegrabilityData U a) (w : AHarmonicFunction a U) : MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand a w) U MeasureTheory.volume

theorem HCPolySupport.ResponseLinearIntegrabilityData.firstVariation {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hInt : ResponseLinearIntegrabilityData U a) (p q : Vec d) (u w : AHarmonicFunction a U) : MeasureTheory.IntegrableOn (scalarFirstVariationIntegrand U a p q u w) U MeasureTheory.volume

theorem HCPolySupport.ResponseLinearIntegrabilityData.response {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (hInt : ResponseLinearIntegrabilityData U a) (p q : Vec d) (u : AHarmonicFunction a U) : MeasureTheory.IntegrableOn (scalarResponseIntegrand U a p q u) U MeasureTheory.volume

def HCPolySupport.IsResponseMaximizer {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) (u : AHarmonicFunction a U) : Prop

The function's averaged scalar response is at least that of every a-harmonic competitor.

Equations

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

theorem HCPolySupport.IsResponseMaximizer.addConst {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {u : AHarmonicFunction a U} (hmax : IsResponseMaximizer U p q a u) (c : ℝ) : IsResponseMaximizer U p q a (u.addConst c)

theorem HCPolySupport.IsResponseMaximizer.normalizeMeanZero {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {u : AHarmonicFunction a U} (hmax : IsResponseMaximizer U p q a u) : IsResponseMaximizer U p q a u.normalizeMeanZero

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

A mean-zero a-harmonic function maximizing the averaged scalar response.

• toAHarmonicFunctionMeanZero : AHarmonicFunctionMeanZero a U

  The mean-zero harmonic representative of the maximizing function.

• isMaximizer : IsResponseMaximizer U p q a self.toAHarmonicFunctionMeanZero.toAHarmonicFunction

@[instance_reducible]

instance HCPolySupport.ScalarCanonicalMaximizer.instCoeOutAHarmonicFunctionMeanZero {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} : CoeOut (ScalarCanonicalMaximizer U p q a) (AHarmonicFunctionMeanZero a U)

Equations

• HCPolySupport.ScalarCanonicalMaximizer.instCoeOutAHarmonicFunctionMeanZero = { coe := fun (v : HCPolySupport.ScalarCanonicalMaximizer U p q a) => v.toAHarmonicFunctionMeanZero }

@[instance_reducible]

instance HCPolySupport.ScalarCanonicalMaximizer.instCoeOutAHarmonicFunction {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} : CoeOut (ScalarCanonicalMaximizer U p q a) (AHarmonicFunction a U)

Equations

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

theorem HCPolySupport.ScalarCanonicalMaximizer.meanZero {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) : MeanZeroOn U v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.toFun

theorem HCPolySupport.ScalarCanonicalMaximizer.isResponseMaximizer {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} (v : ScalarCanonicalMaximizer U p q a) : IsResponseMaximizer U p q a v.toAHarmonicFunctionMeanZero.toAHarmonicFunction

noncomputable def HCPolySupport.ScalarCanonicalMaximizer.ofIsResponseMaximizer {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) : ScalarCanonicalMaximizer U p q a

Normalize a scalar response maximizer by subtracting its volume mean.

Equations

• HCPolySupport.ScalarCanonicalMaximizer.ofIsResponseMaximizer u hmax = { toAHarmonicFunctionMeanZero := u.toMeanZero, isMaximizer := ⋯ }

@[simp]

theorem HCPolySupport.ScalarCanonicalMaximizer.coe_ofIsResponseMaximizer {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) : (ofIsResponseMaximizer u hmax).toAHarmonicFunctionMeanZero.toAHarmonicFunction = u.normalizeMeanZero

noncomputable def HCPolySupport.scalarPerturbation {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u w : AHarmonicFunction a U) (t : ℝ) (hu_int : weakFluxIntegrable U a u) (hw_int : weakFluxIntegrable U a w) : AHarmonicFunction a U

The harmonic perturbation u + t • w, built using integrable weak fluxes.

Equations

• HCPolySupport.scalarPerturbation u w t hu_int hw_int = u.addSMulOfIntegrable w hu_int hw_int t

@[simp]

theorem HCPolySupport.scalarPerturbation_grad {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u w : AHarmonicFunction a U) (t : ℝ) (hu_int : weakFluxIntegrable U a u) (hw_int : weakFluxIntegrable U a w) : (scalarPerturbation u w t hu_int hw_int).toH1.grad = u.toH1.grad + t • w.toH1.grad

theorem HCPolySupport.scalarResponseIntegrand_scalarPerturbation {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (u w : AHarmonicFunction a U) (t : ℝ) (hu_int : weakFluxIntegrable U a u) (hw_int : weakFluxIntegrable U a w) : scalarResponseIntegrand U a p q (scalarPerturbation u w t hu_int hw_int) = scalarResponseIntegrand U a p q u + t • scalarFirstVariationIntegrand U a p q u w - (t ^ 2 / 2) • scalarVariationEnergyIntegrand a w

theorem HCPolySupport.volumeAverage_scalarResponseIntegrand_scalarPerturbation {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (u w : AHarmonicFunction a U) (t : ℝ) (hu_int : weakFluxIntegrable U a u) (hw_int : weakFluxIntegrable U a w) (hresp_u : MeasureTheory.IntegrableOn (scalarResponseIntegrand U a p q u) U MeasureTheory.volume) (hlin : MeasureTheory.IntegrableOn (scalarFirstVariationIntegrand U a p q u w) U MeasureTheory.volume) (henergy : MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand a w) U MeasureTheory.volume) : volumeAverage U (scalarResponseIntegrand U a p q (scalarPerturbation u w t hu_int hw_int)) = volumeAverage U (scalarResponseIntegrand U a p q u) + t * volumeAverage U (scalarFirstVariationIntegrand U a p q u w) - t ^ 2 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a w)

theorem HCPolySupport.scalarFirstVariationIntegrand_split {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q p' q' : Vec d) (u w : AHarmonicFunction a U) : scalarFirstVariationIntegrand U a p q u w = scalarFirstVariationIntegrand U a p' q' u w + scalarResponseIntegrand U a (p - p') (q - q') w + (1 / 2) • scalarVariationEnergyIntegrand a w

theorem HCPolySupport.scalarResponseIntegrand_scalarPerturbation_one_split {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q p' q' : Vec d) (u w : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (hw_int : weakFluxIntegrable U a w) : scalarResponseIntegrand U a p q (scalarPerturbation u w 1 hu_int hw_int) = scalarResponseIntegrand U a p q u + scalarResponseIntegrand U a (p - p') (q - q') w + scalarFirstVariationIntegrand U a p' q' u w

theorem HCPolySupport.linearCoeff_eq_zero_of_quadratic_nonpos (L Q : ℝ) (h : ∀ (t : ℝ), t * L - t ^ 2 / 2 * Q ≤ 0) : L = 0

theorem HCPolySupport.basic_cg_identities_first_variation_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (w : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (hw_int : weakFluxIntegrable U a w) (hresp_u : MeasureTheory.IntegrableOn (scalarResponseIntegrand U a p q u) U MeasureTheory.volume) (hlin : MeasureTheory.IntegrableOn (scalarFirstVariationIntegrand U a p q u w) U MeasureTheory.volume) (henergy : MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand a w) U MeasureTheory.volume) : volumeAverage U (scalarFirstVariationIntegrand U a p q u w) = 0

theorem HCPolySupport.basic_cg_identities_first_variation_eq_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (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 fun (x : Vec d) => vecDot (w.toH1.grad x) (matVecMul (symmPart (a x)) (u.toH1.grad x))

theorem HCPolySupport.isResponseMaximizer_of_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) (p q : Vec d) (u : AHarmonicFunction a U) (hfirst : ∀ (w : AHarmonicFunction a U), volumeAverage U (scalarFirstVariationIntegrand U a p q u w) = 0) : IsResponseMaximizer U p q a u

theorem HCPolySupport.ScalarCanonicalMaximizer.firstVariation_eq_zero_of_integral_eq_zero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {p q : Vec d} {u : AHarmonicFunction a U} (hfirst : ∀ (w : AHarmonicFunction a U), ∫ (x : Vec d) in U, scalarFirstVariationIntegrand U a p q u w x = 0) (w : AHarmonicFunction a U) : volumeAverage U (scalarFirstVariationIntegrand U a p q u w) = 0

noncomputable def HCPolySupport.ScalarCanonicalMaximizer.ofFirstVariationEqZeroOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (u : AHarmonicFunction a U) (hfirst : ∀ (w : AHarmonicFunction a U), volumeAverage U (scalarFirstVariationIntegrand U a p q u w) = 0) : ScalarCanonicalMaximizer U p q a

Construct a mean-zero response maximizer from vanishing first variation under ellipticity.

Equations

• HCPolySupport.ScalarCanonicalMaximizer.ofFirstVariationEqZeroOfIsEllipticFieldOn hEll p q u hfirst = HCPolySupport.ScalarCanonicalMaximizer.ofIsResponseMaximizer u ⋯

@[simp]

theorem HCPolySupport.ScalarCanonicalMaximizer.coe_ofFirstVariationEqZeroOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (u : AHarmonicFunction a U) (hfirst : ∀ (w : AHarmonicFunction a U), volumeAverage U (scalarFirstVariationIntegrand U a p q u w) = 0) : (ofFirstVariationEqZeroOfIsEllipticFieldOn hEll p q u hfirst).toAHarmonicFunctionMeanZero.toAHarmonicFunction = u.normalizeMeanZero

theorem HCPolySupport.ScalarCanonicalMaximizer.nonempty_of_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) (p q : Vec d) (hex : ∃ (u : AHarmonicFunction a U), ∀ (w : AHarmonicFunction a U), volumeAverage U (scalarFirstVariationIntegrand U a p q u w) = 0) : Nonempty (ScalarCanonicalMaximizer U p q a)

theorem HCPolySupport.ScalarCanonicalMaximizer.nonempty_of_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) (p q : Vec d) (hex : ∃ (u : AHarmonicFunction a U), ∀ (w : AHarmonicFunction a U), ∫ (x : Vec d) in U, scalarFirstVariationIntegrand U a p q u w x = 0) : Nonempty (ScalarCanonicalMaximizer U p q a)

theorem HCPolySupport.volumeAverage_scalarResponseIntegrand_scalarPerturbation_one_split_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q p' q' : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p' q' a u) (w : AHarmonicFunction a U) : volumeAverage U (scalarResponseIntegrand U a p q (scalarPerturbation u w 1 ⋯ ⋯)) = volumeAverage U (scalarResponseIntegrand U a p q u) + volumeAverage U (scalarResponseIntegrand U a (p - p') (q - q') w)

theorem HCPolySupport.basic_cg_identities_sub_isResponseMaximizer_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q p' q' : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u u' : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p q a u) (hmax' : IsResponseMaximizer U p' q' a u') : IsResponseMaximizer U (p - p') (q - q') a (u.subOfIntegrable u' ⋯ ⋯)