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

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

Public H1 transport bridges for Chapter 3

This file transports public H1, H10, mean-zero, and zero-trace data to the deterministic half-open cube setting used by Chapter 3 engines.

noncomputable def HCPolySupport.Book.Ch03.publicH1ToCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H1Function (Ch02.cubeDomain Q).carrier) : H1Function (cubeSet Q)

View a public open-domain H¹ function as an H¹ function on the half-open triadic cube used by the deterministic layer.

Equations

• HCPolySupport.Book.Ch03.publicH1ToCubeSet u = (HCPolySupport.Book.Ch03.castH1Domain ⋯ u).toCubeSet

@[simp]

theorem HCPolySupport.Book.Ch03.publicH1ToCubeSet_grad {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H1Function (Ch02.cubeDomain Q).carrier) : (publicH1ToCubeSet u).grad = u.grad

@[simp]

theorem HCPolySupport.Book.Ch03.publicH1ToCubeSet_toFun {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H1Function (Ch02.cubeDomain Q).carrier) : (publicH1ToCubeSet u).toFun = u.toFun

theorem HCPolySupport.Book.Ch03.publicH1ToCubeSet_grad_memVectorL2_descendant_cubeSet {d : ℕ} [NeZero d] {Q R : TriadicCube d} {j : ℕ} (u : H1Function (Ch02.cubeDomain Q).carrier) (hR : R ∈ descendantsAtDepth Q j) : MemVectorL2 (cubeSet R) u.grad

noncomputable def HCPolySupport.Book.Ch03.H1MeanZeroFunction.toCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H1MeanZeroFunction (openCubeSet Q)) : H1MeanZeroFunction (cubeSet Q)

Promote a mean-zero H¹ witness on an open triadic cube to the corresponding half-open cube.

Equations

• HCPolySupport.Book.Ch03.H1MeanZeroFunction.toCubeSet u = { toH1Function := u.toH1Function.toCubeSet, meanZero := ⋯ }

@[simp]

theorem HCPolySupport.Book.Ch03.H1MeanZeroFunction.toCubeSet_toH1Function_grad {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H1MeanZeroFunction (openCubeSet Q)) : (toCubeSet u).toH1Function.grad = u.toH1Function.grad

@[simp]

theorem HCPolySupport.Book.Ch03.H1MeanZeroFunction.toCubeSet_toH1Function_toFun {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H1MeanZeroFunction (openCubeSet Q)) : (toCubeSet u).toH1Function.toFun = u.toH1Function.toFun

noncomputable def HCPolySupport.Book.Ch03.H1MeanZeroFunction.toOpenCubeSet {d : ℕ} {Q : TriadicCube d} (u : H1MeanZeroFunction (cubeSet Q)) : H1MeanZeroFunction (openCubeSet Q)

Restrict a mean-zero H¹ witness on a half-open triadic cube to its open realization.

Equations

• HCPolySupport.Book.Ch03.H1MeanZeroFunction.toOpenCubeSet u = { toH1Function := u.toH1Function.toOpenCubeSet, meanZero := ⋯ }

@[simp]

theorem HCPolySupport.Book.Ch03.H1MeanZeroFunction.toOpenCubeSet_toH1Function_grad {d : ℕ} {Q : TriadicCube d} (u : H1MeanZeroFunction (cubeSet Q)) : (toOpenCubeSet u).toH1Function.grad = u.toH1Function.grad

@[simp]

theorem HCPolySupport.Book.Ch03.H1MeanZeroFunction.toOpenCubeSet_toH1Function_toFun {d : ℕ} {Q : TriadicCube d} (u : H1MeanZeroFunction (cubeSet Q)) : (toOpenCubeSet u).toH1Function.toFun = u.toH1Function.toFun

noncomputable def HCPolySupport.Book.Ch03.publicH1MeanZeroToCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H1MeanZeroFunction (Ch02.cubeDomain Q).carrier) : H1MeanZeroFunction (cubeSet Q)

View a public open-domain mean-zero H¹ function as a mean-zero H¹ function on the half-open triadic cube used by the deterministic layer.

Equations

