Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.FiniteLp

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

Finite-exponent cube Calderón--Zygmund interface

The source-facing finite-L^p carriers and weak solution predicates for the constant-coefficient cube Calderón--Zygmund argument. The one-level good-λ input remains internal to this module while the source-facing declarations below keep the manuscript's supplied-solution interfaces exact.

structure HCPolySupport.CubeEuclideanL2LpField {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) extends HCPolySupport.CubeEuclideanLpField Q p : Type

A cube field with Euclidean L^p and L² membership for the normalized cube measure.

• toField : Vec d → Vec d
• euclideanMemLp : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (self.toField x)) p.exponent (normalizedCubeMeasure Q)
• euclideanMemL2 : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (self.toField x)) 2 (normalizedCubeMeasure Q)

structure HCPolySupport.CubeEuclideanWspL2Field {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) extends HCPolySupport.CubeEuclideanWspField Q s p : Type

A fractional W^{s,p} cube field with additional Euclidean L² membership for the normalized cube measure.

• toField : Vec d → Vec d
• euclideanMemLp : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (self.toField x)) p.exponent (normalizedCubeMeasure Q)
• euclideanMemWsp : MemCubeEuclideanWsp Q s p self.toField
• euclideanMemL2 : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (self.toField x)) 2 (normalizedCubeMeasure Q)

noncomputable def HCPolySupport.CubeEuclideanL2LpField.toLpTwo {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeEuclideanL2LpField Q p) : CubeEuclideanLpField Q FiniteLpExponent.two

View an L^p cube field as an L² field using its stored Euclidean L² witness.

Equations

• F.toLpTwo = { toField := F.toField, euclideanMemLp := ⋯ }

noncomputable def HCPolySupport.CubeEuclideanWspL2Field.toLpTwo {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanWspL2Field Q s p) : CubeEuclideanLpField Q FiniteLpExponent.two

View a fractional cube field as an L² field using its stored Euclidean L² witness.

Equations

• F.toLpTwo = { toField := F.toField, euclideanMemLp := ⋯ }

def HCPolySupport.IsCenteredCubeW10pScalarDivergenceSolution {d : ℕ} {q : FiniteLpExponent} (m : ℤ) (sigma0 : ℝ) (w : W10pFunction (openCubeSet (originCube d m)) q.exponent) (h : CubeEuclideanLpField (originCube d m) q) : Prop

The zero-trace weak equation sigma0 * ∫ grad w · grad phi = -∫ h · grad phi on the centered cube, tested against smooth compactly supported functions.

Equations

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

def HCPolySupport.IsCenteredCubeH10ScalarDivergenceSolution {d : ℕ} (m : ℤ) (sigma0 : ℝ) (w : H10Function (openCubeSet (originCube d m))) (h : CubeEuclideanLpField (originCube d m) FiniteLpExponent.two) : Prop

The energy-space equation sigma0 * ∫ grad w · grad phi = -∫ h · grad phi on the centered cube, tested against every H10Function.

Equations

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

noncomputable def HCPolySupport.CubeCalderonZygmund.finiteLpExponentSucc (p : FiniteLpExponent) : FiniteLpExponent

Increase a finite exponent by one, retaining the proofs that it lies in (1, ∞).

Equations

• HCPolySupport.CubeCalderonZygmund.finiteLpExponentSucc p = { exponent := p.exponent + 1, one_lt := ⋯, lt_top := ⋯ }

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeH10ScalarDivergence_cz_two {d : ℕ} (m : ℤ) (sigma0 : ℝ) (h : CubeEuclideanL2LpField (originCube d m) FiniteLpExponent.two) (u : H10Function (openCubeSet (originCube d m))) (hsigma0 : 0 < sigma0) (hsolution : IsCenteredCubeH10ScalarDivergenceSolution m sigma0 u h.toLpTwo) : (centeredCubeDomain d m).normalizedEuclideanLpENorm FiniteLpExponent.two.exponent u.grad ≤ (ENNReal.ofReal sigma0)⁻¹ * (centeredCubeDomain d m).normalizedEuclideanLpENorm FiniteLpExponent.two.exponent h.toField

The energy (q = 2) endpoint for the supplied-solution cube Calderón--Zygmund interface; this is the base case used by the all-exponent assembly.

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeH10ScalarDivergence_cz_of_two_lt (d : ℕ) [NeZero d] (q : FiniteLpExponent) (hq : 2 < q.exponent.toReal) : ∃ C < ⊤, ∀ (m : ℤ) (sigma0 : ℝ) (h : CubeEuclideanL2LpField (originCube d m) q) (u : H10Function (openCubeSet (originCube d m))), 0 < sigma0 → IsCenteredCubeH10ScalarDivergenceSolution m sigma0 u h.toLpTwo → (centeredCubeDomain d m).normalizedEuclideanLpENorm q.exponent u.grad ≤ C * (ENNReal.ofReal sigma0)⁻¹ * (centeredCubeDomain d m).normalizedEuclideanLpENorm q.exponent h.toField

Cube Calderón--Zygmund estimate above the energy exponent.