Coarse-graining support: Support.CoarseGraining.BlockResponse.Perturbation.Integrand #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
BlockResponse perturbation -- integrand algebra and plain upper bound #
Integrand basics (zero / smul / add), the first-variation and variation- energy integrands, the plainUpperBound upper bound under IsEllipticFieldOn, and the resulting blockJValueSet / blockJ upper bounds.
theorem
HCPolySupport.blockResponse_integrand_smul
{d : ℕ}
(a : CoeffField d)
(P Q : BlockVec d)
(c : ℝ)
(X : BlockState d)
:
blockResponseIntegrand a P Q (c • X) = fun (x : Vec d) =>
-c ^ 2 * blockEnergyDensity a X x - c * blockVecDot P (blockMatVecMul (blockCoeffField a x) (X.eval x)) + c * blockVecDot Q (X.eval x)
theorem
HCPolySupport.blockResponse_integrand_smul_data_state
{d : ℕ}
(a : CoeffField d)
(P Q : BlockVec d)
(c : ℝ)
(X : BlockState d)
:
blockResponseIntegrand a (c • P) (c • Q) (c • X) = fun (x : Vec d) => c ^ 2 * blockResponseIntegrand a P Q X x
noncomputable def
HCPolySupport.blockFirstVariationIntegrand
{d : ℕ}
(a : CoeffField d)
(P Q : BlockVec d)
(X Y : BlockState d)
:
The linear term in the doubled response functional at base state X
in the direction Y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
HCPolySupport.blockVariationEnergyIntegrand
{d : ℕ}
(a : CoeffField d)
(Y : BlockState d)
:
The quadratic energy term governing the second variation of the doubled response functional.
Equations
Instances For
@[simp]
theorem
HCPolySupport.blockVariationEnergyIntegrand_eq_blockEnergyDensity
{d : ℕ}
(a : CoeffField d)
(Y : BlockState d)
:
theorem
HCPolySupport.blockFirstVariationIntegrand_add_direction
{d : ℕ}
(a : CoeffField d)
(P Q : BlockVec d)
(X Y Z : BlockState d)
:
blockFirstVariationIntegrand a P Q X (Y + Z) = fun (x : Vec d) =>
blockFirstVariationIntegrand a P Q X Y x + blockFirstVariationIntegrand a P Q X Z x
theorem
HCPolySupport.blockFirstVariationIntegrand_smul_direction
{d : ℕ}
(a : CoeffField d)
(P Q : BlockVec d)
(X Y : BlockState d)
(c : ℝ)
:
blockFirstVariationIntegrand a P Q X (c • Y) = fun (x : Vec d) => c * blockFirstVariationIntegrand a P Q X Y x
theorem
HCPolySupport.blockResponse_integrand_add_smul_eq_firstVariation_sub_energy
{d : ℕ}
(a : CoeffField d)
(P Q : BlockVec d)
(X Y : BlockState d)
(c : ℝ)
:
blockResponseIntegrand a P Q (X + c • Y) = fun (x : Vec d) =>
blockResponseIntegrand a P Q X x + c * blockFirstVariationIntegrand a P Q X Y x - c ^ 2 * blockVariationEnergyIntegrand a Y x
theorem
HCPolySupport.blockResponse_integrand_add_eq_firstVariation_sub_energy
{d : ℕ}
(a : CoeffField d)
(P Q : BlockVec d)
(X Y : BlockState d)
:
blockResponseIntegrand a P Q (X + Y) = fun (x : Vec d) =>
blockResponseIntegrand a P Q X x + blockFirstVariationIntegrand a P Q X Y x - blockVariationEnergyIntegrand a Y x
theorem
HCPolySupport.volumeAverage_blockResponse_integrand_add_smul_eq_firstVariation_sub_energy
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
(P Q : BlockVec d)
(X Y : BlockState d)
(c : ℝ)
(hresp : MeasureTheory.IntegrableOn (blockResponseIntegrand a P Q X) U MeasureTheory.volume)
(hlin : MeasureTheory.IntegrableOn (blockFirstVariationIntegrand a P Q X Y) U MeasureTheory.volume)
(henergy : MeasureTheory.IntegrableOn (blockVariationEnergyIntegrand a Y) U MeasureTheory.volume)
:
volumeAverage U (blockResponseIntegrand a P Q (X + c • Y)) = volumeAverage U (blockResponseIntegrand a P Q X) + c * volumeAverage U (blockFirstVariationIntegrand a P Q X Y) - c ^ 2 * volumeAverage U (blockVariationEnergyIntegrand a Y)
theorem
HCPolySupport.volumeAverage_blockResponse_integrand_add_eq_firstVariation_sub_energy
{d : ℕ}
{U : Set (Vec d)}
(a : CoeffField d)
(P Q : BlockVec d)
(X Y : BlockState d)
(hresp : MeasureTheory.IntegrableOn (blockResponseIntegrand a P Q X) U MeasureTheory.volume)
(hlin : MeasureTheory.IntegrableOn (blockFirstVariationIntegrand a P Q X Y) U MeasureTheory.volume)
(henergy : MeasureTheory.IntegrableOn (blockVariationEnergyIntegrand a Y) U MeasureTheory.volume)
:
volumeAverage U (blockResponseIntegrand a P Q (X + Y)) = volumeAverage U (blockResponseIntegrand a P Q X) + volumeAverage U (blockFirstVariationIntegrand a P Q X Y) - volumeAverage U (blockVariationEnergyIntegrand a Y)
theorem
HCPolySupport.volumeAverage_blockFirstVariationIntegrand_zero_data_eq_zero_of_mem_responseSpace
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{X Y : BlockState d}
(hX : BlockResponseSpace a U X)
(hY : IsBlockTestOn U Y)
:
noncomputable def
HCPolySupport.blockResponsePlainUpperBound
{d : ℕ}
(lam Lam : ℝ)
(P Q : BlockVec d)
:
An explicit upper bound for the block response density in terms of the ellipticity parameters
and the squared norms of P and Q.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.blockResponseIntegrand_le_plainUpperBound_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(P Q : BlockVec d)
(X : BlockState d)
(x : Vec d)
:
x ∈ U → blockResponseIntegrand a P Q X x ≤ blockResponsePlainUpperBound lam Lam P Q
theorem
HCPolySupport.volumeAverage_blockResponseIntegrand_le_plainUpperBound_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(P Q : BlockVec d)
(X : BlockState d)
(hInt : MeasureTheory.IntegrableOn (blockResponseIntegrand a P Q X) U MeasureTheory.volume)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
:
theorem
HCPolySupport.blockJValueSet_bddAbove_of_isEllipticFieldOn_of_integrableOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(P Q : BlockVec d)
(hInt :
∀ (X : BlockState d),
BlockResponseSpace a U X → MeasureTheory.IntegrableOn (blockResponseIntegrand a P Q X) U MeasureTheory.volume)
:
BddAbove (blockJValueSet U P Q a)
theorem
HCPolySupport.le_blockJ_of_mem_blockJValueSet_of_isEllipticFieldOn_of_integrableOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(P Q : BlockVec d)
(hInt :
∀ (X : BlockState d),
BlockResponseSpace a U X → MeasureTheory.IntegrableOn (blockResponseIntegrand a P Q X) U MeasureTheory.volume)
{m : ℝ}
(hm : m ∈ blockJValueSet U P Q a)
:
theorem
HCPolySupport.blockJValueSet_bddAbove_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(P Q : BlockVec d)
:
BddAbove (blockJValueSet U P Q a)
theorem
HCPolySupport.le_blockJ_of_mem_blockJValueSet_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(P Q : BlockVec d)
{m : ℝ}
(hm : m ∈ blockJValueSet U P Q a)
:
theorem
HCPolySupport.blockJ_le_plainUpperBound_of_isEllipticFieldOn_of_integrableOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(P Q : BlockVec d)
(hInt :
∀ (X : BlockState d),
BlockResponseSpace a U X → MeasureTheory.IntegrableOn (blockResponseIntegrand a P Q X) U MeasureTheory.volume)
:
theorem
HCPolySupport.blockJ_le_plainUpperBound_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hU : MeasurableSet U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(P Q : BlockVec d)
: