High-contrast homogenization: Provider.Regularity.PrintOrderParametricFiniteRecurrence

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Finite recurrence at a tolerance-selected rounded generation

The stochastic certificate and every finite response row use the printed order. The deterministic Dirichlet response retains its independently selected private order; the two sides meet only through order-independent coefficient and energy data.

structure HCPolySupport.HighContrast.PrintOrderParametricRoundedResponseJoin (d : ℕ) [NeZero d] (g : ℝ) (a : CoeffSpace d) (abar : Mat d) (sourceAmplitude target kappa Cid : ℝ) (X : CoeffSpace d → ℝ) : Type

The selected-generation application together with the fixed private Dirichlet response. No equality between the two fractional orders occurs.

• application : PrintOrderParametricRoundedCoefficientApplication d g a abar sourceAmplitude target kappa Cid X

  Rounded coefficient application at the selected absorption generation.

• responseSpine : PrivateRoundedPhysicalDirichletSpine d

  Fixed private rounded Dirichlet response used alongside the coefficient application.

• responseSpine_eq : self.responseSpine = privateRoundedPhysicalDirichletSpine d
• privateOrder_lt_printOrder : ↑self.responseSpine.order < printCertificateOrder g

def HCPolySupport.HighContrast.PrintOrderParametricRoundedResponseJoin.geometry {d : ℕ} [NeZero d] {g : ℝ} {a : CoeffSpace d} {abar : Mat d} {sourceAmplitude target kappa Cid : ℝ} {X : CoeffSpace d → ℝ} (join : PrintOrderParametricRoundedResponseJoin d g a abar sourceAmplitude target kappa Cid X) : RoundedGenerationAnalyticGeometry d

The deterministic geometry selected by the absorption tolerance.

Equations

• join.geometry = HCPolySupport.HighContrast.RoundedGenerationAnalyticGeometry.ofApplication join.application

structure HCPolySupport.HighContrast.PrintOrderParametricFiniteRecurrenceInputs (d : ℕ) [NeZero d] (g : ℝ) (a : CoeffSpace d) (abar : Mat d) (sourceAmplitude target kappa Cid : ℝ) (X : CoeffSpace d → ℝ) (join : PrintOrderParametricRoundedResponseJoin d g a abar sourceAmplitude target kappa Cid X) : Type

Complete analytic data for the finite recurrence at the selected rounded generation and printed response order.

• step : ℕ

  Positive number of generations dropped in the one-step best-fit contraction.

• step_pos : 0 < self.step
• stepConstant : ℝ

  Nonnegative coefficient of the weak-error energy term in the one-step contraction.

• stepConstant_nonneg : 0 ≤ self.stepConstant
• oneStep (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) join.application.aRounded) (k : ℤ) (hkm : k ≤ m) : finiteCenteredCubeBestFitErrorAt join.application.aRounded m u (k - ↑self.step) ⋯ ≤ 1 / 8 * finiteCenteredCubeBestFitErrorAt join.application.aRounded m u k hkm + self.stepConstant * join.geometry.spatialWeakError a abar ⋯ (printCertificateOrder g) k * finiteCenteredCubeSolutionEnergy join.application.aRounded m u k
• caccioppoliConstant : ℝ

  Positive constant controlling the inner-cube H1 norm by affine approximation error and slope.

• caccioppoliConstant_pos : 0 < self.caccioppoliConstant
• caccioppoli (k : ℤ) (u : Book.Ch03.CubeSolution (originCube d k) join.application.aRounded) (c : ℝ) (e : Vec d) : join.geometry.spatialWeakError a abar ⋯ (printCertificateOrder g) k ≤ 1 → Book.Ch03.h1EnergyNormOnCube (originCube d (k - 2)) join.application.aRounded (finiteCubeSolutionRestriction join.application.aRounded ⋯ u).toH1 ≤ self.caccioppoliConstant * (normalizedAffineCandidateError (originCube d k) u.toH1.toFun c e + euclideanNorm e)
• terminalConstant : ℝ

  Positive constant bounding the terminal best slope by its finite Lipschitz energy row.

• terminalConstant_pos : 0 < self.terminalConstant
• terminalSlope (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) join.application.aRounded) : join.geometry.spatialWeakError a abar ⋯ (printCertificateOrder g) m ≤ 1 → euclideanNorm (FiniteLipschitzCoreInternal.finiteLipschitzBestSlope join.application.aRounded m u m) ≤ self.terminalConstant * FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow join.application.aRounded m u m
• affineErrorConstant : ℝ

  Positive constant bounding the finite Lipschitz affine error row by the energy row.

• affineErrorConstant_pos : 0 < self.affineErrorConstant
• affineErrorEnergy (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) join.application.aRounded) (k : ℤ) (_hkm : k ≤ m) : join.geometry.spatialWeakError a abar ⋯ (printCertificateOrder g) k ≤ 1 → FiniteLipschitzCoreInternal.finiteLipschitzAffineErrorRow join.application.aRounded m u k ≤ self.affineErrorConstant * FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow join.application.aRounded m u k

theorem HCPolySupport.HighContrast.nonempty_printOrderParametricFiniteRecurrenceInputs {d : ℕ} [NeZero d] {g : ℝ} {a : CoeffSpace d} {abar : Mat d} {sourceAmplitude target kappa Cid : ℝ} {X : CoeffSpace d → ℝ} (hg : g ∈ Set.Ico 0 1) (join : PrintOrderParametricRoundedResponseJoin d g a abar sourceAmplitude target kappa Cid X) : Nonempty (PrintOrderParametricFiniteRecurrenceInputs d g a abar sourceAmplitude target kappa Cid X join)

Every selected-generation join supplies all four analytic fields.