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

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

theorem HCPolySupport.MeanZeroNeumannCorrectorData.sq_negativeBesovSeminormTwo_flux_le_descendantMean_add_harmonic_energy {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)) (s : ℝ) (hs : 0 < s) (energy : Vec d → ℝ) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu_mem : MemVectorL2 (cubeSet Q) u) (hg : MemVectorL2 (cubeSet Q) g) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hflux : CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) energy) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) (huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) (hchildBdd : ∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u x))) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + (geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a * cubeAverage Q energy

Full-seminorm form of the weak-flux local step. This turns the finite-depth local recurrence from FluxStepping into the one-step recurrence for the full q = 2 negative seminorm, assuming the child full seminorms bound their finite partials.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.sq_negativeBesovSeminormTwo_flux_le_childMean_add_energy_add_correctorEnergy {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)) (s : ℝ) (hs : 0 < s) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu_mem : MemVectorL2 (cubeSet Q) u) (hg : MemVectorL2 (cubeSet Q) g) (hflux : CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) (coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x)) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) (huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) (hchildBdd : ∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u x))) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) * cubeAverage Q (coefficientEnergyDensity a u) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) * cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x)

Coefficient-energy version of the weak-flux local step after splitting the harmonic remainder energy into the original field and the mean-zero Neumann corrector.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.sq_negativeBesovSeminormTwo_flux_le_childMean_add_energy_add_correction {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)) (s : ℝ) (hs : 0 < s) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu_mem : MemVectorL2 (cubeSet Q) u) (hg_mem : MemVectorL2 (cubeSet Q) g) (hflux : CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) (coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x)) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) (huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) (hchildBdd : ∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u x))) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u)) (hwBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g)) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) * cubeAverage Q (coefficientEnergyDensity a u) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) * (↑d * (3 ^ (↑d + s) * (√2 * (cubeBesovNegativeVectorSeminormTwo Q s u + cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => w.toH1.grad x)) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g))

Full-seminorm local recurrence with the Neumann-corrector energy replaced by the sharp centered Besov product bound.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.sq_negativeBesovSeminormTwo_flux_le_childMean_add_energy_add_YoungError {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)) (s : ℝ) {η : ℝ} (hs : 0 < s) (hη : 0 < η) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu_mem : MemVectorL2 (cubeSet Q) u) (hg_mem : MemVectorL2 (cubeSet Q) g) (hflux : CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) (coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x)) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) (huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) (hchildBdd : ∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u x))) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u)) (hwBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g)) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) * cubeAverage Q (coefficientEnergyDensity a u) + η * cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 + η * (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => w.toH1.grad x) ^ 2 + 2 * η⁻¹ * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a * (↑d * (3 ^ (↑d + s) * √2)) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g) ^ 2

Full-seminorm local recurrence with the short corrector product absorbed into quadratic u, harmonic-remainder, and forcing terms.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.exists_centeredCorrector_aHarmonicRemainder_fluxSeminormStepEnergy {d : ℕ} {a : CoeffField d} [NeZero d] {P R : TriadicCube d} {n : ℕ} {lam Lam s : ℝ} {u g : Vec d → Vec d} (hs : 0 < s) (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) ∧ ∀ (energy : Vec d → ℝ), (∀ x ∈ cubeSet R, 0 ≤ energy x) → MeasureTheory.IntegrableOn energy (cubeSet R) MeasureTheory.volume → CubeAverageFluxEnergyControl R a (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) energy → (Summable fun (m : ℕ) => geometricWeight s 2 m * maxDescendantBBlockNormAtScale R (R.scale - ↑m) a) → (∀ S ∈ descendantsAtDepth R 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo S s N fun (x : Vec d) => matVecMul (a x) (u x))) → (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + (geometricDiscount s 2)⁻¹ * LambdaSq R s (MultiscaleExponent.finite 2) a * cubeAverage R energy

Descendant-cube full-seminorm recurrence from parent potential/solenoidal weak-flux data. This is the local iteration-facing version of the centered Neumann-corrector construction.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.exists_centeredCorrector_aHarmonicRemainder_fluxSeminormStepCoeffEnergy {d : ℕ} {a : CoeffField d} [NeZero d] {P R : TriadicCube d} {n : ℕ} {lam Lam s : ℝ} {u g : Vec d → Vec d} (hs : 0 < s) (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) ∧ (CubeAverageFluxEnergyControl R a (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) (coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x) → (Summable fun (m : ℕ) => geometricWeight s 2 m * maxDescendantBBlockNormAtScale R (R.scale - ↑m) a) → (∀ S ∈ descendantsAtDepth R 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo S s N fun (x : Vec d) => matVecMul (a x) (u x))) → (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq R s (MultiscaleExponent.finite 2) a) * cubeAverage R (coefficientEnergyDensity a u) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq R s (MultiscaleExponent.finite 2) a) * cubeAverage R (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x))

