Coarse-graining support: Support.Deterministic.WeakFluxRHS.NeumannCorrector

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

Mean-zero Neumann correctors for the RHS weak-flux lane

This file packages the local correction used in Section 3.2.3. The key feature, absent from the zero-trace Dirichlet corrector, is that the Neumann residual has zero normal trace; on a cube this forces the residual flux average to vanish.

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

noncomputable def HCPolySupport.cubeSetH1CoerciveEstimate {d : ℕ} (Q : TriadicCube d) : H1CoerciveEstimate (cubeSet Q)

The half-open triadic cube inherits the mean-zero H¹ coercive estimate from the corresponding open cube, since the two realizations differ only by a Lebesgue-null boundary.

Equations

• HCPolySupport.cubeSetH1CoerciveEstimate Q = { constantValue := (HCPolySupport.h1CoerciveEstimateOfOpenBoundedConvexDomain ⋯).constantValue, constant_nonneg := ⋯, bound := ⋯ }

theorem HCPolySupport.cubeAverageVec_centered_eq_zero {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) (hg : MemVectorL2 (cubeSet Q) g) : (cubeAverageVec Q fun (x : Vec d) => g x - cubeAverageVec Q g) = 0

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

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

• toH1MeanZero : H1MeanZeroFunction (cubeSet Q)

  The mean-zero H¹ function solving the local Neumann corrector equation.

• weakSolution : IsMeanZeroNeumannRhsWeakSolution a (cubeSet Q) self.toH1MeanZero g

noncomputable def HCPolySupport.meanZeroNeumannCorrectorDataOfH1CoerciveEstimate {d : ℕ} (Q : TriadicCube d) {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 (cubeSet Q) g) (hC : H1CoerciveEstimate (cubeSet Q)) (hne : (cubeSet Q).Nonempty) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) : MeanZeroNeumannCorrectorData Q a g

Package a local mean-zero Neumann corrector from a supplied coercive estimate on the half-open cube. A later cube-realization bridge can discharge the coercive input from the open-cube Poincare estimate.

Equations

• HCPolySupport.meanZeroNeumannCorrectorDataOfH1CoerciveEstimate Q hg hC hne hEll = { toH1MeanZero := HCPolySupport.H1MeanZeroFunction.coeffGradientProblemSolution hg hC hne hEll, weakSolution := ⋯ }

theorem HCPolySupport.MeanZeroNeumannCorrectorData.residualFlux_zeroNormalTrace {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (ω : MeanZeroNeumannCorrectorData Q a g) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hg : MemVectorL2 (cubeSet Q) g) : IsSolenoidalZeroNormalTraceOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (ω.toH1MeanZero.toH1Function.grad x) - g x

The Neumann-corrector residual has zero normal trace.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.cubeAverageVec_residualFlux_eq_zero {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (ω : MeanZeroNeumannCorrectorData Q a g) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hg : MemVectorL2 (cubeSet Q) g) : (cubeAverageVec Q fun (x : Vec d) => matVecMul (a x) (ω.toH1MeanZero.toH1Function.grad x) - g x) = 0

The averaged residual flux of a Neumann corrector vanishes on a cube.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.cubeAverageVec_flux_eq_zero_of_cubeAverageVec_rhs_eq_zero {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (ω : MeanZeroNeumannCorrectorData Q a g) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hg : MemVectorL2 (cubeSet Q) g) (havg_g : cubeAverageVec Q g = 0) : (cubeAverageVec Q fun (x : Vec d) => matVecMul (a x) (ω.toH1MeanZero.toH1Function.grad x)) = 0

If the Neumann RHS is centered, then the corrector flux itself has zero cube average, the algebraic cancellation used in manuscript Section 3.2.3.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.cubeAverageVec_flux_eq_zero_of_centered_rhs {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hg : MemVectorL2 (cubeSet Q) g) : (cubeAverageVec Q fun (x : Vec d) => matVecMul (a x) (ω.toH1MeanZero.toH1Function.grad x)) = 0

Centered-RHS form of the zero-average corrector-flux cancellation.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.exists_aHarmonicRemainder_of_potential_solenoidal_centered {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q 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) (hg : MemVectorL2 (cubeSet Q) g) : ∃ (w : AHarmonicFunction a (cubeSet Q)), ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x

Correcting a potential weak solution by the mean-zero Neumann solution with centered RHS produces an a-harmonic remainder on the cube.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.cubeAverageVec_flux_eq_harmonicRemainderFlux_of_centered_rhs {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (w : AHarmonicFunction a (cubeSet Q)) {u : Vec d → Vec d} (hdecomp : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu_mem : MemVectorL2 (cubeSet Q) u) (hg : MemVectorL2 (cubeSet Q) g) : (cubeAverageVec Q fun (x : Vec d) => matVecMul (a x) (u x)) = cubeAverageVec Q fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)

The zero average of the centered Neumann corrector flux lets the local flux average of the original field be replaced by the harmonic remainder's flux average.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.cubeAverage_coefficientEnergyDensity_eq_centered_rhs_pairing {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) : cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) = cubeAverage Q fun (x : Vec d) => vecDot (g x - cubeAverageVec Q g) (ω.toH1MeanZero.toH1Function.grad x)

Cube-average form of the Neumann corrector energy identity obtained by testing the centered corrector equation with the corrector itself.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.cubeAverage_coefficientEnergyDensity_harmonic_le_two_mul_add {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) {u : Vec d → Vec d} (w : AHarmonicFunction a (cubeSet Q)) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) (hu : MemVectorL2 (cubeSet Q) u) : cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x) ≤ 2 * cubeAverage Q (coefficientEnergyDensity a u) + 2 * cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x)

Coefficient-energy version of the split w = u - grad omega for the mean-zero Neumann corrector.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.exists_aHarmonicRemainder_of_parent_potential_solenoidal_centered {d : ℕ} {a : CoeffField d} {g : Vec d → Vec d} [NeZero d] {P R : TriadicCube d} {n : ℕ} {lam Lam : ℝ} (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g) {u : Vec d → Vec d} (hu_potential : IsPotentialOn (cubeSet P) u) (hu_residual : IsSolenoidalOn (cubeSet P) fun (x : Vec d) => matVecMul (a x) (u x) - g x) (hR : R ∈ descendantsAtDepth P 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 + ω.toH1MeanZero.toH1Function.grad x

Descendant-cube form of the centered Neumann corrector harmonic-remainder construction. The parent potential/solenoidal predicates are restricted to the descendant cube, matching the local step used in the weak-flux recurrence.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.exists_centeredCorrector_harmonicRemainder_of_parentCoercivity {d : ℕ} {a : CoeffField d} {g : Vec d → Vec d} [NeZero d] {P R : TriadicCube d} {n : ℕ} {lam Lam : ℝ} {u : Vec d → Vec d} (hu_potential : IsPotentialOn (cubeSet P) u) (hu_residual : IsSolenoidalOn (cubeSet P) fun (x : Vec d) => matVecMul (a x) (u x) - g x) (hR : R ∈ descendantsAtDepth P n) (hEllR : IsEllipticFieldOn lam Lam (cubeSet R) a) (hu_memR : MemVectorL2 (cubeSet R) u) (hg_memR : MemVectorL2 (cubeSet R) g) (hC : H1CoerciveEstimate (cubeSet R)) : ∃ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g) (w : AHarmonicFunction a (cubeSet R)), ∀ x ∈ cubeSet R, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x

Fully constructed descendant-cube centered Neumann corrector and harmonic remainder from parent potential/solenoidal PDE data, assuming the local mean-zero coercive estimate on the descendant half-open cube.