Coarse-graining support: Support.Deterministic.ConstantCoefficientDirichletBesov.CubeVectorH1

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

def HCPolySupport.CubeDirichletDivergenceProblem {d : ℕ} (Q : TriadicCube d) (w : H10Function (openCubeSet Q)) (h : Vec d → Vec d) : Prop

Weak zero-trace formulation of -Δw = div h on a cube.

Equations

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

@[reducible, inline]

abbrev HCPolySupport.CubeKBesovNormModel (d : ℕ) : Type

Abstract placeholder for the cube vector K-functional Besov norm. The formal proof will later replace this model by the actual K-functional definition; keeping it as a parameter lets the Dirichlet proof consume only the properties it needs.

Equations

• HCPolySupport.CubeKBesovNormModel d = (HCPolySupport.TriadicCube d → ℝ → (HCPolySupport.Vec d → HCPolySupport.Vec d) → ℝ)

structure HCPolySupport.CubeVectorH1Function {d : ℕ} (Q : TriadicCube d) : Type

Coordinatewise H¹ vector-field competitors on a cube for the K-functional.

• coord : Fin d → H1Function (openCubeSet Q)

  Scalar Sobolev witnesses for the coordinates of the vector-field K-functional competitor.

@[instance_reducible]

instance HCPolySupport.CubeVectorH1Function.instInhabited {d : ℕ} {Q : TriadicCube d} : Inhabited (CubeVectorH1Function Q)

Equations

• HCPolySupport.CubeVectorH1Function.instInhabited = { default := { coord := fun (x : Fin d) => 0 } }

noncomputable def HCPolySupport.CubeVectorH1Function.toField {d : ℕ} {Q : TriadicCube d} (G : CubeVectorH1Function Q) : Vec d → Vec d

The vector field represented by a coordinatewise H¹ competitor.

Equations

• G.toField x i = (G.coord i).toFun x

