Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.CoarseFluxResponse.RHSConstantApexZeroDirichletEnergy

Coarse-graining support: #

Support.Deterministic.CoarseFluxResponse.RHSConstantApexZeroDirichletEnergy

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

Zero-Dirichlet energy input for the one-cube RHS coarse-flux response apex #

This leaf records the zero-trace energy envelope and the Poincare scalar budget used by the corrected zero-Dirichlet apex route.

source
noncomputable def HCPolySupport.zeroTraceDirichletPoincareScalarBudget {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (g : Vec d → Vec d) :
ℝ

Displayed Poincare scalar budget after the zero-trace energy envelope has been inserted.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.zeroTraceDirichletEnergyEnvelope_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g : Vec d → Vec d) (hs : 0 < s) :
    0 ≤ zeroTraceDirichletEnergyEnvelope Q a s g
    source
    theorem HCPolySupport.zeroTraceDirichletPoincareScalarBudget_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (g : Vec d → Vec d) (hs : 0 < s) :
    0 ≤ zeroTraceDirichletPoincareScalarBudget Q a a0 s g
    source
    theorem HCPolySupport.zeroTraceDirichletPoincareScalarBudget_le_const_mul_correctionBound_sq_of_component_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (C s : ℝ) (g : Vec d → Vec d) {Benergy Bforce : ℝ} (henergy : matNorm a0 ^ 2 * (250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * zeroTraceDirichletEnergyEnvelope Q a s g) ≤ Benergy) (hforce : matNorm a0 ^ 2 * (15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) ≤ Bforce) (hsum : Benergy + Bforce ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2) :
    zeroTraceDirichletPoincareScalarBudget Q a a0 s g ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2

    Component bounds imply the named Poincare scalar budget inequality.

    source
    theorem HCPolySupport.matNorm_sq_mul_fluxPoincareRadicand_le_zeroTraceDirichletPoincareScalarBudget {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (g gradV : Vec d → Vec d) (hs : 0 < s) (henergy : cubeAverage Q (coefficientEnergyDensity a gradV) ≤ zeroTraceDirichletEnergyEnvelope Q a s g) :
    matNorm a0 ^ 2 * coarseFluxResponseRHSPoincareExpandedRadicand Q a s g gradV ≤ zeroTraceDirichletPoincareScalarBudget Q a a0 s g

    The matrix-weighted depth-zero Poincare expanded radicand is controlled by the named zero-trace Poincare scalar budget once the correction energy is bounded by the zero-trace energy envelope.

    source
    theorem HCPolySupport.matNorm_sq_mul_fluxPoincareRadicand_le_const_mul_correctionBound_sq_of_envelope {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (C : ℝ) {s : ℝ} (g gradV : Vec d → Vec d) (hs : 0 < s) (henergy : cubeAverage Q (coefficientEnergyDensity a gradV) ≤ zeroTraceDirichletEnergyEnvelope Q a s g) (hbudget : zeroTraceDirichletPoincareScalarBudget Q a a0 s g ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2) :
    matNorm a0 ^ 2 * coarseFluxResponseRHSPoincareExpandedRadicand Q a s g gradV ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2

    Poincare square-radicand closure from the named zero-trace scalar budget.

    source
    theorem HCPolySupport.matNorm_mul_fluxPoincareBound_le_const_mul_correctionBound_of_correctionBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {C s : ℝ} (g gradV : Vec d → Vec d) (hC_nonneg : 0 ≤ C) (hs : 0 < s) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a gradV)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (henergy : cubeAverage Q (coefficientEnergyDensity a gradV) ≤ zeroTraceDirichletEnergyEnvelope Q a s g) (hbudget : zeroTraceDirichletPoincareScalarBudget Q a a0 s g ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2) :
    matNorm a0 * coarseFluxResponseRHSPoincareExpandedBound Q a s g gradV ≤ C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

    Poincare square-root absorption from the zero-trace energy envelope and the named Poincare scalar budget.