Chapter 3 solution and estimate vocabulary

Solution carriers and estimate right-hand sides for the pinned CoarseGraining development. The coefficient, Besov and cube geometry primitives are separated into DomainGeometry so clients can import that foundation independently.

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch03.normalizedSetAverage {d : ℕ} (V : Set (Vec d)) (f : Vec d → ℝ) : ℝ

Normalized integral over an arbitrary measurable set, written as a total quantity so theorem statements do not need side hypotheses merely to parse.

Equations

• HCPolySupport.Book.Ch03.normalizedSetAverage V f = HCPolySupport.volumeAverage V f

noncomputable def HCPolySupport.Book.Ch03.normalizedL2SqOnSet {d : ℕ} (V : Set (Vec d)) (u : Vec d → ℝ) : ℝ

Normalized L² square over a set.

Equations

• HCPolySupport.Book.Ch03.normalizedL2SqOnSet V u = HCPolySupport.Book.Ch03.normalizedSetAverage V fun (x : HCPolySupport.Vec d) => u x ^ 2

noncomputable def HCPolySupport.Book.Ch03.localizedCoeffEnergyValue {d : ℕ} {U : Ch02.Domain d} (V : Set (Vec d)) (a : Ch02.CoeffOn U) (u : H1Function U.carrier) : ℝ

