Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.CoarseFluxResponse.RHSConstantApexZeroDirichletCorrectedWeakFlux

Coarse-graining support: #

Support.Deterministic.CoarseFluxResponse.RHSConstantApexZeroDirichletCorrectedWeakFlux

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

Corrected zero-Dirichlet weak-flux component route #

This leaf is the live bridge from the zero-Dirichlet apex to the corrected Lambda * lambda^{-1} weak-flux scalar surface. It uses the corrector-energy recurrence directly, avoiding the older absorbed forcing route whose displayed force term has Lambda^2 units.

source
theorem HCPolySupport.ZeroTraceDirichletCorrectorData.isEllipticFieldOn_descendant_cubeSet_of_parent {d : ℕ} {Q R : TriadicCube d} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hRdesc : ∃ (n : ℕ), R ∈ descendantsAtDepth Q n) :
IsEllipticFieldOn lam Lam (cubeSet R) a
source
noncomputable def HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceFluxApexDisplayScale (d : ℕ) (s : ℝ) :
ℝ

Displayed dimensional scale in the corrected zero-Dirichlet scalar budgets.

Equations
Instances For
    source
    noncomputable def HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceFluxApexConstant (d : ℕ) (s : ℝ) :
    ℝ

    Fixed internal scalar constant for the corrected zero-Dirichlet apex route.

    Equations
    Instances For
      source
      theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletCorrectedWeakFluxApexDisplayScale_nonneg (d : ℕ) (s : ℝ) :
      0 ≤ zeroTraceFluxApexDisplayScale d s
      source
      theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceFluxApexConstant_nonneg (d : ℕ) (s : ℝ) :
      0 ≤ zeroTraceFluxApexConstant d s
      source
      theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletCorrectedWeakFluxApexPoincareConstant_sq (d : ℕ) (s : ℝ) :
      177500 * zeroTraceFluxApexDisplayScale d s ^ 2 ≤ zeroTraceFluxApexConstant d s ^ 2
      source
      theorem HCPolySupport.ZeroTraceDirichletCorrectorData.negativeBesovFluxAverage_matVecMul_grad_le_sqrt_correctorEnergyComponents {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q a g) (s : ℝ) {Bcorr lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (m : ℕ) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (z : TriadicCube d → Vec d → Vec d) (hzdecomp : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, ∃ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g) (w0 : AHarmonicFunction a (cubeSet R)), (z R = fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ∧ ∀ x ∈ cubeSet R, ρ.toH10.grad x = w0.toH1.grad x + z R x) (hcorr : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalCorrectorEnergyErrorAverage Q a z s (m + k) ≤ Bcorr) :
      localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (ρ.toH10.grad x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * ((weakFluxRHSWeightedCoefficientEnergyBase Q a (fun (x : Vec d) => ρ.toH10.grad x) s + Bcorr) * (1 - Real.rpow 3 (-s))⁻¹))

      Localized zero-Dirichlet weak-flux estimate through the corrector-energy component iteration.

      The u coefficient-energy component is discharged internally from the coefficient-localization bound; hcorr is the remaining Neumann-corrector component input. No Lambda^2 absorbed-force estimate is used here.