Coarse-graining support: Support.Sobolev.Fractional.ExactOverlapFinitePAveraging

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

Finite-p synchronized overlap averaging

This module packages the concrete smooth overlap average simultaneously as an H¹ and a finite-W¹ᵖ vector field. The two witnesses have literally the same field and the same coordinate derivative matrix. The remaining one-depth estimates are stated against the direct Euclidean overlap energy, so later Calderón--Zygmund interpolation can use them without introducing a separate K-functional carrier.

noncomputable def HCPolySupport.cubeEuclideanPositiveBesovOverlapDepthENorm {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) (F : Vec d → Vec d) (j : ℕ) : ENNReal

The rooted direct Euclidean overlap energy at one depth. Its p-th power is exactly the unweighted j summand in cubeEuclideanPositiveBesovOverlapESeminorm.

Equations

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

theorem HCPolySupport.cubeEuclideanPositiveBesovOverlapDepthENorm_nonneg {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) (F : Vec d → Vec d) (j : ℕ) : 0 ≤ cubeEuclideanPositiveBesovOverlapDepthENorm Q p F j

Nonnegativity of the rooted one-depth Euclidean overlap energy.

theorem HCPolySupport.cubeEuclideanPositiveBesovOverlapDepthENorm_rpow {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) (F : Vec d → Vec d) (j : ℕ) : cubeEuclideanPositiveBesovOverlapDepthENorm Q p F j ^ p.exponent.toReal = (↑(ScalarOverlap.centersAtDepth Q j).card)⁻¹ * ∑ S ∈ (ScalarOverlap.centersAtDepth Q j).attach, MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (F x - ScalarOverlap.cubeAverageVec (↑S) F)) p.exponent (ScalarOverlap.normalizedCubeMeasure ↑S) ^ p.exponent.toReal

Raising the rooted depth energy to p recovers its unrooted finite overlap average exactly.

