Coarse-graining support: Support.Book.Ch03.Theorems.CoarseCaccioppoliRHS.Setup

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

Coarse Caccioppoli with RHS Setup

This file is split mechanically out of CoarseCaccioppoliRHS.lean.

Audit tag

Claim: define the public forced-boundary Caccioppoli decomposition data and transport the zero-trace corrector into the open-cube public domain.

Downstream target: CoarseCaccioppoliRHS/EnergySplit.lean. This file should remain setup infrastructure, not a public theorem-package surface.

noncomputable def HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorOpenH10 {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : H10Function (Ch02.cubeDomain Q).carrier

The public/open-cube form of the zero-trace corrector attached to the forced boundary Caccioppoli decomposition.

Equations

• HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorOpenH10 ρ = HCPolySupport.Book.Ch03.castH10Domain ⋯ ρ.toH10.toOpenCubeSet

@[simp]

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorOpenH10_grad {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : (boundaryForcedCaccioppoliCorrectorOpenH10 ρ).grad = ρ.toH10.grad

@[simp]

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorOpenH10_toFun {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : (boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toFun = ρ.toH10.toFun

theorem HCPolySupport.Book.Ch03.isZeroTraceDirichletRhsWeakSolution_openCubeSet_of_cubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {A : CoeffField d} {u : H10Function (cubeSet Q)} {g : Vec d → Vec d} (h : IsZeroTraceDirichletRhsWeakSolution A (cubeSet Q) u g) : IsZeroTraceDirichletRhsWeakSolution A (openCubeSet Q) u.toOpenCubeSet g

Half-open zero-trace RHS weak solutions transport to the open cube because the boundary has zero volume.

theorem HCPolySupport.Book.Ch03.isZeroTraceDirichletRhsWeakSolution_coeffOn_openCubeSet_of_publicCoeffField {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} {u : H10Function (openCubeSet Q)} {g : Vec d → Vec d} (h : IsZeroTraceDirichletRhsWeakSolution (publicCoeffField Q a) (openCubeSet Q) u g) : IsZeroTraceDirichletRhsWeakSolution (a.coeffOn Q).toCoeffField (openCubeSet Q) u g

On the public open cube, replacing publicCoeffField by the deterministic coeffOn representative preserves zero-trace RHS weak solutions.

noncomputable def HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorZeroTraceForcedCubeSolution {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : ZeroTraceForcedCubeSolution Q a g

Public zero-trace forced-solution wrapper for the auxiliary corrector in the forced boundary Caccioppoli decomposition.

Equations

• HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorZeroTraceForcedCubeSolution ρ = { toH10 := HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorOpenH10 ρ, weakSolution := ⋯ }

noncomputable def HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorForcedCubeSolution {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : ForcedCubeSolution Q a g

Public forced-solution wrapper for the zero-trace corrector, used when the RHS Poincare gradient estimate is applied to the corrector itself.

Equations

• HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorForcedCubeSolution ρ = { toH1 := (HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toH1Function, weakSolution := ⋯ }

@[simp]

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorForcedCubeSolution_grad {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : (boundaryForcedCaccioppoliCorrectorForcedCubeSolution ρ).toH1.grad = ρ.toH10.grad

@[simp]

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorForcedCubeSolution_energyNorm_eq {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : forcedSolutionEnergyNorm Q a (boundaryForcedCaccioppoliCorrectorForcedCubeSolution ρ) = zeroTraceForcedSolutionEnergyNorm Q a (boundaryForcedCaccioppoliCorrectorZeroTraceForcedCubeSolution ρ)

noncomputable def HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderOpenH1 {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : H1Function (Ch02.cubeDomain Q).carrier

Value-level homogeneous remainder w = u - ρ on the public open cube.

Equations

• HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderOpenH1 u ρ = u.toH1 - (HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toH1Function

@[simp]

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderOpenH1_grad {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : (boundaryForcedCaccioppoliRemainderOpenH1 u ρ).grad = fun (y : Vec d) => u.toH1.grad y - ρ.toH10.grad y

@[simp]

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderOpenH1_toFun {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : (boundaryForcedCaccioppoliRemainderOpenH1 u ρ).toFun = fun (y : Vec d) => u.toH1.toFun y - ρ.toH10.toFun y

noncomputable def HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderCubeH1 {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : H1Function (cubeSet Q)

Deterministic half-open-cube realization of the homogeneous remainder.

Equations

• HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderCubeH1 u ρ = HCPolySupport.Book.Ch03.publicH1ToCubeSet (HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderOpenH1 u ρ)

@[simp]

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderCubeH1_grad {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : (boundaryForcedCaccioppoliRemainderCubeH1 u ρ).grad = fun (y : Vec d) => u.toH1.grad y - ρ.toH10.grad y

@[simp]

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderCubeH1_toFun {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) : (boundaryForcedCaccioppoliRemainderCubeH1 u ρ).toFun = fun (y : Vec d) => u.toH1.toFun y - ρ.toH10.toFun y

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderCube_isAHarmonicGradient_publicCoeffField {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hg_mem : MemVectorL2 (cubeSet Q) g) : IsAHarmonicGradient (publicCoeffField Q a) (cubeSet Q) (boundaryForcedCaccioppoliRemainderCubeH1 u ρ).grad

The value-level remainder is a-harmonic on the deterministic cube.

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderOpen_isAHarmonicGradient_publicCoeffField {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hg_mem : MemVectorL2 (cubeSet Q) g) : IsAHarmonicGradient (publicCoeffField Q a) (openCubeSet Q) (boundaryForcedCaccioppoliRemainderOpenH1 u ρ).grad

The value-level remainder is harmonic for the public coefficient field on the open cube.

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderOpen_isAHarmonicGradient_coeffOn {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hg_mem : MemVectorL2 (cubeSet Q) g) : IsAHarmonicGradient (a.coeffOn Q).toCoeffField (Ch02.cubeDomain Q).carrier (boundaryForcedCaccioppoliRemainderOpenH1 u ρ).grad

The value-level remainder is harmonic for the note-facing coefficient representative on the public cube domain.

noncomputable def HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderDatum {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hg_mem : MemVectorL2 (cubeSet Q) g) : BoundaryCaccioppoliDatum Q a x

Homogeneous boundary datum obtained by subtracting the zero-trace Dirichlet corrector from a forced boundary datum.

Equations

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

@[simp]

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliRemainderDatum_toH1 {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hg_mem : MemVectorL2 (cubeSet Q) g) : (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem).toH1 = boundaryForcedCaccioppoliRemainderOpenH1 u ρ