noncomputable def HCPolySupport.CubeVectorH1Function.restrictCoordToOpenOverlap {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (G : CubeVectorH1Function Q) (hS : S ∈ overlapCentersAtDepth Q j) (i : Fin d) : H1Function (openOverlapCubeSet S)

Restrict one coordinate of a parent-cube H¹ vector competitor to an admitted open overlap cube.

Equations

• G.restrictCoordToOpenOverlap hS i = (G.coord i).restrict ⋯ ⋯

@[simp]

theorem HCPolySupport.CubeVectorH1Function.restrictCoordToOpenOverlap_apply {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (G : CubeVectorH1Function Q) (hS : S ∈ overlapCentersAtDepth Q j) (i : Fin d) (x : Vec d) : (G.restrictCoordToOpenOverlap hS i).toFun x = (G.coord i).toFun x

@[simp]

theorem HCPolySupport.CubeVectorH1Function.restrictCoordToOpenOverlap_grad {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (G : CubeVectorH1Function Q) (hS : S ∈ overlapCentersAtDepth Q j) (i : Fin d) (x : Vec d) : (G.restrictCoordToOpenOverlap hS i).grad x = (G.coord i).grad x

theorem HCPolySupport.CubeVectorH1Function.memLp_toField_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} (G : CubeVectorH1Function Q) : MeasureTheory.MemLp G.toField 2 (normalizedCubeMeasure Q)

Coordinatewise H¹ competitors are L² vector fields for the normalized cube measure.

theorem HCPolySupport.CubeVectorH1Function.memVectorL2_toField_openCubeSet {d : ℕ} {Q : TriadicCube d} (G : CubeVectorH1Function Q) : MemVectorL2 (openCubeSet Q) G.toField

Coordinatewise H¹ competitors are vector L² fields on the open cube.

theorem HCPolySupport.CubeVectorH1Function.memLp_sub_toField_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} {h : Vec d → Vec d} (hh : MeasureTheory.MemLp h 2 (normalizedCubeMeasure Q)) (G : CubeVectorH1Function Q) : MeasureTheory.MemLp (fun (x : Vec d) => h x - G.toField x) 2 (normalizedCubeMeasure Q)

If the datum is L², then its residual against an H¹ competitor is also L². This is the integrability input needed by the residual energy estimate.

noncomputable def HCPolySupport.CubeVectorH1Function.gradientCoordL2NormSum {d : ℕ} {Q : TriadicCube d} (G : CubeVectorH1Function Q) : ℝ

Coordinate-summed H¹ gradient size for a vector-field competitor.

Equations

• G.gradientCoordL2NormSum = ∑ i : Fin d, (G.coord i).gradientCoordL2NormSum

theorem HCPolySupport.CubeVectorH1Function.gradientCoordL2NormSum_nonneg {d : ℕ} {Q : TriadicCube d} (G : CubeVectorH1Function Q) : 0 ≤ G.gradientCoordL2NormSum

noncomputable def HCPolySupport.CubeVectorH1Function.relativeGradientCoordL2NormSum {d : ℕ} {Q : TriadicCube d} (G : CubeVectorH1Function Q) : ℝ

Parent-normalized coordinate-summed H¹ gradient size.

The local overlapping Besov oscillations use normalized L² norms. Converting the raw L²(openCubeSet Q) gradient size to that normalization costs the scale factor side(Q) / volume(Q)^{1/2}.

Equations

• G.relativeGradientCoordL2NormSum = HCPolySupport.cubeScaleFactor Q / √(HCPolySupport.cubeVolume Q) * G.gradientCoordL2NormSum

theorem HCPolySupport.CubeVectorH1Function.relativeGradientCoordL2NormSum_nonneg {d : ℕ} {Q : TriadicCube d} (G : CubeVectorH1Function Q) : 0 ≤ G.relativeGradientCoordL2NormSum

theorem HCPolySupport.CubeVectorH1Function.relativeGradientCoordL2NormSum_le_mul_of_gradientCoordL2NormSum_le {d : ℕ} {Q : TriadicCube d} {C : ℝ} {V G : CubeVectorH1Function Q} (hGrad : V.gradientCoordL2NormSum ≤ C * G.gradientCoordL2NormSum) : V.relativeGradientCoordL2NormSum ≤ C * G.relativeGradientCoordL2NormSum

noncomputable def HCPolySupport.CubeVectorH1Function.divergence {d : ℕ} {Q : TriadicCube d} (G : CubeVectorH1Function Q) : Vec d → ℝ

Distributional divergence of a coordinatewise H¹ vector competitor.

Equations

• G.divergence x = ∑ i : Fin d, (G.coord i).grad x i

theorem HCPolySupport.CubeVectorH1Function.divergence_memLp_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} (G : CubeVectorH1Function Q) : MeasureTheory.MemLp G.divergence 2 (normalizedCubeMeasure Q)

theorem HCPolySupport.CubeVectorH1Function.divergence_memScalarL2_openCubeSet {d : ℕ} {Q : TriadicCube d} (G : CubeVectorH1Function Q) : MemScalarL2 (openCubeSet Q) G.divergence

theorem HCPolySupport.CubeVectorH1Function.norm_toScalarL2_divergence_le_gradientCoordL2NormSum {d : ℕ} {Q : TriadicCube d} (G : CubeVectorH1Function Q) (hdiv : MemScalarL2 (openCubeSet Q) G.divergence) : ‖toScalarL2 hdiv‖ ≤ G.gradientCoordL2NormSum

theorem HCPolySupport.CubeVectorH1Function.integral_divergence_mul_zeroTrace_eq_neg_integral_vecDot {d : ℕ} {Q : TriadicCube d} (G : CubeVectorH1Function Q) (φ : H10Function (openCubeSet Q)) : ∫ (x : Vec d) in openCubeSet Q, G.divergence x * φ.toFun x = -∫ (x : Vec d) in openCubeSet Q, vecDot (G.toField x) (φ.grad x)

Integration by parts for the distributional divergence of a coordinatewise H¹ vector field tested against an H¹₀ function.

noncomputable def HCPolySupport.CubeVectorH1Function.ofWeakHessianGradient {d : ℕ} {Q : TriadicCube d} {v : H10Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v.toH1Function) : CubeVectorH1Function Q