Descendant-cube local recurrence with the harmonic flux energy split into the original-field energy and the mean-zero Neumann-corrector energy.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.exists_centeredCorrector_aHarmonicRemainder_of_coarseData {d : ℕ} {a : CoeffField d} [NeZero d] {P R : TriadicCube d} {n : ℕ} {lam Lam s : ℝ} {u g : Vec d → Vec d} (hs : 0 < s) (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)) (hDataR : OpenCubeDescendantDeterministicCoarseData R a) (hsum : Summable fun (m : ℕ) => geometricWeight s 2 m * maxDescendantBBlockNormAtScale R (R.scale - ↑m) a) (hchildBdd : ∀ S ∈ descendantsAtDepth R 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo S s N fun (x : Vec d) => matVecMul (a x) (u x))) : ∃ (ω : 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) ∧ (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq R s (MultiscaleExponent.finite 2) a) * cubeAverage R (coefficientEnergyDensity a u) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq R s (MultiscaleExponent.finite 2) a) * cubeAverage R (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x)

Descendant-cube coefficient-energy recurrence with harmonic flux control supplied by deterministic coarse data.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.exists_centeredCorrector_aHarmonicRemainder_fluxSeminormStepShortTerm {d : ℕ} {a : CoeffField d} [NeZero d] {P R : TriadicCube d} {n : ℕ} {lam Lam s : ℝ} {u g : Vec d → Vec d} (hs : 0 < s) (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)) (hDataR : OpenCubeDescendantDeterministicCoarseData R a) (hsum : Summable fun (m : ℕ) => geometricWeight s 2 m * maxDescendantBBlockNormAtScale R (R.scale - ↑m) a) (hchildBdd : ∀ S ∈ descendantsAtDepth R 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo S s N fun (x : Vec d) => matVecMul (a x) (u x))) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : Vec d) => g x - cubeAverageVec R g)) : ∃ (ω : 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) ∧ (BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => w.toH1.grad x) → (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq R s (MultiscaleExponent.finite 2) a) * cubeAverage R (coefficientEnergyDensity a u) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq R s (MultiscaleExponent.finite 2) a) * (↑d * (3 ^ (↑d + s) * (√2 * (cubeBesovNegativeVectorSeminormTwo R s u + cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => w.toH1.grad x)) * cubeBesovPositiveVectorSeminormTwo R s fun (x : Vec d) => g x - cubeAverageVec R g)))

Descendant-cube coefficient-energy recurrence with the corrector term replaced by the short centered Besov product bound. The harmonic seminorm boundedness is returned as an input to the packaged step because the harmonic remainder is created by the local Neumann construction.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.exists_centeredCorrector_harmonicRemainder_fluxStepBound {d : ℕ} {a : CoeffField d} [NeZero d] {P R : TriadicCube d} {n : ℕ} {lam Lam s η : ℝ} {u g : Vec d → Vec d} (hs : 0 < s) (hη : 0 < η) (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)) (hDataR : OpenCubeDescendantDeterministicCoarseData R a) (hsum : Summable fun (m : ℕ) => geometricWeight s 2 m * maxDescendantBBlockNormAtScale R (R.scale - ↑m) a) (hchildBdd : ∀ S ∈ descendantsAtDepth R 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo S s N fun (x : Vec d) => matVecMul (a x) (u x))) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : Vec d) => g x - cubeAverageVec R g)) : ∃ (ω : 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) ∧ (BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => w.toH1.grad x) → (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq R s (MultiscaleExponent.finite 2) a) * cubeAverage R (coefficientEnergyDensity a u) + η * cubeBesovNegativeVectorSeminormTwo R s u ^ 2 + η * (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => w.toH1.grad x) ^ 2 + 2 * η⁻¹ * ((geometricDiscount s 2)⁻¹ * LambdaSq R s (MultiscaleExponent.finite 2) a * (↑d * (3 ^ (↑d + s) * √2)) * cubeBesovPositiveVectorSeminormTwo R s fun (x : Vec d) => g x - cubeAverageVec R g) ^ 2)

