Coarse-graining support: Support.Deterministic.CoarseFluxResponse.Response

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

def HCPolySupport.CubeAverageFluxResponseControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (defect : Vec d → Vec d) (energy : Vec d → ℝ) : Prop

Descendant cube-average control for a flux-defect field by the local normalized block response and a scalar energy density.

Equations

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

theorem HCPolySupport.cubeAverageFluxResponseControl_of_descendantScalarCanonicalFluxDefectData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (defect : Vec d → Vec d) (energy : Vec d → ℝ) {lam0 Lam0 : ℝ} (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hdesc : DescendantScalarCanonicalFluxDefectData Q a a0 defect energy) : CubeAverageFluxResponseControl Q a a0 defect energy

theorem HCPolySupport.cubeAverageFluxResponseControl_of_aHarmonicFunction {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {lam Lam lam0 Lam0 : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (u : AHarmonicFunction a (cubeSet Q)) : CubeAverageFluxResponseControl Q a a0 (fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) - matVecMul a0 (u.toH1.grad x)) (scalarVariationEnergyIntegrand a u)

Direct descendant-average control for the actual flux defect of one harmonic field on cubeSet Q.

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_le_fluxResponseEnergy {d : ℕ} {Q : TriadicCube d} (a : CoeffField d) (a0 : Mat d) (defect : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hresp : CubeAverageFluxResponseControl Q a a0 defect energy) (j : ℕ) : cubeBesovNegativeVectorDepthAverage Q defect j ≤ 4 * matNorm a0 * maxDescendantNormalizedBlockResponseAtScale Q (Q.scale - ↑j) a a0 * cubeAverage Q energy

theorem HCPolySupport.coarseFluxResponse_qone_partialSeminorm_le_of_cubeAverageFluxResponseControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (hs : 0 < s) (defect : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hresp : CubeAverageFluxResponseControl Q a a0 defect energy) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) (N : ℕ) : cubeBesovNegativeVectorPartialSeminorm Q s N defect ≤ (geometricDiscount s 1)⁻¹ * HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 * (√(4 * matNorm a0) * √(cubeAverage Q energy))

Finite-depth q = 1 deterministic coarse flux-response bound under an explicit descendant-local one-cube response bound.

theorem HCPolySupport.coarseFluxResponse_qone_of_cubeAverageFluxResponseControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (hs : 0 < s) (defect : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hresp : CubeAverageFluxResponseControl Q a a0 defect energy) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : cubeBesovNegativeVectorSeminorm Q s defect ≤ (geometricDiscount s 1)⁻¹ * HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 * (√(4 * matNorm a0) * √(cubeAverage Q energy))

Note-normalized q = 1 deterministic coarse flux-response inequality under an explicit descendant-local one-cube response bound.

theorem HCPolySupport.coarseFluxResponse_qone_of_descendantScalarCanonicalFluxDefectData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (hs : 0 < s) (defect : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) {lam0 Lam0 : ℝ} (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hdesc : DescendantScalarCanonicalFluxDefectData Q a a0 defect energy) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : cubeBesovNegativeVectorSeminorm Q s defect ≤ (geometricDiscount s 1)⁻¹ * HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 * (√(4 * matNorm a0) * √(cubeAverage Q energy))

Note-facing q = 1 deterministic coarse flux-response inequality for the actual defect field, packaged directly from descendant scalar canonical maximizer data.

theorem HCPolySupport.coarseFluxResponse_qone_of_descendantScalarCanonicalFluxDefectAHarmonicData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (hs : 0 < s) {lam Lam lam0 Lam0 : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (u : AHarmonicFunction a (cubeSet Q)) (hdesc : DescendantScalarCanonicalFluxDefectAHarmonicData Q a a0 u) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : (cubeBesovNegativeVectorSeminorm Q s fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) - matVecMul a0 (u.toH1.grad x)) ≤ (geometricDiscount s 1)⁻¹ * HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 * (√(4 * matNorm a0) * √(cubeAverage Q (scalarVariationEnergyIntegrand a u)))

Note-facing q = 1 deterministic coarse flux-response inequality for the actual defect field of one harmonic function on cubeSet Q.

theorem HCPolySupport.coarseFluxResponse_qone_partialSeminorm_le_of_aHarmonicFunction {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (hs : 0 < s) {lam Lam lam0 Lam0 : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (u : AHarmonicFunction a (cubeSet Q)) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) (N : ℕ) : (cubeBesovNegativeVectorPartialSeminorm Q s N fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) - matVecMul a0 (u.toH1.grad x)) ≤ (geometricDiscount s 1)⁻¹ * HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 * (√(4 * matNorm a0) * √(cubeAverage Q (scalarVariationEnergyIntegrand a u)))

Finite-depth q = 1 deterministic coarse flux-response bound for the actual defect field of one harmonic function on cubeSet Q, with no separate descendant witness package.

theorem HCPolySupport.coarseFluxResponse_qone_of_aHarmonicFunction {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (hs : 0 < s) {lam Lam lam0 Lam0 : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (u : AHarmonicFunction a (cubeSet Q)) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : (cubeBesovNegativeVectorSeminorm Q s fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) - matVecMul a0 (u.toH1.grad x)) ≤ (geometricDiscount s 1)⁻¹ * HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 * (√(4 * matNorm a0) * √(cubeAverage Q (scalarVariationEnergyIntegrand a u)))

Note-facing q = 1 deterministic coarse flux-response inequality for the actual defect field of one harmonic function on cubeSet Q, with no separate descendant witness package.