Coarse-graining support: Support.Book.Ch03.Theorems.PublicInternalBridges.EndPoints

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

Public/internal bridges for Chapter 3

This file now contains the Besov, flux-RHS, and coarse-graining public/internal bridge endpoints. Lower bridge layers live in the PublicInternalBridges/ submodules.

theorem HCPolySupport.Book.Ch03.cubeBesovPairing_eq_of_left_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {f₁ f₂ g : Vec d → ℝ} (hf : f₁ =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] f₂) : cubeBesovPairing Q f₁ g = cubeBesovPairing Q f₂ g

theorem HCPolySupport.Book.Ch03.cubeBesovDualFullNormValueSet_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {f₁ f₂ : Vec d → ℝ} (s : ℝ) (p q : ENNReal) (hf : f₁ =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] f₂) : cubeBesovDualFullNormValueSet Q s p q f₁ = cubeBesovDualFullNormValueSet Q s p q f₂

theorem HCPolySupport.Book.Ch03.cubeBesovDualFullNorm_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {f₁ f₂ : Vec d → ℝ} (s : ℝ) (p q : ENNReal) (hf : f₁ =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] f₂) : cubeBesovDualFullNorm Q s p q f₁ = cubeBesovDualFullNorm Q s p q f₂

theorem HCPolySupport.Book.Ch03.scaleNormalizedDualNegativeBesovVectorNormTwo_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {F G : Vec d → Vec d} (s : ℝ) (hFG : F =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] G) : scaleNormalizedDualNegativeBesovVectorNormTwo Q s F = scaleNormalizedDualNegativeBesovVectorNormTwo Q s G

theorem HCPolySupport.Book.Ch03.negativeBesovVectorDepthAverage_eq_cubeBesovNegativeVectorDepthAverage {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (j : ℕ) : negativeBesovVectorDepthAverage Q F j = cubeBesovNegativeVectorDepthAverage Q F j

theorem HCPolySupport.Book.Ch03.negativeBesovVectorDepthSeminorm_eq_cubeBesovNegativeVectorDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (j : ℕ) : negativeBesovVectorDepthSeminorm Q s F j = cubeBesovNegativeVectorDepthSeminorm Q s F j

theorem HCPolySupport.Book.Ch03.negativeBesovVectorDepthAverage_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {F G : Vec d → Vec d} (hFG : F =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] G) (j : ℕ) : negativeBesovVectorDepthAverage Q F j = negativeBesovVectorDepthAverage Q G j

theorem HCPolySupport.Book.Ch03.negativeBesovVectorDepthSeminorm_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {F G : Vec d → Vec d} (s : ℝ) (hFG : F =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] G) (j : ℕ) : negativeBesovVectorDepthSeminorm Q s F j = negativeBesovVectorDepthSeminorm Q s G j

theorem HCPolySupport.Book.Ch03.negativeBesovVectorPartialNormFinite_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {F G : Vec d → Vec d} (s q : ℝ) (N : ℕ) (hFG : F =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] G) : negativeBesovVectorPartialNormFinite Q s q N F = negativeBesovVectorPartialNormFinite Q s q N G

theorem HCPolySupport.Book.Ch03.scaleNormalizedNegativeBesovVectorNorm_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {F G : Vec d → Vec d} (s : ℝ) (q : Ch02.MultiscaleExponent) (hFG : F =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] G) : scaleNormalizedNegativeBesovVectorNorm Q s q F = scaleNormalizedNegativeBesovVectorNorm Q s q G

theorem HCPolySupport.Book.Ch03.scaleNegativeBesovVectorNorm_finiteTwo_eq_cubeNegativeSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) : scaleNormalizedNegativeBesovVectorNorm Q s (Ch02.MultiscaleExponent.finite 2) F = cubeBesovNegativeVectorSeminormTwo Q s F

theorem HCPolySupport.Book.Ch03.scaleNormalizedNegativeBesovVectorNorm_finite_one_eq_cubeBesovNegativeVectorSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) : scaleNormalizedNegativeBesovVectorNorm Q s (Ch02.MultiscaleExponent.finite 1) F = cubeBesovNegativeVectorSeminorm Q s F

theorem HCPolySupport.Book.Ch03.publicDualBesovScaleWeight_eq_cubeBesovScaleWeight {d : ℕ} (Q : TriadicCube d) (s : ℝ) : Real.rpow 3 (-s * ↑Q.scale) = cubeBesovScaleWeight s Q

