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

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

Ellipticity-driven response bounds

Variation-energy arithmetic on subOfIntegrable, scalarResponseIntegrand_le_plainUpperBound_of_isEllipticFieldOn (the main Young-inequality estimate), and the responseJ supremum structure under ellipticity assumptions.

theorem HCPolySupport.scalarVariationEnergyIntegrand_subOfIntegrable {d : ℕ} (a : CoeffField d) {U : Set (Vec d)} (u u' : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (hu'_int : weakFluxIntegrable U a u') : scalarVariationEnergyIntegrand a (u.subOfIntegrable u' hu_int hu'_int) = scalarVariationEnergyIntegrand a u + scalarVariationEnergyIntegrand a u' - 2 • fun (x : Vec d) => vecDot (u'.toH1.grad x) (matVecMul (symmPart (a x)) (u.toH1.grad x))

theorem HCPolySupport.volumeAverage_scalarVariationEnergyIntegrand_subOfIntegrable {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (hInt : ResponseLinearIntegrabilityData U a) (u u' : AHarmonicFunction a U) : volumeAverage U (scalarVariationEnergyIntegrand a (u.subOfIntegrable u' ⋯ ⋯)) = volumeAverage U (scalarVariationEnergyIntegrand a u) + volumeAverage U (scalarVariationEnergyIntegrand a u') - 2 * volumeAverage U fun (x : Vec d) => vecDot (u'.toH1.grad x) (matVecMul (symmPart (a x)) (u.toH1.grad x))

theorem HCPolySupport.basic_cg_identities_second_variation_line_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) (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 ^ 2 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a w)

theorem HCPolySupport.basic_cg_identities_second_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 (scalarResponseIntegrand U a p q (scalarPerturbation u w 1 hu_int hw_int)) = volumeAverage U (scalarResponseIntegrand U a p q u) - 1 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a w)

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

theorem HCPolySupport.volumeAverage_scalarResponseIntegrand_eq_firstVariation_self_add_half_energy {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (u : AHarmonicFunction a U) (hlin_self : MeasureTheory.IntegrableOn (scalarFirstVariationIntegrand U a p q u u) U MeasureTheory.volume) (henergy : MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand a u) U MeasureTheory.volume) : volumeAverage U (scalarResponseIntegrand U a p q u) = volumeAverage U (scalarFirstVariationIntegrand U a p q u u) + 1 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a u)

theorem HCPolySupport.basic_cg_identities_energy_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) (hu_int : weakFluxIntegrable U a u) (hresp_u : MeasureTheory.IntegrableOn (scalarResponseIntegrand U a p q u) U MeasureTheory.volume) (hlin_self : MeasureTheory.IntegrableOn (scalarFirstVariationIntegrand U a p q u u) U MeasureTheory.volume) (henergy : MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand a u) U MeasureTheory.volume) : volumeAverage U (scalarResponseIntegrand U a p q u) = 1 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a u)

theorem HCPolySupport.responseJValueSet_mem {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) (u : AHarmonicFunction a U) : volumeAverage U (scalarResponseIntegrand U a p q u) ∈ responseJValueSet U p q a

theorem HCPolySupport.responseJValueSet_zero_mem {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) : 0 ∈ responseJValueSet U p q a

theorem HCPolySupport.responseJValueSet_nonempty {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) : (responseJValueSet U p q a).Nonempty

def HCPolySupport.responseJValueSetMeanZero {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) : Set ℝ

The set of averaged scalar response values attained by mean-zero harmonic functions.

Equations

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

theorem HCPolySupport.responseJValueSetMeanZero_mem {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} (u : AHarmonicFunctionMeanZero a U) : volumeAverage U (scalarResponseIntegrand U a p q u.toAHarmonicFunction) ∈ responseJValueSetMeanZero U p q a

