Coarse-graining support: Support.Book.Ch03.Theorems.PublicInternalBridges.WeakSolutions #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Public weak-solution bridges for Chapter 3 #
This file contains forced-solution, flux-field, weak-solution, and comparison-pair bridges from the public Chapter 3 data to the deterministic cube APIs.
theorem
HCPolySupport.Book.Ch03.forcedSolutionGradientField_memVectorL2_cubeSet
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
(u : ForcedCubeSolution Q a g)
:
theorem
HCPolySupport.Book.Ch03.forcedSolutionGradientField_memVectorL2_descendant_cubeSet
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
{j : ℕ}
(u : ForcedCubeSolution Q a g)
(hR : R ∈ descendantsAtDepth Q j)
:
theorem
HCPolySupport.Book.Ch03.forcedSolutionGradientField_negativeBesovPartialSeminormTwo_bddAbove
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
{s : ℝ}
(u : ForcedCubeSolution Q a g)
(hs : 0 < s)
:
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N (forcedSolutionGradientField u))
theorem
HCPolySupport.Book.Ch03.forcedSolutionGradientField_descendant_negativeBesovPartialSeminormTwo_bddAbove
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
{j : ℕ}
{s : ℝ}
(u : ForcedCubeSolution Q a g)
(hR : R ∈ descendantsAtDepth Q j)
(hs : 0 < s)
:
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (forcedSolutionGradientField u))
theorem
HCPolySupport.Book.Ch03.AHarmonicFunction.grad_negativeBesovPartialSeminormTwo_bddAbove
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{s : ℝ}
(w : AHarmonicFunction a (cubeSet Q))
(hs : 0 < s)
:
Harmonic H¹ gradients automatically have bounded finite negative-Besov
partials on their cube.
theorem
HCPolySupport.Book.Ch03.forcedSolutionPublicFlux_memVectorL2_descendant_cubeSet
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
{j : ℕ}
(u : ForcedCubeSolution Q a g)
(hR : R ∈ descendantsAtDepth Q j)
:
MemVectorL2 (cubeSet R) fun (x : Vec d) => matVecMul (publicCoeffField Q a x) (forcedSolutionGradientField u x)
theorem
HCPolySupport.Book.Ch03.forcedSolutionPublicFlux_memLp_normalizedCubeMeasure_descendant
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
{j : ℕ}
(u : ForcedCubeSolution Q a g)
(hR : R ∈ descendantsAtDepth Q j)
:
MeasureTheory.MemLp (fun (x : Vec d) => matVecMul (publicCoeffField Q a x) (forcedSolutionGradientField u x)) 2
(normalizedCubeMeasure R)
theorem
HCPolySupport.Book.Ch03.forcedSolutionPublicFlux_negativeBesovPartialSeminormTwo_bddAbove_descendant
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
{j : ℕ}
{s : ℝ}
(u : ForcedCubeSolution Q a g)
(hR : R ∈ descendantsAtDepth Q j)
(hs : 0 < s)
:
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) =>
matVecMul (publicCoeffField Q a x) (forcedSolutionGradientField u x))
theorem
HCPolySupport.Book.Ch03.forcedSolutionPublicFlux_negativeBesovPartialSeminormTwo_bddAbove_child
{d : ℕ}
[NeZero d]
{Q R S : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
{j : ℕ}
{s : ℝ}
(u : ForcedCubeSolution Q a g)
(hR : R ∈ descendantsAtDepth Q j)
(hS : S ∈ descendantsAtDepth R 1)
(hs : 0 < s)
:
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovNegativeVectorPartialSeminormTwo S s N fun (x : Vec d) =>
matVecMul (publicCoeffField Q a x) (forcedSolutionGradientField u x))
theorem
HCPolySupport.Book.Ch03.publicH1_fluxDefect_memVectorL2_descendant_cubeSet
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{a : CoeffFamily d}
{a0 : ConstantCoeffMatrix d}
{j : ℕ}
(u : H1Function (Ch02.cubeDomain Q).carrier)
(hR : R ∈ descendantsAtDepth Q j)
:
MemVectorL2 (cubeSet R) (fluxDefect (publicCoeffField Q a) a0.matrix u.grad)
theorem
HCPolySupport.Book.Ch03.publicH1_fluxDefect_negativeBesovPartialSeminormTwo_bddAbove_descendant
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{a : CoeffFamily d}
{a0 : ConstantCoeffMatrix d}
{j : ℕ}
{s : ℝ}
(u : H1Function (Ch02.cubeDomain Q).carrier)
(hR : R ∈ descendantsAtDepth Q j)
(hs : 0 < s)
:
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect (publicCoeffField Q a) a0.matrix u.grad))
theorem
HCPolySupport.Book.Ch03.CoarseGrainingComparisonDatum.fluxDefect_negativeBesovPartialSeminormTwo_bddAbove_descendant
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{a : CoeffFamily d}
{a0 : ConstantCoeffMatrix d}
{g : Vec d → Vec d}
{j : ℕ}
{s : ℝ}
(w : CoarseGrainingComparisonDatum Q a a0 g)
(hR : R ∈ descendantsAtDepth Q j)
(hs : 0 < s)
:
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect (publicCoeffField Q a) a0.matrix w.u.grad))
theorem
HCPolySupport.Book.Ch03.IsH1DirichletRhsWeakSolutionOn.of_residual_solenoidal
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{u : H1Function U}
{g : Vec d → Vec d}
(hflux : MemVectorL2 U fun (x : Vec d) => matVecMul (a x) (u.grad x))
(hg : MemVectorL2 U g)
(hsol : IsSolenoidalOn U fun (x : Vec d) => matVecMul (a x) (u.grad x) - g x)
:
IsH1DirichletRhsWeakSolutionOn a U u g
theorem
HCPolySupport.Book.Ch03.IsH1DirichletRhsWeakSolutionOn.restrict_cubeSet_of_mem_descendantsAtDepth
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{j : ℕ}
{a : CoeffField d}
{u : H1Function (cubeSet Q)}
{g : Vec d → Vec d}
{lam Lam : ℝ}
(h : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hg : MemVectorL2 (cubeSet Q) g)
(hR : R ∈ descendantsAtDepth Q j)
:
theorem
HCPolySupport.Book.Ch03.weakFluxRHSScaledAveragedSeminormSq_bddAbove_publicCoeffField_forcedSolution
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
{s : ℝ}
(u : ForcedCubeSolution Q a g)
(hs : 0 < s)
:
BddAbove
(Set.range fun (n : ℕ) =>
weakFluxRHSScaledAveragedSeminormSq Q (publicCoeffField Q a) s (forcedSolutionGradientField u) n)
theorem
HCPolySupport.Book.Ch03.forcedSolutionFluxField_ae_eq_publicCoeffField_cubeSet
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
(u : ForcedCubeSolution Q a g)
:
forcedSolutionFluxField Q a u =ᵐ[volumeMeasureOn (cubeSet Q)] fun (x : Vec d) =>
matVecMul (publicCoeffField Q a x) (u.toH1.grad x)
theorem
HCPolySupport.Book.Ch03.forcedSolutionFluxDefectField_ae_eq_fluxDefect_publicCoeffField_cubeSet
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{a0 : ConstantCoeffMatrix d}
{g : Vec d → Vec d}
(u : ForcedCubeSolution Q a g)
:
forcedSolutionFluxDefectField Q a a0 u =ᵐ[volumeMeasureOn (cubeSet Q)]
fluxDefect (publicCoeffField Q a) a0.matrix u.toH1.grad
theorem
HCPolySupport.Book.Ch03.homogenizationComparisonFluxDefectFromGradient_ae_eq_fluxDefect_publicCoeffField_cubeSet
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{a0 : ConstantCoeffMatrix d}
(G : Vec d → Vec d)
:
homogenizationComparisonFluxDefectFromGradient Q a a0 G =ᵐ[volumeMeasureOn (cubeSet Q)]
fluxDefect (publicCoeffField Q a) a0.matrix G
theorem
HCPolySupport.Book.Ch03.homogenizationFluxDefectFromGradient_ae_eq_fluxDefect_parent_descendant_cube
{d : ℕ}
{Q R : TriadicCube d}
{a : CoeffFamily d}
{a0 : ConstantCoeffMatrix d}
{j : ℕ}
(hR : R ∈ descendantsAtDepth Q j)
(G : Vec d → Vec d)
:
homogenizationComparisonFluxDefectFromGradient R a a0 G =ᵐ[volumeMeasureOn (cubeSet R)]
fluxDefect (publicCoeffField Q a) a0.matrix G
theorem
HCPolySupport.Book.Ch03.homogenizationComparisonFluxField_ae_eq_fluxComparison_publicCoeffField_cubeSet
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{a0 : ConstantCoeffMatrix d}
(u v : H1Function (Ch02.cubeDomain Q).carrier)
:
homogenizationComparisonFluxField Q a a0 u v =ᵐ[volumeMeasureOn (cubeSet Q)]
fluxComparison (publicCoeffField Q a) a0.matrix u.grad v.grad
theorem
HCPolySupport.Book.Ch03.homogenizationComparisonConstantGradientField_eq_constantGradientComparison
{d : ℕ}
{Q : TriadicCube d}
{a0 : ConstantCoeffMatrix d}
(u v : H1Function (Ch02.cubeDomain Q).carrier)
:
theorem
HCPolySupport.Book.Ch03.isPotentialZeroTraceOn_cubeSet_of_openCubeSet_ae
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{f g : Vec d → Vec d}
(hf : IsPotentialZeroTraceOn (openCubeSet Q) f)
(hfg : f =ᵐ[volumeMeasureOn (openCubeSet Q)] g)
:
A zero-trace potential on the public open cube can be moved to cubeSet
after changing representatives a.e. on the open cube.
theorem
HCPolySupport.Book.Ch03.IsSolenoidalOn.congr_ae
{d : ℕ}
{U : Set (Vec d)}
{f g : Vec d → Vec d}
(hfg : f =ᵐ[volumeMeasureOn U] g)
(hf : IsSolenoidalOn U f)
:
IsSolenoidalOn U g
The solenoidal predicate is insensitive to a.e. changes of the vector field on the test domain.
theorem
HCPolySupport.Book.Ch03.isH1DirichletRhsWeakSolutionOn_coeffOn_of_isForcedEquation
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{u : H1Function (Ch02.cubeDomain Q).carrier}
{g : Vec d → Vec d}
(h : IsForcedEquation Q a u g)
:
IsH1DirichletRhsWeakSolutionOn (a.coeffOn Q).toCoeffField (Ch02.cubeDomain Q).carrier u g
theorem
HCPolySupport.Book.Ch03.isH1DirichletRhsWeakSolutionOn_publicCoeffField_of_isForcedEquation
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{u : H1Function (Ch02.cubeDomain Q).carrier}
{g : Vec d → Vec d}
(h : IsForcedEquation Q a u g)
:
IsH1DirichletRhsWeakSolutionOn (publicCoeffField Q a) (Ch02.cubeDomain Q).carrier u g
theorem
HCPolySupport.Book.Ch03.isZeroTraceDirichletRhsWeakSolution_coeffOn_of_zeroTraceForcedCubeSolution
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
(u : ZeroTraceForcedCubeSolution Q a g)
:
theorem
HCPolySupport.Book.Ch03.isZeroTraceDirichletRhsWeakSolution_publicCoeffField_of_zeroTraceForcedCubeSolution
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
(u : ZeroTraceForcedCubeSolution Q a g)
:
theorem
HCPolySupport.Book.Ch03.isMeanZeroNeumannRhsWeakSolution_coeffOn_of_isMeanZeroNeumannForcedEquation
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{w : H1MeanZeroFunction (Ch02.cubeDomain Q).carrier}
{g : Vec d → Vec d}
(h : IsMeanZeroNeumannForcedEquation Q a w g)
:
theorem
HCPolySupport.Book.Ch03.isMeanZeroNeumannRhsWeakSolution_publicCoeffField_of_isMeanZeroNeumannForcedEquation
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{w : H1MeanZeroFunction (Ch02.cubeDomain Q).carrier}
{g : Vec d → Vec d}
(h : IsMeanZeroNeumannForcedEquation Q a w g)
:
theorem
HCPolySupport.Book.Ch03.isMeanZeroNeumannRhsWeakSolution_publicCoeffField_of_neumannForcedCubeSolution
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
(w : NeumannForcedCubeSolution Q a g)
:
IsMeanZeroNeumannRhsWeakSolution (publicCoeffField Q a) (Ch02.cubeDomain Q).carrier w.toH1MeanZero fun (x : Vec d) =>
g x - cubeAverageVec Q g
theorem
HCPolySupport.Book.Ch03.isH1DirichletRhsWeakSolutionOn_constantCoeff_of_isConstantCoeffForcedEquation
{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.isH1DirichletRhsWeakSolutionOn_cubeSet_of_openCubeSet
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffField d}
{u : H1Function (openCubeSet Q)}
{g : Vec d → Vec d}
(h : IsH1DirichletRhsWeakSolutionOn a (openCubeSet Q) u g)
:
IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u.toCubeSet g
Open-cube weak equations transport to the half-open triadic cube because the two realizations differ by a null boundary.
theorem
HCPolySupport.Book.Ch03.isZeroTraceDirichletRhsWeakSolution_cubeSet_of_openCubeSet
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffField d}
{u : H10Function (openCubeSet Q)}
{g : Vec d → Vec d}
(h : IsZeroTraceDirichletRhsWeakSolution a (openCubeSet Q) u g)
:
theorem
HCPolySupport.Book.Ch03.isMeanZeroNeumannRhsWeakSolution_cubeSet_of_openCubeSet
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffField d}
{u : H1MeanZeroFunction (openCubeSet Q)}
{g : Vec d → Vec d}
(h : IsMeanZeroNeumannRhsWeakSolution a (openCubeSet Q) u g)
:
theorem
HCPolySupport.Book.Ch03.isH1DirichletRhsWeakSolutionOn_publicCoeffField_cubeSet_of_isForcedEquation
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{u : H1Function (Ch02.cubeDomain Q).carrier}
{g : Vec d → Vec d}
(h : IsForcedEquation Q a u g)
:
IsH1DirichletRhsWeakSolutionOn (publicCoeffField Q a) (cubeSet Q) (publicH1ToCubeSet u) g
theorem
HCPolySupport.Book.Ch03.CoarseGrainingComparisonDatum.fluxDefect_negativeBesov_le_coarseFluxResponseBound
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{a : CoeffFamily d}
{a0 : ConstantCoeffMatrix d}
{g : Vec d → Vec d}
{j : ℕ}
{s : ℝ}
(w : CoarseGrainingComparisonDatum Q a a0 g)
(hs : 0 < s)
(hs_lt : s < 1)
(hg : ForceBesovRegularity Q s g)
(hR : R ∈ descendantsAtDepth Q j)
:
cubeBesovNegativeVectorSeminormTwo R s (fluxDefect (publicCoeffField Q a) a0.matrix w.u.grad) ≤ 2 * ZeroTraceDirichletCorrectorData.zeroTraceFluxApexConstant d 1 * coarseFluxResponseRHSBound R (publicCoeffField Q a) a0.matrix s w.u.grad g
theorem
HCPolySupport.Book.Ch03.isMeanZeroNeumannRhsWeakSolution_publicCoeffField_cubeSet_of_isMeanZeroNeumannForcedEquation
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{w : H1MeanZeroFunction (Ch02.cubeDomain Q).carrier}
{g : Vec d → Vec d}
(h : IsMeanZeroNeumannForcedEquation Q a w g)
:
theorem
HCPolySupport.Book.Ch03.isMeanZeroNeumannRhsWeakSolution_publicCoeffField_cubeSet_of_neumannForcedCubeSolution
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{g : Vec d → Vec d}
(w : NeumannForcedCubeSolution Q a g)
:
IsMeanZeroNeumannRhsWeakSolution (publicCoeffField Q a) (cubeSet Q) (publicH1MeanZeroToCubeSet w.toH1MeanZero)
fun (x : Vec d) => g x - cubeAverageVec Q g