• HCPolySupport.Book.Ch03.publicH1MeanZeroToCubeSet u = HCPolySupport.Book.Ch03.H1MeanZeroFunction.toCubeSet (HCPolySupport.Book.Ch03.castH1MeanZeroDomain ⋯ u)

@[simp]

theorem HCPolySupport.Book.Ch03.publicH1MeanZeroToCubeSet_toH1Function_grad {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H1MeanZeroFunction (Ch02.cubeDomain Q).carrier) : (publicH1MeanZeroToCubeSet u).toH1Function.grad = u.toH1Function.grad

@[simp]

theorem HCPolySupport.Book.Ch03.publicH1MeanZeroToCubeSet_toH1Function_toFun {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H1MeanZeroFunction (Ch02.cubeDomain Q).carrier) : (publicH1MeanZeroToCubeSet u).toH1Function.toFun = u.toH1Function.toFun

noncomputable def HCPolySupport.Book.Ch03.publicH10ToCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H10Function (Ch02.cubeDomain Q).carrier) : H10Function (cubeSet Q)

View a public open-domain H¹₀ function as an H¹₀ function on the half-open triadic cube used by the deterministic layer.

Equations

• HCPolySupport.Book.Ch03.publicH10ToCubeSet u = (HCPolySupport.Book.Ch03.castH10Domain ⋯ u).toCubeSet

@[simp]

theorem HCPolySupport.Book.Ch03.publicH10ToCubeSet_toH1Function_grad {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H10Function (Ch02.cubeDomain Q).carrier) : (publicH10ToCubeSet u).grad = u.grad

@[simp]

theorem HCPolySupport.Book.Ch03.publicH10ToCubeSet_toH1Function_toFun {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H10Function (Ch02.cubeDomain Q).carrier) : (publicH10ToCubeSet u).toFun = u.toFun

theorem HCPolySupport.Book.Ch03.publicH10ToCubeSet_toH1Function_grad_memVectorL2_descendant_cubeSet {d : ℕ} [NeZero d] {Q R : TriadicCube d} {j : ℕ} (u : H10Function (Ch02.cubeDomain Q).carrier) (hR : R ∈ descendantsAtDepth Q j) : MemVectorL2 (cubeSet R) u.grad