Descendant-cube recurrence with the short corrector product absorbed into quadratic u, harmonic, and forcing terms.

theorem HCPolySupport.exists_centeredCorrector_harmonicRemainder_fluxSeminormStepEnergy {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {s lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hg : MemVectorL2 (cubeSet Q) g) (hC : H1CoerciveEstimate (cubeSet Q)) : ∃ (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (w : AHarmonicFunction a (cubeSet Q)), (∀ x ∈ cubeSet Q, u.grad x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) ∧ ∀ (energy : Vec d → ℝ), (∀ x ∈ cubeSet Q, 0 ≤ energy x) → MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume → CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) energy → (Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) → (∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u.grad x))) → (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2) + (geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a * cubeAverage Q energy

PDE-facing full-seminorm local recurrence interface for the weak-flux RHS lane.

This is the one-cube recurrence after constructing the centered Neumann corrector from an H¹ RHS weak solution.

theorem HCPolySupport.exists_centeredCorrector_harmonicRemainder_fluxSeminormStepCoeffEnergy {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {s lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hg : MemVectorL2 (cubeSet Q) g) (hC : H1CoerciveEstimate (cubeSet Q)) : ∃ (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (w : AHarmonicFunction a (cubeSet Q)), (∀ x ∈ cubeSet Q, u.grad x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) ∧ (CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) (coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x) → (Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) → (∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u.grad x))) → (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) * cubeAverage Q (coefficientEnergyDensity a u.grad) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) * cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x))

PDE-facing coefficient-energy local recurrence for the weak-flux RHS lane.

This is the Step-2-ready form of the one-cube recurrence after constructing the centered Neumann corrector from an H¹ RHS weak solution.

theorem HCPolySupport.exists_centeredCorrector_harmonicRemainder_of_h1DirichletRhsWeakSolutionOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {s lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hg : MemVectorL2 (cubeSet Q) g) (hC : H1CoerciveEstimate (cubeSet Q)) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) (hchildBdd : ∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u.grad x))) : ∃ (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (w : AHarmonicFunction a (cubeSet Q)), (∀ x ∈ cubeSet Q, u.grad x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) ∧ (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) * cubeAverage Q (coefficientEnergyDensity a u.grad) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) * cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x)

PDE-facing coefficient-energy recurrence with harmonic flux control supplied by deterministic coarse data.

theorem HCPolySupport.exists_centeredCorrector_harmonicRemainder_fluxSeminormStepShortTerm {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {s lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hg : MemVectorL2 (cubeSet Q) g) (hC : H1CoerciveEstimate (cubeSet Q)) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) (hchildBdd : ∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u.grad x))) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u.grad)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g)) : ∃ (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (w : AHarmonicFunction a (cubeSet Q)), (∀ x ∈ cubeSet Q, u.grad x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) ∧ (BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x) → (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) * cubeAverage Q (coefficientEnergyDensity a u.grad) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) * (↑d * (3 ^ (↑d + s) * (√2 * (cubeBesovNegativeVectorSeminormTwo Q s u.grad + cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => w.toH1.grad x)) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g)))

PDE-facing coefficient-energy recurrence with the corrector term replaced by the short centered Besov product bound. As in the descendant-cube wrapper, the harmonic boundedness assumption is exposed after the harmonic remainder has been constructed.

theorem HCPolySupport.exists_centeredCorrector_harmonicRemainder_fluxSeminormStepAbsorbedShortTerm {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {s η lam Lam : ℝ} (hs : 0 < s) (hη : 0 < η) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hg : MemVectorL2 (cubeSet Q) g) (hC : H1CoerciveEstimate (cubeSet Q)) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) (hchildBdd : ∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u.grad x))) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u.grad)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g)) : ∃ (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (w : AHarmonicFunction a (cubeSet Q)), (∀ x ∈ cubeSet Q, u.grad x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) ∧ (BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x) → (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) * cubeAverage Q (coefficientEnergyDensity a u.grad) + η * cubeBesovNegativeVectorSeminormTwo Q s u.grad ^ 2 + η * (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => w.toH1.grad x) ^ 2 + 2 * η⁻¹ * ((geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a * (↑d * (3 ^ (↑d + s) * √2)) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g) ^ 2)

PDE-facing recurrence with the short corrector product absorbed into quadratic u, harmonic, and forcing terms.