Coarse-graining support: Support.Book.Ch03.ABK26.FluxComparisonBridges

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

Structural bridges for the Chapter 3 flux-comparison estimate

This module converts the exact public hypotheses of the source-facing flux-comparison statement into the representative-level potential and solenoidal predicates used by the deterministic testing layer. It contains only algebraic and measure-normalization bridges; no quantitative estimate is proved here.

theorem HCPolySupport.Book.Ch03.ABK26.HasCenteredCubeH10Difference.exists_grad_ae_eq {d : ℕ} {m : ℤ} {u v : H1Function (openCubeSet (originCube d m))} (hzero : HasCenteredCubeH10Difference m u v) : ∃ (w : H10Function (openCubeSet (originCube d m))), w.grad =ᵐ[volumeMeasureOn (openCubeSet (originCube d m))] fun (x : Vec d) => u.grad x - v.grad x

A zero-trace value difference has the expected gradient difference, up to the a.e. equality intrinsic to Sobolev functions.

theorem HCPolySupport.Book.Ch03.ABK26.HasCenteredCubeH10Difference.isPotentialZeroTraceOn_openCubeSet {d : ℕ} {m : ℤ} {u v : H1Function (openCubeSet (originCube d m))} (hzero : HasCenteredCubeH10Difference m u v) : IsPotentialZeroTraceOn (openCubeSet (originCube d m)) fun (x : Vec d) => u.grad x - v.grad x

The source-facing zero-trace difference hypothesis supplies the exact potential predicate for the gradient difference on the open cube.

theorem HCPolySupport.Book.Ch03.ABK26.HasCenteredCubeH10Difference.isPotentialZeroTraceOn_cubeSet {d : ℕ} [NeZero d] {m : ℤ} {u v : H1Function (openCubeSet (originCube d m))} (hzero : HasCenteredCubeH10Difference m u v) : IsPotentialZeroTraceOn (cubeSet (originCube d m)) fun (x : Vec d) => u.grad x - v.grad x

The same zero-trace potential, transported to the half-open cube used by the deterministic testing API.

theorem HCPolySupport.Book.Ch03.ABK26.cubeDirichletDivergenceProblem_to_centeredCubeH10ScalarDivergenceSolution {d : ℕ} {p : FiniteLpExponent} (m : ℤ) {z : H10Function (openCubeSet (originCube d m))} {h : CubeEuclideanLpField (originCube d m) p} (hh : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (h.toField x)) 2 (normalizedCubeMeasure (originCube d m))) (hz : CubeDirichletDivergenceProblem (originCube d m) z h.toField) : IsCenteredCubeH10ScalarDivergenceSolution m 1 z { toField := h.toField, euclideanMemLp := hh }

A raw cube Dirichlet divergence problem is the same weak equation after moving to the normalized centered-cube measure.

theorem HCPolySupport.Book.Ch03.ABK26.CubeEuclideanL2LpField.to_centeredH10DivergenceSolution {d : ℕ} {p : FiniteLpExponent} (m : ℤ) (h : CubeEuclideanL2LpField (originCube d m) p) (z : H10Function (openCubeSet (originCube d m))) (hz : CubeDirichletDivergenceProblem (originCube d m) z h.toField) : IsCenteredCubeH10ScalarDivergenceSolution m 1 z h.toLpTwo

The same normalization bridge when the datum already carries both its finite-exponent and L² certificates.

theorem HCPolySupport.Book.Ch03.ABK26.IsCenteredCubeFluxBalanced.isSolenoidalOn_openCubeSet {d : ℕ} {m : ℤ} {a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))} {sigma0 : ℝ} {u v : H1Function (openCubeSet (originCube d m))} (hbal : IsCenteredCubeFluxBalanced m a sigma0 u v) : IsSolenoidalOn (openCubeSet (originCube d m)) fun (x : Vec d) => matVecMul (a.toCoeffField x) (u.grad x) - sigma0 • v.grad x

The normalized weak flux balance is equivalent to raw solenoidality on the open cube: the positive volume-normalization factor cancels.

theorem HCPolySupport.Book.Ch03.ABK26.IsCenteredCubeFluxBalanced.isSolenoidalOn_cubeSet {d : ℕ} [NeZero d] {m : ℤ} {a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))} {sigma0 : ℝ} {u v : H1Function (openCubeSet (originCube d m))} (hbal : IsCenteredCubeFluxBalanced m a sigma0 u v) : IsSolenoidalOn (cubeSet (originCube d m)) fun (x : Vec d) => matVecMul (a.toCoeffField x) (u.grad x) - sigma0 • v.grad x

The raw solenoidal field, transported to the half-open cube used by the deterministic testing API.

noncomputable def HCPolySupport.Book.Ch03.ABK26.centeredCubeRootFluxDefectL2Field {d : ℕ} (m : ℤ) (a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))) (sigma0 : ℝ) (u : H1Function (openCubeSet (originCube d m))) : CubeEuclideanLpField (originCube d m) FiniteLpExponent.two

The root scalar-comparator flux defect, with the literal representative used in every descendant defect.

Equations

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

theorem HCPolySupport.Book.Ch03.ABK26.centeredCubeFluxDifference_eq_smul_gradientDifference_add_rootDefect {d : ℕ} (m : ℤ) (a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))) (sigma0 : ℝ) (u v : H1Function (openCubeSet (originCube d m))) : (centeredCubeFluxDifferenceL2Field m a sigma0 u v).toField = sigma0 • (centeredCubeGradientDifferenceL2Field m u v).toField + (centeredCubeRootFluxDefectL2Field m a sigma0 u).toField

Exact pointwise decomposition of the global flux into the scalar gradient difference and the root coefficient defect.

theorem HCPolySupport.Book.Ch03.ABK26.centeredCubeRootFluxDefectL2Field_toField_eq_local {d : ℕ} (m n : ℤ) (hnm : n < m) (a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))) (sigma0 : ℝ) (u : H1Function (openCubeSet (originCube d m))) (R : TriadicCube d) (hR : R ∈ descendantsAtScale (originCube d m) n) : (centeredCubeRootFluxDefectL2Field m a sigma0 u).toField = (centeredCubeLocalFluxDefectL2Field m n hnm a sigma0 u R hR).toField

Every local defect is literally the same representative as the root defect, merely supplied with the local L² certificate.