noncomputable def HCPolySupport.Book.Ch03.DirichletForcedCubeSolution.zeroTraceDifferenceH10 {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (u : DirichletForcedCubeSolution Q a g) : H10Function (Ch02.cubeDomain Q).carrier

Chosen public zero-trace representative for the Dirichlet boundary condition v - h ∈ H¹₀(Q).

Equations

• u.zeroTraceDifferenceH10 = Classical.choose ⋯

theorem HCPolySupport.Book.Ch03.DirichletForcedCubeSolution.zeroTraceDifferenceH10_toFun_ae_eq {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (u : DirichletForcedCubeSolution Q a g) : u.zeroTraceDifferenceH10.toFun =ᵐ[volumeMeasureOn (Ch02.cubeDomain Q).carrier] fun (x : Vec d) => u.toH1.toFun x - u.boundaryData.toFun x

noncomputable def HCPolySupport.Book.Ch03.DirichletForcedCubeSolution.zeroTraceDifferenceH10CubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (u : DirichletForcedCubeSolution Q a g) : H10Function (cubeSet Q)

The chosen public zero-trace representative, transported to the deterministic half-open cube.

Equations

• u.zeroTraceDifferenceH10CubeSet = HCPolySupport.Book.Ch03.publicH10ToCubeSet u.zeroTraceDifferenceH10

@[simp]

theorem HCPolySupport.Book.Ch03.DirichletForcedCubeSolution.zeroTraceDifferenceH10CubeSet_grad {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (u : DirichletForcedCubeSolution Q a g) : u.zeroTraceDifferenceH10CubeSet.grad = u.zeroTraceDifferenceH10.grad

@[simp]

theorem HCPolySupport.Book.Ch03.DirichletForcedCubeSolution.zeroTraceDifferenceH10CubeSet_toFun {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (u : DirichletForcedCubeSolution Q a g) : u.zeroTraceDifferenceH10CubeSet.toFun = u.zeroTraceDifferenceH10.toFun

theorem HCPolySupport.Book.Ch03.isPotentialZeroTraceOn_cubeSet_of_publicH10Function {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H10Function (Ch02.cubeDomain Q).carrier) : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.grad x

Zero-trace public test functions provide the deterministic zero-trace-potential predicate on the corresponding half-open cube.

theorem HCPolySupport.Book.Ch03.ZeroTraceForcedCubeSolution.isPotentialZeroTraceOn_cubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (u : ZeroTraceForcedCubeSolution Q a g) : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.toH10.grad x

theorem HCPolySupport.Book.Ch03.HasWeakPartialDerivOn.ae_eq_of_toFun_ae_eq {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {i : Fin d} {u v gi hi : Vec d → ℝ} (huv : u =ᵐ[MeasureTheory.volume.restrict U] v) (hgiLoc : MeasureTheory.LocallyIntegrableOn gi U MeasureTheory.volume) (hhiLoc : MeasureTheory.LocallyIntegrableOn hi U MeasureTheory.volume) (hgi : HasWeakPartialDerivOn U i u gi) (hhi : HasWeakPartialDerivOn U i v hi) : gi =ᵐ[MeasureTheory.volume.restrict U] hi

Weak partial derivatives are unique even when the underlying scalar representatives agree only a.e. on the open domain.

theorem HCPolySupport.Book.Ch03.H1Function.grad_ae_eq_of_toFun_ae_eq {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {u v : H1Function U} (huv : u.toFun =ᵐ[MeasureTheory.volume.restrict U] v.toFun) : u.grad =ᵐ[MeasureTheory.volume.restrict U] v.grad

On an open domain, two H¹ representatives with a.e.-equal values have a.e.-equal weak gradients.

theorem HCPolySupport.Book.Ch03.DirichletForcedCubeSolution.zeroTraceDifferenceH10CubeSet_grad_ae_eq {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (u : DirichletForcedCubeSolution Q a g) : u.zeroTraceDifferenceH10CubeSet.grad =ᵐ[volumeMeasureOn (cubeSet Q)] fun (x : Vec d) => u.toH1.grad x - u.boundaryData.grad x

theorem HCPolySupport.Book.Ch03.DirichletForcedCubeSolution.cubeAverage_energy_le_two_mul_zeroTraceDifference_add_boundary {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (u : DirichletForcedCubeSolution Q a g) : cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) u.toH1.grad) ≤ 2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => u.zeroTraceDifferenceH10CubeSet.grad x) + 2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) (dirichletBoundaryGradientField u))

Coefficient-energy split for a public Dirichlet solution: ∇v = ∇(v - h) + ∇h on the deterministic cube, with the zero-trace representative chosen from the public boundary condition.

theorem HCPolySupport.Book.Ch03.isPotentialZeroTraceOn_cubeSet_of_public_zeroTraceDifference {d : ℕ} [NeZero d] {Q : TriadicCube d} {u v : H1Function (Ch02.cubeDomain Q).carrier} (hzero : ∃ (w : H10Function (Ch02.cubeDomain Q).carrier), w.toFun =ᵐ[volumeMeasureOn (Ch02.cubeDomain Q).carrier] fun (x : Vec d) => u.toFun x - v.toFun x) : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.grad x - v.grad x

The public value-level zero-trace difference u - v ∈ H¹₀ supplies the deterministic zero-trace-potential predicate for the gradient difference.

theorem HCPolySupport.Book.Ch03.HomogenizationComparisonDatum.isPotentialZeroTraceOn_cubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {a0 : ConstantCoeffMatrix d} (w : HomogenizationComparisonDatum Q a a0) : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => w.u.grad x - w.v.grad x

theorem HCPolySupport.Book.Ch03.CoarseGrainingComparisonDatum.isPotentialZeroTraceOn_cubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {a0 : ConstantCoeffMatrix d} {g : Vec d → Vec d} (w : CoarseGrainingComparisonDatum Q a a0 g) : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => w.u.grad x - w.v.grad x