theorem HCPolySupport.cubeEuclideanPositiveBesovOverlapPowerEnergy_eq_tsum_depthENorm {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : cubeEuclideanPositiveBesovOverlapPowerEnergy Q s p F = ∑' (j : ℕ), ENNReal.ofReal (Real.rpow 3 (-(↑s * p.exponent.toReal * ↑(Q.scale - ↑j)))) * cubeEuclideanPositiveBesovOverlapDepthENorm Q p F j ^ p.exponent.toReal

The complete overlap energy is the weighted sum of the rooted depth energies. This is the precise connection used by the later one-level Calderón--Zygmund estimate.

theorem HCPolySupport.lintegral_enorm_rpow_sub_averagingField_le_overlapDepthENorm_rpow {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (p : FiniteLpExponent) (hh : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (h x)) p.exponent (normalizedCubeMeasure Q)) : ∫⁻ (x : Vec d), ‖HilbertVec.ofVec (h x - P.averagingField h x)‖ₑ ^ p.exponent.toReal ∂normalizedCubeMeasure Q ≤ 3 ^ d * cubeEuclideanPositiveBesovOverlapDepthENorm Q p h j ^ p.exponent.toReal

The powered finite-p residual of the concrete average is controlled by the direct Euclidean overlap energy at the same depth.

noncomputable def HCPolySupport.SmoothOverlapPartition.averagingCompetitorW1p {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (p : FiniteLpExponent) : CubeVectorW1pFunction Q p

The concrete smooth overlap average as a finite-W^{1,p} vector field. It intentionally reuses the field formula of averagingCompetitor; only the Sobolev witness changes.

Equations

• P.averagingCompetitorW1p h p = { coord := fun (i : Fin d) => HCPolySupport.W1pFunction.ofContDiffOnIsOpenBoundedConvexDomain ⋯ ⋯ }

theorem HCPolySupport.SmoothOverlapPartition.averagingCompetitorW1p_toField_apply {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (p : FiniteLpExponent) (x : Vec d) (i : Fin d) : (P.averagingCompetitorW1p h p).toField x i = P.averagingField h x i

theorem HCPolySupport.SmoothOverlapPartition.averagingCompetitorW1p_jacobian_apply {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (p : FiniteLpExponent) (x : Vec d) (i k : Fin d) : (P.averagingCompetitorW1p h p).jacobian x i k = euclideanCoordDeriv k (fun (y : Vec d) => P.averagingField h y i) x

theorem HCPolySupport.SmoothOverlapPartition.averagingCompetitors_toField_eq {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (p : FiniteLpExponent) : (P.averagingCompetitor h).toField = (P.averagingCompetitorW1p h p).toField

The Hilbert and finite-p overlap-average witnesses are synchronized at the field level.

theorem HCPolySupport.SmoothOverlapPartition.averagingCompetitors_grad_eq {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (p : FiniteLpExponent) (x : Vec d) (i k : Fin d) : ((P.averagingCompetitor h).coord i).grad x k = (P.averagingCompetitorW1p h p).jacobian x i k

The Hilbert and finite-p overlap-average witnesses are synchronized at the derivative level.

theorem HCPolySupport.SmoothOverlapPartition.enorm_rpow_averagingCompetitorW1p_jacobian_le {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (p : FiniteLpExponent) {x : Vec d} (hx : x ∈ openCubeSet Q) : ‖HilbertMat.ofMat ((P.averagingCompetitorW1p h p).jacobian x)‖ₑ ^ p.exponent.toReal ≤ ((if p.exponent.toReal ≤ 2 then 1 else ↑(Fintype.card (Fin d × Fin d)) ^ (p.exponent.toReal / 2 - 1)) * ↑(Fintype.card (Fin d × Fin d)) * ENNReal.ofReal (3 ^ d * (P.coordDerivConstant / (cubeScaleFactor Q / 3 ^ j)) ^ 2) ^ (p.exponent.toReal / 2) * if p.exponent.toReal ≤ 2 then 1 else (3 ^ d) ^ (p.exponent.toReal / 2 - 1)) * ∑ S ∈ ScalarOverlap.centersAtDepth Q j, (ScalarOverlap.cubeSet S).indicator (fun (y : Vec d) => ‖HilbertVec.ofVec (h y - ScalarOverlap.cubeAverageVec S h)‖ₑ ^ p.exponent.toReal) x

Pointwise finite-p Jacobian control for the concrete overlap-average formula. The finite-center and finite-matrix losses are dimension-only.

theorem HCPolySupport.SmoothOverlapPartition.lintegral_enorm_rpow_averagingCompetitorW1p_jacobian_le_depthENorm {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (p : FiniteLpExponent) (hh : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (h x)) p.exponent (normalizedCubeMeasure Q)) : ∫⁻ (x : Vec d), ‖HilbertMat.ofMat ((P.averagingCompetitorW1p h p).jacobian x)‖ₑ ^ p.exponent.toReal ∂normalizedCubeMeasure Q ≤ ((if p.exponent.toReal ≤ 2 then 1 else ↑(Fintype.card (Fin d × Fin d)) ^ (p.exponent.toReal / 2 - 1)) * ↑(Fintype.card (Fin d × Fin d)) * ENNReal.ofReal (3 ^ d * (P.coordDerivConstant / (cubeScaleFactor Q / 3 ^ j)) ^ 2) ^ (p.exponent.toReal / 2) * if p.exponent.toReal ≤ 2 then 1 else (3 ^ d) ^ (p.exponent.toReal / 2 - 1)) * 3 ^ d * cubeEuclideanPositiveBesovOverlapDepthENorm Q p h j ^ p.exponent.toReal

Powered normalized finite-p Jacobian estimate for the overlap-average competitor. The only overlap loss is the dimension-only bounded-overlap constant; in particular no depth-cardinality appears.

theorem HCPolySupport.SmoothOverlapPartition.exists_synchronized_averagingCompetitors {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (p : FiniteLpExponent) (_h2 : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (h x)) 2 (normalizedCubeMeasure Q)) (_hp : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (h x)) p.exponent (normalizedCubeMeasure Q)) : ∃ (G2 : CubeVectorH1Function Q) (Gp : CubeVectorW1pFunction Q p), G2.toField = P.averagingField h ∧ Gp.toField = P.averagingField h ∧ ∀ (x : Vec d) (i k : Fin d), (G2.coord i).grad x k = Gp.jacobian x i k

Simultaneous Hilbert and finite-p witnesses for an input carrying both integrability classes. The membership assumptions are retained here because the later residual estimates consume both witnesses from the same datum.