Coarse-graining support: Support.Book.Ch03.Theorems.PublicInternalBridges.WeakSolutionConstructors #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Public weak-solution constructor bridges #
This file contains terminal constructor bridges built from the public weak-solution conversion lemmas.
Audit tag #
Claim: construct the public-coefficient corrector data and homogenization comparison-pair witnesses used by the Chapter 3 endpoint theorem packages.
Downstream target: Ch3 public aggregate imports. This file is constructor
plumbing only and introduces no public *Theory package.
noncomputable def
HCPolySupport.Book.Ch03.publicNeumannForcedMeanZeroCorrectorData
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
(w : NeumannForcedCubeSolution Q a g)
:
MeanZeroNeumannCorrectorData Q (publicCoeffField Q a) fun (x : Vec d) => g x - cubeAverageVec Q g
Realize a forced Neumann solution as mean-zero corrector data on the closed cube, with the public coefficient field and the force centered by its cube average.
Equations
- HCPolySupport.Book.Ch03.publicNeumannForcedMeanZeroCorrectorData w = { toH1MeanZero := HCPolySupport.Book.Ch03.publicH1MeanZeroToCubeSet w.toH1MeanZero, weakSolution := ⋯ }
Instances For
@[simp]
theorem
HCPolySupport.Book.Ch03.neumannForcedSolutionMeanZeroCorrectorData_publicCoeffField_grad
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
(w : NeumannForcedCubeSolution Q a g)
:
theorem
HCPolySupport.Book.Ch03.forcedSolutionGradientField_coarsePoincareRHSSn_le_expanded_publicCoeffField
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
{s : ℝ}
(u : ForcedCubeSolution Q a g)
(hs : 0 < s)
(hs_le : s ≤ 1)
(hg : ForceBesovRegularity Q s g)
(m : ℕ)
:
coarsePoincareRHSSn Q s (forcedSolutionGradientField u) m ≤ 250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) (publicCoeffField Q a))⁻¹ * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) (forcedSolutionGradientField u)) + 15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) (publicCoeffField Q a))⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2
theorem
HCPolySupport.Book.Ch03.isH1DirichletRhsWeakSolutionOn_constantCoeff_cubeSet_of_isConstantCoeffForcedEquation
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a0 : ConstantCoeffMatrix d}
{u : H1Function (Ch02.cubeDomain Q).carrier}
{g : Vec d → Vec d}
(h : IsConstantCoeffForcedEquation Q a0 u g)
:
theorem
HCPolySupport.Book.Ch03.forcedCubeSolution_is_zeroTraceDirichletWeakSolution
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
(u : ZeroTraceForcedCubeSolution Q a g)
:
noncomputable def
HCPolySupport.Book.Ch03.publicZeroTraceDirichletCorrectorData
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffFamily d)
{g : Vec d → Vec d}
(hg : MemVectorL2 (cubeSet Q) g)
:
Canonical public-coefficient zero-trace RHS corrector on the half-open
cube. This is the public Chapter 3 bridge for the auxiliary zero-boundary
solution v₀ used in the Dirichlet energy argument.
Equations
Instances For
theorem
HCPolySupport.Book.Ch03.isHomogenizationComparisonPairOn_publicCoeffField_cubeSet_of_public_comparison
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{a0 : ConstantCoeffMatrix d}
(w : HomogenizationComparisonDatum Q a a0)
(hzero : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => w.u.grad x - w.v.grad x)
:
IsHomogenizationComparisonPairOn (cubeSet Q) (publicCoeffField Q a) a0.matrix (publicH1ToCubeSet w.u).grad
(publicH1ToCubeSet w.v).grad
theorem
HCPolySupport.Book.Ch03.HomogenizationComparisonDatum.isHomogenizationComparisonPairOn_publicCoeffField_cubeSet
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{a0 : ConstantCoeffMatrix d}
(w : HomogenizationComparisonDatum Q a a0)
:
IsHomogenizationComparisonPairOn (cubeSet Q) (publicCoeffField Q a) a0.matrix (publicH1ToCubeSet w.u).grad
(publicH1ToCubeSet w.v).grad
theorem
HCPolySupport.Book.Ch03.isHomogenizationComparisonPairOn_publicCoeffField_cubeSet_of_same_public_forcedEquations
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{a0 : ConstantCoeffMatrix d}
{u v : H1Function (Ch02.cubeDomain Q).carrier}
{g : Vec d → Vec d}
(hu : IsForcedEquation Q a u g)
(hv : IsConstantCoeffForcedEquation Q a0 v g)
(hzero : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.grad x - v.grad x)
:
IsHomogenizationComparisonPairOn (cubeSet Q) (publicCoeffField Q a) a0.matrix (publicH1ToCubeSet u).grad
(publicH1ToCubeSet v).grad
theorem
HCPolySupport.Book.Ch03.CoarseGrainingComparisonDatum.isHomogenizationComparisonPairOn_publicCoeffField_cubeSet
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{a0 : ConstantCoeffMatrix d}
{g : Vec d → Vec d}
(w : CoarseGrainingComparisonDatum Q a a0 g)
:
IsHomogenizationComparisonPairOn (cubeSet Q) (publicCoeffField Q a) a0.matrix (publicH1ToCubeSet w.u).grad
(publicH1ToCubeSet w.v).grad