theorem HCPolySupport.responseJValueSet_eq_responseJValueSetMeanZero {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : responseJValueSet U p q a = responseJValueSetMeanZero U p q a

theorem HCPolySupport.responseJ_eq_sSup_responseJValueSetMeanZero {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : ResponseJ U p q a = sSup (responseJValueSetMeanZero U p q a)

theorem HCPolySupport.responseJ_nonneg {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) : 0 ≤ ResponseJ U p q a

theorem HCPolySupport.responseJValueSet_smul_mem {d : ℕ} {U : Set (Vec d)} {p q : Vec d} {a : CoeffField d} {m : ℝ} (hm : m ∈ responseJValueSet U p q a) (c : ℝ) : c ^ 2 * m ∈ responseJValueSet U (c • p) (c • q) a

theorem HCPolySupport.responseJValueSet_homogeneous {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) {c : ℝ} (hc : c ≠ 0) : responseJValueSet U (c • p) (c • q) a = c ^ 2 • responseJValueSet U p q a

theorem HCPolySupport.responseJ_homogeneous {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) {c : ℝ} (hc : c ≠ 0) : ResponseJ U (c • p) (c • q) a = c ^ 2 * ResponseJ U p q a

theorem HCPolySupport.responseJ_homogeneous_zero_left {d : ℕ} (U : Set (Vec d)) (q : Vec d) (a : CoeffField d) {c : ℝ} (hc : c ≠ 0) : ResponseJ U 0 (c • q) a = c ^ 2 * ResponseJ U 0 q a

theorem HCPolySupport.responseJ_homogeneous_zero_right {d : ℕ} (U : Set (Vec d)) (p : Vec d) (a : CoeffField d) {c : ℝ} (hc : c ≠ 0) : ResponseJ U (c • p) 0 a = c ^ 2 * ResponseJ U p 0 a

theorem HCPolySupport.scalarResponseIntegrand_rescaleCoeff_sq {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (c : ℝ) (hc : c ≠ 0) (u : AHarmonicFunction a U) : scalarResponseIntegrand U (c ^ 2 • a) p q ((c⁻¹ • u).rescaleCoeff (c ^ 2)) = scalarResponseIntegrand U a (c • p) (c⁻¹ • q) u

theorem HCPolySupport.scalarResponseIntegrand_unscaleCoeff_sq {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (c : ℝ) (hc : c ≠ 0) (u : AHarmonicFunction (c ^ 2 • a) U) : scalarResponseIntegrand U (c ^ 2 • a) p q u = scalarResponseIntegrand U a (c • p) (c⁻¹ • q) (c • AHarmonicFunction.unscaleCoeff (c ^ 2) ⋯ u)

theorem HCPolySupport.responseJValueSet_rescaleCoeff_sq_eq {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) (c : ℝ) (hc : c ≠ 0) : responseJValueSet U p q (c ^ 2 • a) = responseJValueSet U (c • p) (c⁻¹ • q) a

theorem HCPolySupport.responseJ_homogeneous_coeffField_sq {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) (c : ℝ) (hc : c ≠ 0) : ResponseJ U p q (c ^ 2 • a) = ResponseJ U (c • p) (c⁻¹ • q) a

theorem HCPolySupport.responseJ_homogeneous_coeffField {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) {lam : ℝ} (hlam : 0 < lam) : ResponseJ U p q (lam • a) = ResponseJ U (√lam • p) ((√lam)⁻¹ • q) a

theorem HCPolySupport.scalarResponseIntegrand_integrableOn_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) : MeasureTheory.IntegrableOn (scalarResponseIntegrand U a p q u) U MeasureTheory.volume

theorem HCPolySupport.scalarResponseIntegrand_le_plainUpperBound_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (u : AHarmonicFunction a U) (x : Vec d) : x ∈ U → scalarResponseIntegrand U a p q u x ≤ lam⁻¹ * (Lam ^ 2 * vecNormSq p + vecNormSq q)

theorem HCPolySupport.responseJValueSet_bddAbove_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (p q : Vec d) : BddAbove (responseJValueSet U p q a)

theorem HCPolySupport.le_responseJ_of_mem_responseJValueSet_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (p q : Vec d) {m : ℝ} (hm : m ∈ responseJValueSet U p q a) : m ≤ ResponseJ U p q a

theorem HCPolySupport.responseJValueSet_bddAbove_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) {u : AHarmonicFunction a U} (hmax : IsResponseMaximizer U p q a u) : BddAbove (responseJValueSet U p q a)

theorem HCPolySupport.responseJValueSet_isGreatest_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) {u : AHarmonicFunction a U} (hmax : IsResponseMaximizer U p q a u) : IsGreatest (responseJValueSet U p q a) (volumeAverage U (scalarResponseIntegrand U a p q u))

theorem HCPolySupport.responseJ_eq_of_isResponseMaximizer {d : ℕ} (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) {u : AHarmonicFunction a U} (hmax : IsResponseMaximizer U p q a u) : ResponseJ U p q a = volumeAverage U (scalarResponseIntegrand U a p q u)

theorem HCPolySupport.responseJ_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.responseJ_second_variation_line_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) (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)) = ResponseJ U p q a - t ^ 2 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a w)

theorem HCPolySupport.responseJ_second_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 (scalarResponseIntegrand U a p q (scalarPerturbation u w 1 hu_int hw_int)) = ResponseJ U p q a - 1 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a w)

theorem HCPolySupport.responseJ_energy_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) (hu_int : weakFluxIntegrable U a u) (hresp_u : MeasureTheory.IntegrableOn (scalarResponseIntegrand U a p q u) U MeasureTheory.volume) (hlin_self : MeasureTheory.IntegrableOn (scalarFirstVariationIntegrand U a p q u u) U MeasureTheory.volume) (henergy : MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand a u) U MeasureTheory.volume) : ResponseJ U p q a = 1 / 2 * volumeAverage U (scalarVariationEnergyIntegrand a u)

theorem HCPolySupport.scalarVariationEnergyIntegrand_nonneg_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (w : AHarmonicFunction a U) (x : Vec d) : x ∈ U → 0 ≤ scalarVariationEnergyIntegrand a w x

theorem HCPolySupport.volumeAverage_scalarVariationEnergyIntegrand_nonneg_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (w : AHarmonicFunction a U) : 0 ≤ volumeAverage U (scalarVariationEnergyIntegrand a w)