Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.Correctors

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

Coarse Poincare with right-hand side

This file starts the deterministic Chapter-3 RHS development. The present pass only packages the local zero-trace corrector surface on one triadic cube, leaving the scale recurrence and iteration for downstream work.

theorem HCPolySupport.isFiniteMeasureVolumeMeasureOnCubeSet_rhs {d : ℕ} (Q : TriadicCube d) : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))

instance HCPolySupport.instIsFiniteMeasureVolumeMeasureOnCubeSet_rhs {d : ℕ} (Q : TriadicCube d) : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))

theorem HCPolySupport.openCubeSet_nonempty_rhs {d : ℕ} (Q : TriadicCube d) : (openCubeSet Q).Nonempty

structure HCPolySupport.ZeroTraceDirichletCorrectorData {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) : Type

A local zero-trace corrector on one cube for the weak equation - div (a grad rho) = div g.

• toH10 : H10Function (cubeSet Q)

  The zero-trace H¹ function solving the local Dirichlet corrector equation.

• weakSolution : IsZeroTraceDirichletRhsWeakSolution a (cubeSet Q) self.toH10 g

noncomputable def HCPolySupport.zeroTraceDirichletCorrectorDataOfClosureRealization {d : ℕ} (Q : TriadicCube d) {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 (cubeSet Q) g) (hRealize : PotentialSolenoidalL2Data.HasPotentialZeroTraceClosureRealization (cubeSet Q)) (hne : (cubeSet Q).Nonempty) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) : ZeroTraceDirichletCorrectorData Q a g

Package a local zero-trace corrector on one cube from the abstract Dirichlet RHS existence theorem.

Equations

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

theorem HCPolySupport.isZeroTraceDirichletRhsWeakSolution_cubeSet_of_openCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} {u : H10Function (openCubeSet Q)} (hu : IsZeroTraceDirichletRhsWeakSolution a (openCubeSet Q) u g) : IsZeroTraceDirichletRhsWeakSolution a (cubeSet Q) u.toCubeSet g

noncomputable def HCPolySupport.zeroTraceDirichletCorrectorDataOfCubeEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 (cubeSet Q) g) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) : ZeroTraceDirichletCorrectorData Q a g

Canonical local zero-trace corrector on the half-open cube, obtained by solving the Dirichlet problem on the corresponding open cube and transporting the weak formulation across the a.e.-equal cube realizations.

Equations

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

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.residualFlux_solenoidal {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (ρ : ZeroTraceDirichletCorrectorData Q a g) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hmem : MemVectorL2 (cubeSet Q) g) : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (ρ.toH10.grad x) - g x

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.exists_aHarmonicRemainder_of_potential_solenoidal {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (ρ : ZeroTraceDirichletCorrectorData Q a g) {u : Vec d → Vec d} (hu_potential : IsPotentialOn (cubeSet Q) u) (hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g x) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hmem : MemVectorL2 (cubeSet Q) g) : ∃ (w : AHarmonicFunction a (cubeSet Q)), ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.exists_aHarmonicRemainder_of_parent_potential_solenoidal {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} [NeZero d] {R : TriadicCube d} {n : ℕ} {lam Lam : ℝ} (ρ : ZeroTraceDirichletCorrectorData R a g) {u : Vec d → Vec d} (hu_potential : IsPotentialOn (cubeSet Q) u) (hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g x) (hR : R ∈ descendantsAtDepth Q n) (hEllR : IsEllipticFieldOn lam Lam (cubeSet R) a) (hu_memR : MemVectorL2 (cubeSet R) u) (hg_memR : MemVectorL2 (cubeSet R) g) : ∃ (w : AHarmonicFunction a (cubeSet R)), ∀ x ∈ cubeSet R, u x = w.toH1.grad x + ρ.toH10.grad x

Descendant-cube form of the local harmonic-remainder construction. The global PDE predicates on the parent half-open cube are restricted to R using the Sobolev cube bridge, and then the existing one-cube corrector lemma is applied on R.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.exists_harmonicCorrectorDecomposition {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} [NeZero d] {R : TriadicCube d} {n : ℕ} {lam Lam : ℝ} {u : Vec d → Vec d} (hu_potential : IsPotentialOn (cubeSet Q) u) (hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g x) (hR : R ∈ descendantsAtDepth Q n) (hEllR : IsEllipticFieldOn lam Lam (cubeSet R) a) (hu_memR : MemVectorL2 (cubeSet R) u) (hg_memR : MemVectorL2 (cubeSet R) g) : ∃ (ρ : ZeroTraceDirichletCorrectorData R a g) (w : AHarmonicFunction a (cubeSet R)), ∀ x ∈ cubeSet R, u x = w.toH1.grad x + ρ.toH10.grad x

Fully constructed descendant-cube corrector and harmonic remainder from parent potential/solenoidal PDE data. The zero-trace corrector is built on the open cube and transported to the half-open cube, so callers no longer need a separate realization hypothesis on cubeSet R.