theorem HCPolySupport.Book.Ch03.normalizedDualNegativeBesovNormTwo_le_constant_mul_negativeBesovSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (hs : 0 < s) (hF : MemVectorL2 (cubeSet Q) F) : scaleNormalizedDualNegativeBesovVectorNormTwo Q s F ≤ ↑d * Real.rpow 3 (↑d + s) * cubeBesovNegativeVectorSeminormTwo Q s F

theorem HCPolySupport.Book.Ch03.forcedSolutionFluxDefect_dualNorm_le_constant_mul_negativeBesovSeminormTwo {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {a0 : ConstantCoeffMatrix d} {s : ℝ} {g : Vec d → Vec d} (u : ForcedCubeSolution Q a g) (hs : 0 < s) : scaleNormalizedDualNegativeBesovVectorNormTwo Q s (forcedSolutionFluxDefectField Q a a0 u) ≤ ↑d * Real.rpow 3 (↑d + s) * cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect (publicCoeffField Q a) a0.matrix (forcedSolutionGradientField u))

theorem HCPolySupport.Book.Ch03.homogenizationNegativeBesovLHS_eq_solutionComparisonLHS {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s : ℝ) (u v : H1Function (Ch02.cubeDomain Q).carrier) : homogenizationComparisonNegativeBesovLHS Q a a0 s u v = solutionComparisonNegativeBesovLhs Q s (publicCoeffField Q a) a0.matrix u.grad v.grad

theorem HCPolySupport.Book.Ch03.homogenizationNegativeBesovLHS_le_constant_mul_solutionNegativeBesovLhs {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s : ℝ) (u v : H1Function (Ch02.cubeDomain Q).carrier) (hs : 0 < s) : homogenizationComparisonNegativeBesovLHS Q a a0 s u v ≤ ↑d * Real.rpow 3 (↑d + s) * solutionComparisonNegativeBesovLhs Q s (publicCoeffField Q a) a0.matrix u.grad v.grad

theorem HCPolySupport.Book.Ch03.HomogenizationFluxDefectAverage_eq_negativeBesovFluxAverage {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s : ℝ) (j : ℕ) (u : H1Function (Ch02.cubeDomain Q).carrier) : localizedHomogenizationFluxDefectAverage Q a a0 s j u = localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect (publicCoeffField Q a) a0.matrix u.grad) j

theorem HCPolySupport.Book.Ch03.forcedSolutionFluxFieldNegativeBesovNorm_finite_eq_negativeBesovSeminormTwo {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (s : ℝ) {g : Vec d → Vec d} (u : ForcedCubeSolution Q a g) : scaleNormalizedNegativeBesovVectorNorm Q s (Ch02.MultiscaleExponent.finite 2) (forcedSolutionFluxField Q a u) = cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (publicCoeffField Q a x) (forcedSolutionGradientField u x)

theorem HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo_nonneg_of_forceBesovRegularity {d : ℕ} {Q : TriadicCube d} {s : ℝ} {g : Vec d → Vec d} (hg : ForceBesovRegularity Q s g) : 0 ≤ scaleNormalizedPositiveBesovVectorSeminormTwo Q s g

theorem HCPolySupport.Book.Ch03.coarseGrainingHomogenizationErrorAtDepth_publicCoeffField_eq_public {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s : ℝ) (j : ℕ) : HCPolySupport.coarseGrainingHomogenizationErrorAtDepth Q (publicCoeffField Q a) a0.matrix s j = coarseGrainingHomogenizationErrorAtDepth Q a a0 s j

theorem HCPolySupport.Book.Ch03.weakFluxRHSBound_publicCoeffField_le_dim_sq_mul_public {d : ℕ} [NeZero d] (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) {s : ℝ} {g : Vec d → Vec d} (u : ForcedCubeSolution Q a g) (hC : 0 ≤ C) (hs : 0 < s) (hB_nonneg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s g) : C * (s⁻¹ * √(LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) (publicCoeffField Q a)) * √(cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) (forcedSolutionGradientField u))) + s.rpow (-(5 / 2)) * √(LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) (publicCoeffField Q a)) * √(lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) (publicCoeffField Q a))⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g) ≤ weakFluxWithRHSRHS (↑d ^ 2 * C) Q a s g u