The coordinate-gradient vector field associated to a weak Hessian witness, packaged as a coordinatewise H¹ competitor.

Equations

• HCPolySupport.CubeVectorH1Function.ofWeakHessianGradient H = { coord := fun (i : Fin d) => H.gradCoordH1Function i }

@[simp]

theorem HCPolySupport.CubeVectorH1Function.ofWeakHessianGradient_toField {d : ℕ} {Q : TriadicCube d} {v : H10Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v.toH1Function) : (ofWeakHessianGradient H).toField = fun (x : Vec d) => v.grad x

theorem HCPolySupport.CubeVectorH1Function.gradientCoordL2NormSum_ofWeakHessianGradient {d : ℕ} {Q : TriadicCube d} {v : H10Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v.toH1Function) : (ofWeakHessianGradient H).gradientCoordL2NormSum = H.hessianCoordL2NormSum

structure HCPolySupport.SmoothOverlapPartition {d : ℕ} (Q : TriadicCube d) (j : ℕ) : Type

Smooth relative partition of unity subordinate to the retained overlap cubes at one depth.

The structure is intentionally an implementation interface: the downstream quasi-interpolant only needs smooth weights, partition of unity, support, derivative, and bounded-overlap facts. The explicit normalized cutoff construction will provide a value of this structure.

• weight : TriadicCube d → Vec d → ℝ

  Smooth scalar weights subordinate to the retained overlap cubes, summing to one on the open parent cube.

• contDiff_weight (S : TriadicCube d) : ContDiff ℝ 1 (self.weight S)
• nonneg {S : TriadicCube d} {x : Vec d} : S ∈ overlapCentersAtDepth Q j → x ∈ openCubeSet Q → 0 ≤ self.weight S x
• zero_of_not_mem {S : TriadicCube d} : S ∉ overlapCentersAtDepth Q j → ∀ (x : Vec d), self.weight S x = 0
• support_subset {S : TriadicCube d} {x : Vec d} : S ∈ overlapCentersAtDepth Q j → x ∈ openCubeSet Q → self.weight S x ≠ 0 → x ∈ openOverlapCubeSet S
• sum_eq_one {x : Vec d} : x ∈ openCubeSet Q → ∑ S ∈ overlapCentersAtDepth Q j, self.weight S x = 1
• coordDeriv_sum_eq_zero {x : Vec d} : x ∈ openCubeSet Q → ∀ (i : Fin d), ∑ S ∈ overlapCentersAtDepth Q j, euclideanCoordDeriv i (self.weight S) x = 0
• coordDeriv_zero_of_not_mem_overlap {S : TriadicCube d} {x : Vec d} (i : Fin d) : S ∈ overlapCentersAtDepth Q j → x ∈ openCubeSet Q → x ∉ overlapCubeSet S → euclideanCoordDeriv i (self.weight S) x = 0
• coordDerivConstant : ℝ

  The nonnegative factor bounding each weight derivative after division by the depth scale.

• coordDerivConstant_nonneg : 0 ≤ self.coordDerivConstant
• coordDeriv_bound {S : TriadicCube d} {x : Vec d} (i : Fin d) : S ∈ overlapCentersAtDepth Q j → x ∈ openCubeSet Q → |euclideanCoordDeriv i (self.weight S) x| ≤ self.coordDerivConstant / (cubeScaleFactor Q / 3 ^ j)
• activeCardBound : ℕ

  A uniform bound on the number of nonzero partition weights at a point of the open cube.

• active_card_bound {x : Vec d} : x ∈ openCubeSet Q → {S ∈ overlapCentersAtDepth Q j | self.weight S x ≠ 0}.card ≤ self.activeCardBound

noncomputable def HCPolySupport.concreteSmoothOverlapPartition {d : ℕ} (Q : TriadicCube d) (j : ℕ) : SmoothOverlapPartition Q j

The overlap partition built from normalized smooth cutoffs, with explicit derivative and active- weight bounds.

Equations

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