Localized coefficient energy for an H¹ function, using the symmetric part of the public coefficient representative.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.solutionEnergyNorm {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (u : CubeSolution Q a) : ℝ

The global coefficient-energy norm of a Chapter 2 solution on a cube.

Equations

• HCPolySupport.Book.Ch03.solutionEnergyNorm Q a u = √(HCPolySupport.Book.Ch02.variationEnergyValue (HCPolySupport.Book.Ch02.cubeDomain Q) (a.coeffOn Q) u)

def HCPolySupport.Book.Ch03.IsForcedEquation {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (u : H1Function (Ch02.cubeDomain Q).carrier) (g : Vec d → Vec d) : Prop

Weak public formulation of - div(a grad u) = div g on a cube, in the codebase's RHS sign convention.

Equations

• One or more equations did not get rendered due to their size.

structure HCPolySupport.Book.Ch03.ForcedCubeSolution {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (g : Vec d → Vec d) : Type

Forced cube solution for the public Chapter 3.2 estimates.

• toH1 : H1Function (Ch02.cubeDomain Q).carrier

  The Sobolev function satisfying the forced weak equation on the cube.

• weakSolution : IsForcedEquation Q a self.toH1 g

structure HCPolySupport.Book.Ch03.ZeroTraceForcedCubeSolution {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (g : Vec d → Vec d) : Type

Zero-trace forced solution used by the auxiliary Dirichlet estimate.

• toH10 : H10Function (Ch02.cubeDomain Q).carrier

  The zero-trace Sobolev function satisfying the forced weak equation on the cube.

• weakSolution : IsForcedEquation Q a self.toH10.toH1Function g

structure HCPolySupport.Book.Ch03.BoundaryForcedCaccioppoliDatum {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (x : Vec d) (g : Vec d → Vec d) : Type

Boundary-patch forced solution for the RHS Caccioppoli estimate.

• toH1 : H1Function (Ch02.cubeDomain Q).carrier

  The forced Sobolev solution whose trace vanishes on the specified boundary patch.

• weakSolution : IsForcedEquation Q a self.toH1 g
• zeroTraceOnBoundaryPatch : Ch01.LocalizedZeroTraceFunctionOn (Ch02.cubeDomain Q).carrier (openCubeAtScale x (Q.scale - 1)) self.toH1.toFun

structure HCPolySupport.Book.Ch03.DirichletForcedCubeSolution {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (g : Vec d → Vec d) : Type

Dirichlet forced solution with boundary datum h, formalizing v - h ∈ H¹₀(Q).

• toH1 : H1Function (Ch02.cubeDomain Q).carrier

  The Sobolev solution of the forced Dirichlet problem on the cube.

• boundaryData : H1Function (Ch02.cubeDomain Q).carrier

  Sobolev boundary datum whose difference from the solution has zero trace.

• weakSolution : IsForcedEquation Q a self.toH1 g
• zeroTraceDifference : ∃ (w : H10Function (Ch02.cubeDomain Q).carrier), w.toFun =ᵐ[volumeMeasureOn (Ch02.cubeDomain Q).carrier] fun (x : Vec d) => self.toH1.toFun x - self.boundaryData.toFun x

def HCPolySupport.Book.Ch03.IsMeanZeroNeumannForcedEquation {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (w : H1MeanZeroFunction (Ch02.cubeDomain Q).carrier) (g : Vec d → Vec d) : Prop

Mean-zero Neumann weak formulation for the public energy consequence.

Equations

• One or more equations did not get rendered due to their size.

structure HCPolySupport.Book.Ch03.NeumannForcedCubeSolution {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (g : Vec d → Vec d) : Type

Mean-zero Neumann solution of the forced problem on a cube.

The forcing is centered, matching the variational Neumann statement in the notes. The sign follows the codebase's RHS convention.

• toH1MeanZero : H1MeanZeroFunction (Ch02.cubeDomain Q).carrier

  The mean-zero Sobolev solution tested against mean-zero functions with centered forcing.

• weakSolution : IsMeanZeroNeumannForcedEquation Q a self.toH1MeanZero fun (x : Vec d) => g x - cubeAverageVec Q g

noncomputable def HCPolySupport.Book.Ch03.h1EnergyNormOnCube {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (u : H1Function (Ch02.cubeDomain Q).carrier) : ℝ

Coefficient-energy norm of an arbitrary public H¹ function on a cube.

Equations

• HCPolySupport.Book.Ch03.h1EnergyNormOnCube Q a u = √(HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.openCubeSet Q) (a.coeffOn Q) u)

noncomputable def HCPolySupport.Book.Ch03.forcedSolutionEnergyNorm {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {g : Vec d → Vec d} (u : ForcedCubeSolution Q a g) : ℝ

Energy norm of a forced cube solution.

Equations

• HCPolySupport.Book.Ch03.forcedSolutionEnergyNorm Q a u = HCPolySupport.Book.Ch03.h1EnergyNormOnCube Q a u.toH1

noncomputable def HCPolySupport.Book.Ch03.zeroTraceForcedSolutionEnergyNorm {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {g : Vec d → Vec d} (u : ZeroTraceForcedCubeSolution Q a g) : ℝ

Energy norm of a zero-trace forced solution.

Equations

• HCPolySupport.Book.Ch03.zeroTraceForcedSolutionEnergyNorm Q a u = HCPolySupport.Book.Ch03.h1EnergyNormOnCube Q a u.toH10.toH1Function

noncomputable def HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCoreEnergy {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) : ℝ

Energy norm of boundary-patch forced Caccioppoli data.

Equations

• HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCoreEnergy u = HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.Book.Ch03.caccioppoliCoreSet Q x) (a.coeffOn Q) u.toH1

noncomputable def HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliParentL2Sq {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) : ℝ

Parent-cube L² size of boundary-patch forced Caccioppoli data.

Equations

• HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliParentL2Sq u = HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) u.toH1.toFun

noncomputable def HCPolySupport.Book.Ch03.dirichletForcedSolutionEnergyNorm {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {g : Vec d → Vec d} (u : DirichletForcedCubeSolution Q a g) : ℝ

Energy norm of a Dirichlet forced solution.

Equations

• HCPolySupport.Book.Ch03.dirichletForcedSolutionEnergyNorm Q a u = HCPolySupport.Book.Ch03.h1EnergyNormOnCube Q a u.toH1

noncomputable def HCPolySupport.Book.Ch03.dirichletBoundaryGradientField {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (u : DirichletForcedCubeSolution Q a g) : Vec d → Vec d

Gradient of the boundary datum in a Dirichlet forced solution.

Equations

• HCPolySupport.Book.Ch03.dirichletBoundaryGradientField u = u.boundaryData.grad

noncomputable def HCPolySupport.Book.Ch03.neumannForcedSolutionEnergyNorm {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {g : Vec d → Vec d} (u : NeumannForcedCubeSolution Q a g) : ℝ

Energy norm of a mean-zero Neumann forced solution.

Equations

• HCPolySupport.Book.Ch03.neumannForcedSolutionEnergyNorm Q a u = HCPolySupport.Book.Ch03.h1EnergyNormOnCube Q a u.toH1MeanZero.toH1Function

noncomputable def HCPolySupport.Book.Ch03.solutionGradientField {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} (u : CubeSolution Q a) : Vec d → Vec d

Gradient field of a cube solution.

Equations

• HCPolySupport.Book.Ch03.solutionGradientField u = u.toH1.grad

noncomputable def HCPolySupport.Book.Ch03.forcedSolutionGradientField {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (u : ForcedCubeSolution Q a g) : Vec d → Vec d

Gradient field of a forced cube solution.

Equations

• HCPolySupport.Book.Ch03.forcedSolutionGradientField u = u.toH1.grad

noncomputable def HCPolySupport.Book.Ch03.solutionFluxField {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (u : CubeSolution Q a) : Vec d → Vec d

Flux field a ∇u of a cube solution.

Equations

• HCPolySupport.Book.Ch03.solutionFluxField Q a u x = HCPolySupport.matVecMul ((a.coeffOn Q).toCoeffField x) (u.toH1.grad x)

noncomputable def HCPolySupport.Book.Ch03.forcedSolutionFluxField {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {g : Vec d → Vec d} (u : ForcedCubeSolution Q a g) : Vec d → Vec d

Flux field a ∇u of a forced cube solution.

Equations

• HCPolySupport.Book.Ch03.forcedSolutionFluxField Q a u x = HCPolySupport.matVecMul ((a.coeffOn Q).toCoeffField x) (u.toH1.grad x)

structure HCPolySupport.Book.Ch03.ConstantCoeffMatrix (d : ℕ) : Type

A constant symmetric uniformly elliptic comparison matrix.

• matrix : Mat d

  The symmetric elliptic matrix used to compare the variable-coefficient flux.

• isSymm : Matrix.IsSymm self.matrix
• lam : ℝ

  The positive lower ellipticity bound for the comparison matrix.

• Lam : ℝ

  The upper ellipticity bound for the comparison matrix.

• lam_pos : 0 < self.lam
• lam_le_Lam : self.lam ≤ self.Lam
• elliptic : IsEllipticMatrix self.lam self.Lam self.matrix

noncomputable def HCPolySupport.Book.Ch03.constantCoeffMatrixNormHalf {d : ℕ} (a0 : ConstantCoeffMatrix d) : ℝ

The factor |a0|^{1/2} in the flux-response estimate.

Equations

• HCPolySupport.Book.Ch03.constantCoeffMatrixNormHalf a0 = (HCPolySupport.Book.Ch02.matrixNorm a0.matrix).rpow (1 / 2)

noncomputable def HCPolySupport.Book.Ch03.constantCoeffMatrixNorm {d : ℕ} (a0 : ConstantCoeffMatrix d) : ℝ

The factor |a0| in the inhomogeneous flux-response estimate.

Equations

• HCPolySupport.Book.Ch03.constantCoeffMatrixNorm a0 = HCPolySupport.Book.Ch02.matrixNorm a0.matrix

noncomputable def HCPolySupport.Book.Ch03.solutionFluxDefectField {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (u : CubeSolution Q a) : Vec d → Vec d

Flux defect (a - a0)∇u against a constant comparison matrix.

Equations

• HCPolySupport.Book.Ch03.solutionFluxDefectField Q a a0 u x = HCPolySupport.matVecMul ((a.coeffOn Q).toCoeffField x - a0.matrix) (u.toH1.grad x)

noncomputable def HCPolySupport.Book.Ch03.forcedSolutionFluxDefectField {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) {g : Vec d → Vec d} (u : ForcedCubeSolution Q a g) : Vec d → Vec d

Flux defect (a - a0)∇u for a forced solution.

Equations

• HCPolySupport.Book.Ch03.forcedSolutionFluxDefectField Q a a0 u x = HCPolySupport.matVecMul ((a.coeffOn Q).toCoeffField x - a0.matrix) (u.toH1.grad x)

def HCPolySupport.Book.Ch03.IsConstantCoeffForcedEquation {d : ℕ} (Q : TriadicCube d) (a0 : ConstantCoeffMatrix d) (u : H1Function (Ch02.cubeDomain Q).carrier) (g : Vec d → Vec d) : Prop

Constant-coefficient weak formulation of - div(a0 grad u) = div g on a cube, in the codebase's RHS sign convention.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.homogenizationComparisonConstantGradientField {d : ℕ} {Q : TriadicCube d} (a0 : ConstantCoeffMatrix d) (u v : H1Function (Ch02.cubeDomain Q).carrier) : Vec d → Vec d

Constant-coefficient part a0(∇u - ∇v) in the homogenization comparison.

Equations

• HCPolySupport.Book.Ch03.homogenizationComparisonConstantGradientField a0 u v x = HCPolySupport.matVecMul a0.matrix (u.grad x - v.grad x)

noncomputable def HCPolySupport.Book.Ch03.homogenizationComparisonFluxField {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (u v : H1Function (Ch02.cubeDomain Q).carrier) : Vec d → Vec d

Flux difference a∇u - a0∇v in the homogenization comparison.

Equations

• HCPolySupport.Book.Ch03.homogenizationComparisonFluxField Q a a0 u v x = HCPolySupport.matVecMul ((a.coeffOn Q).toCoeffField x) (u.grad x) - HCPolySupport.matVecMul a0.matrix (v.grad x)

noncomputable def HCPolySupport.Book.Ch03.homogenizationComparisonFluxDefectFromGradient {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (G : Vec d → Vec d) : Vec d → Vec d

Local flux defect (a - a0)G, using the coefficient representative on the cube where the norm is evaluated.

Equations

• HCPolySupport.Book.Ch03.homogenizationComparisonFluxDefectFromGradient Q a a0 G x = HCPolySupport.matVecMul ((a.coeffOn Q).toCoeffField x - a0.matrix) (G x)

noncomputable def HCPolySupport.Book.Ch03.homogenizationComparisonFluxDefectField {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (u : H1Function (Ch02.cubeDomain Q).carrier) : Vec d → Vec d

Local flux defect (a - a0)∇u on a cube.

Equations

• HCPolySupport.Book.Ch03.homogenizationComparisonFluxDefectField Q a a0 u = HCPolySupport.Book.Ch03.homogenizationComparisonFluxDefectFromGradient Q a a0 u.grad

structure HCPolySupport.Book.Ch03.HomogenizationComparisonDatum {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) : Type

Data for the duality lemma: a pair satisfying div(a∇u - a0∇v) = 0 and u - v ∈ H¹₀(Q).

• u : H1Function (Ch02.cubeDomain Q).carrier

  The Sobolev function contributing the variable-coefficient flux to the duality comparison.

• v : H1Function (Ch02.cubeDomain Q).carrier

  The Sobolev comparison function contributing the constant-coefficient flux and sharing the trace of u.

• fluxComparisonSolenoidal : IsSolenoidalOn (Ch02.cubeDomain Q).carrier (homogenizationComparisonFluxField Q a a0 self.u self.v)
• zeroTraceDifference : ∃ (w : H10Function (Ch02.cubeDomain Q).carrier), w.toFun =ᵐ[volumeMeasureOn (Ch02.cubeDomain Q).carrier] fun (x : Vec d) => self.u.toFun x - self.v.toFun x

structure HCPolySupport.Book.Ch03.CoarseGrainingComparisonDatum {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (g : Vec d → Vec d) : Type

Data for the general coarse-graining theorem: two solutions with the same right-hand side and zero-trace difference.

• u : H1Function (Ch02.cubeDomain Q).carrier

  The variable-coefficient solution with forcing g in the coarse-graining comparison.

• v : H1Function (Ch02.cubeDomain Q).carrier

  The constant-coefficient solution with forcing g and the same trace as u.

• uWeakSolution : IsForcedEquation Q a self.u g
• vWeakSolution : IsConstantCoeffForcedEquation Q a0 self.v g
• zeroTraceDifference : ∃ (w : H10Function (Ch02.cubeDomain Q).carrier), w.toFun =ᵐ[volumeMeasureOn (Ch02.cubeDomain Q).carrier] fun (x : Vec d) => self.u.toFun x - self.v.toFun x

noncomputable def HCPolySupport.Book.Ch03.homogenizationComparisonNegativeBesovLHS {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s : ℝ) (u v : H1Function (Ch02.cubeDomain Q).carrier) : ℝ

Left-hand side in the Section 3.3 comparison estimates, using the concrete/circ negative Besov seminorm from the deterministic splitting arguments.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.localizedHomogenizationFluxDefectAverage {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s : ℝ) (j : ℕ) (u : H1Function (Ch02.cubeDomain Q).carrier) : ℝ

Localized ℓ² average of the concrete/circ flux-defect negative Besov seminorms over descendants at depth j = m - n. If the parent cube has scale m = Q.scale, then the manuscript lower scale is n = Q.scale - (j : ℤ), which may be negative.

Equations

• One or more equations did not get rendered due to their size.

structure HCPolySupport.Book.Ch03.BoundaryCaccioppoliDatum {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (x : Vec d) : Type

Public localized boundary data for the boundary Caccioppoli theorem.

The zero-trace condition is scalar and localized: every smooth cutoff supported in the boundary window x + cu_{m-1} turns u into an admissible H¹₀ test function on the parent cube. This is the Lean form of the note's Sobolev trace condition u = 0 on (∂cu_m) ∩ (x + cu_{m-1}); it deliberately does not use a gradient-only potential condition, since gradients cannot see constants.

• toH1 : H1Function (Ch02.cubeDomain Q).carrier

  The Sobolev function with an a-harmonic gradient and zero trace on the boundary patch.

• isHarmonic : IsAHarmonicGradient (a.coeffOn Q).toCoeffField (Ch02.cubeDomain Q).carrier self.toH1.grad
• zeroTraceOnBoundaryPatch : Ch01.LocalizedZeroTraceFunctionOn (Ch02.cubeDomain Q).carrier (openCubeAtScale x (Q.scale - 1)) self.toH1.toFun

noncomputable def HCPolySupport.Book.Ch03.boundaryCaccioppoliCoreEnergy {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} (u : BoundaryCaccioppoliDatum Q a x) : ℝ

Localized energy of boundary Caccioppoli data on the core patch.

Equations

• HCPolySupport.Book.Ch03.boundaryCaccioppoliCoreEnergy u = HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.Book.Ch03.caccioppoliCoreSet Q x) (a.coeffOn Q) u.toH1

noncomputable def HCPolySupport.Book.Ch03.boundaryCaccioppoliParentL2Sq {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} (u : BoundaryCaccioppoliDatum Q a x) : ℝ

Parent-cube L² size for boundary Caccioppoli data.

Equations

• HCPolySupport.Book.Ch03.boundaryCaccioppoliParentL2Sq u = HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) u.toH1.toFun

noncomputable def HCPolySupport.Book.Ch03.interiorCaccioppoliCoreEnergy {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (x : Vec d) (u : CubeSolution Q a) : ℝ

Localized energy of an interior solution on the core patch.

Equations

• HCPolySupport.Book.Ch03.interiorCaccioppoliCoreEnergy Q a x u = HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.Book.Ch03.caccioppoliCoreSet Q x) (a.coeffOn Q) u.toH1

noncomputable def HCPolySupport.Book.Ch03.interiorCaccioppoliParentOscillationL2Sq {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (u : CubeSolution Q a) : ℝ

Parent-cube oscillation L² square for the interior Caccioppoli estimate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.caccioppoliPrefactor {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (s t : ℝ) : ℝ

The Caccioppoli prefactor in e.coarse.grained.Caccioppoli.*.deterministic.theory, excluding the final L² square.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.boundaryCaccioppoliRHS {d : ℕ} (C : ℝ) {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} (s t : ℝ) (u : BoundaryCaccioppoliDatum Q a x) : ℝ

Boundary Caccioppoli right-hand side.

Equations

• HCPolySupport.Book.Ch03.boundaryCaccioppoliRHS C s t u = HCPolySupport.Book.Ch03.caccioppoliPrefactor C Q a s t * HCPolySupport.Book.Ch03.boundaryCaccioppoliParentL2Sq u

noncomputable def HCPolySupport.Book.Ch03.interiorCaccioppoliRHS {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (s t : ℝ) (u : CubeSolution Q a) : ℝ

Interior Caccioppoli right-hand side.

Equations

• HCPolySupport.Book.Ch03.interiorCaccioppoliRHS C Q a s t u = HCPolySupport.Book.Ch03.caccioppoliPrefactor C Q a s t * HCPolySupport.Book.Ch03.interiorCaccioppoliParentOscillationL2Sq Q a u

noncomputable def HCPolySupport.Book.Ch03.poincareDiscountFactor (s : ℝ) (q : Ch02.MultiscaleExponent) : ℝ

The factor c_{s,q}^{-1/q}, with value 1 at q = infinity.

Equations

• HCPolySupport.Book.Ch03.poincareDiscountFactor s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q_2) = (HCPolySupport.Book.Ch02.geometricDiscount s q_2).rpow (-(1 / q_2))
• HCPolySupport.Book.Ch03.poincareDiscountFactor s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity = 1

noncomputable def HCPolySupport.Book.Ch03.poincareLowerEllipticityFactor {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (s : ℝ) (q : Ch02.MultiscaleExponent) : ℝ

The lower-ellipticity factor \lambda_{s,q}^{-1/2}.

Equations

• HCPolySupport.Book.Ch03.poincareLowerEllipticityFactor Q a s q = (HCPolySupport.Book.Ch02.lambdaSq Q s q a).rpow (-(1 / 2))

noncomputable def HCPolySupport.Book.Ch03.poincareUpperEllipticityFactor {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (s : ℝ) (q : Ch02.MultiscaleExponent) : ℝ

The upper-ellipticity factor \Lambda_{s,q}^{1/2}.

Equations

• HCPolySupport.Book.Ch03.poincareUpperEllipticityFactor Q a s q = (HCPolySupport.Book.Ch02.LambdaSq Q s q a).rpow (1 / 2)

noncomputable def HCPolySupport.Book.Ch03.coarsePoincareGradientRHS {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (s : ℝ) (q : Ch02.MultiscaleExponent) (u : CubeSolution Q a) : ℝ

Right-hand side in the gradient coarse Poincare estimate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.coarsePoincareFluxRHS {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (s : ℝ) (q : Ch02.MultiscaleExponent) (u : CubeSolution Q a) : ℝ

Right-hand side in the flux coarse Poincare estimate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.coarseFluxResponseRHS {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s : ℝ) (u : CubeSolution Q a) : ℝ

Right-hand side in the coarse flux-response estimate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.coarsePoincareWithRHSGradientRHS {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (s : ℝ) (g : Vec d → Vec d) (u : ForcedCubeSolution Q a g) : ℝ

Right-hand side in the coarse Poincare estimate with forcing.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.zeroDirichletEnergyWithRHSRHS {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (t : ℝ) (g : Vec d → Vec d) : ℝ

Right-hand side in the auxiliary zero-Dirichlet energy estimate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (s t : ℝ) : ℝ

Common prefactor in the boundary Caccioppoli estimate with forcing.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.boundaryCaccioppoliWithRHSRHS {d : ℕ} (C : ℝ) {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (s t : ℝ) (u : BoundaryForcedCaccioppoliDatum Q a x g) : ℝ

Boundary Caccioppoli right-hand side with forcing.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.weakFluxWithRHSRHS {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (s : ℝ) (g : Vec d → Vec d) (u : ForcedCubeSolution Q a g) : ℝ

Right-hand side in the weak flux estimate with forcing.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.coarseFluxResponseWithRHSRHS {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s : ℝ) (g : Vec d → Vec d) (u : ForcedCubeSolution Q a g) : ℝ

Right-hand side in the coarse flux-response estimate with forcing.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.dirichletEnergyWithRHSRHS {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (s : ℝ) (g : Vec d → Vec d) (u : DirichletForcedCubeSolution Q a g) : ℝ

Right-hand side in the Dirichlet energy estimate with forcing and boundary data.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.neumannEnergyWithRHSRHS {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (s : ℝ) (g : Vec d → Vec d) : ℝ

Right-hand side in the mean-zero Neumann energy estimate with forcing.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.coarseGrainingHomogenizationErrorAtDepth {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s : ℝ) (j : ℕ) : ℝ

Truncated homogenization error \mathcal E_{s,\infty,1}(Q,n; a, a0), encoded by descendant depth j = m - n. Equivalently, the manuscript scale is n = Q.scale - (j : ℤ), so negative n are represented by sufficiently large natural depths j.

This is the Ch3.3 localized envelope: the supremum of the Ch2 one-cube homogenization error over the depth-j descendants of the parent cube.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.dualityFromFluxDefectRHS {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s : ℝ) (j : ℕ) (u : H1Function (Ch02.cubeDomain Q).carrier) : ℝ

Right-hand side in the duality estimate from local flux defect to global comparison.

Equations

• HCPolySupport.Book.Ch03.dualityFromFluxDefectRHS C Q a a0 s j u = C * s⁻¹ * HCPolySupport.Book.Ch03.localizedHomogenizationFluxDefectAverage Q a a0 s j u

noncomputable def HCPolySupport.Book.Ch03.dualityFromFluxDefectExponentLossRHS {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s t : ℝ) (j : ℕ) (u : H1Function (Ch02.cubeDomain Q).carrier) : ℝ

Note-facing two-exponent replacement RHS for the duality estimate.

The comparison field is measured at exponent s, while the localized flux-defect average is measured at the independent lower exponent t. The scalar prefactor is the displayed manuscript loss s^{-1} t^{-2} (1/2 - t)^{-1}.

Equations

• HCPolySupport.Book.Ch03.dualityFromFluxDefectExponentLossRHS C Q a a0 s t j u = C * s⁻¹ * t⁻¹ ^ 2 * (1 / 2 - t)⁻¹ * HCPolySupport.Book.Ch03.localizedHomogenizationFluxDefectAverage Q a a0 t j u

noncomputable def HCPolySupport.Book.Ch03.coarseGrainingDepthHalfWeight (s : ℝ) (j : ℕ) : ℝ

The depth factor 3^{s(m-n)/2} in the Section 3.3 coarse-graining bound.

Equations

• HCPolySupport.Book.Ch03.coarseGrainingDepthHalfWeight s j = Real.rpow 3 (s / 2 * ↑j)

noncomputable def HCPolySupport.Book.Ch03.coarseGrainingDepthWeight (s : ℝ) (j : ℕ) : ℝ

The depth factor 3^{s(m-n)} in the Section 3.3 coarse-graining bound.

Equations

• HCPolySupport.Book.Ch03.coarseGrainingDepthWeight s j = Real.rpow 3 (s * ↑j)

noncomputable def HCPolySupport.Book.Ch03.coarseGrainingDepthInvWeight (s : ℝ) (j : ℕ) : ℝ

The inverse depth factor 3^{-s(m-n)} used by scale-separated forcing.

Equations

• HCPolySupport.Book.Ch03.coarseGrainingDepthInvWeight s j = (HCPolySupport.Book.Ch03.coarseGrainingDepthWeight s j)⁻¹

noncomputable def HCPolySupport.Book.Ch03.generalCoarseGrainingL2TwoExponentFluxDefectRHS {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (r r₂ : ℝ) (j : ℕ) (g : Vec d → Vec d) (u : H1Function (Ch02.cubeDomain Q).carrier) : ℝ

Scale-separated local flux-defect RHS in the repaired general coarse-graining estimate. The flux-response quantities are measured at exponent r, while the force is measured at the stronger exponent r₂.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.generalCoarseGrainingL2TwoExponentRHS {d : ℕ} (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s r r₂ : ℝ) (j : ℕ) (g : Vec d → Vec d) (u : H1Function (Ch02.cubeDomain Q).carrier) : ℝ

Note-facing RHS with an independent stronger force exponent r₂. The comparison is measured at exponent s, the flux response at r, and the forcing at r₂.

Equations

• One or more equations did not get rendered due to their size.