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

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

Below-two support for cube Calderón--Zygmund estimates

This file isolates the self-adjoint weak-form calculation used to pass from the already-established above-two estimate to 1 < q < 2. It deliberately exports no source-facing Calderón--Zygmund theorem: the statements here only turn the canonical adjoint solution into a normalized weak solution and identify the two cross pairings.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.scalarDivergence_cross_pairing {d : ℕ} {U : Set (Vec d)} {sigma0 : ℝ} (u v : H10Function U) (h G : Vec d → Vec d) (hu : ∀ (psi : H10Function U), sigma0 * ∫ (x : Vec d) in U, vecDot (u.grad x) (psi.grad x) = -∫ (x : Vec d) in U, vecDot (h x) (psi.grad x)) (hv : ∀ (psi : H10Function U), sigma0 * ∫ (x : Vec d) in U, vecDot (v.grad x) (psi.grad x) = -∫ (x : Vec d) in U, vecDot (G x) (psi.grad x)) : ∫ (x : Vec d) in U, vecDot (u.grad x) (G x) = ∫ (x : Vec d) in U, vecDot (h x) (v.grad x)

Two scalar divergence weak equations can be tested against one another. The scalar coefficient cancels by symmetry of the Euclidean dot product; no positivity assumption is needed for this algebraic cross-pairing identity.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.centeredCube_scalarDivergence_cross_pairing {d : ℕ} (m : ℤ) {sigma0 : ℝ} (u v : H10Function (openCubeSet (originCube d m))) (h G : Vec d → Vec d) (hu : ∀ (psi : H10Function (openCubeSet (originCube d m))), sigma0 * ∫ (x : Vec d), vecDot (u.grad x) (psi.grad x) ∂(centeredCubeDomain d m).normalizedVolume = -∫ (x : Vec d), vecDot (h x) (psi.grad x) ∂(centeredCubeDomain d m).normalizedVolume) (hv : ∀ (psi : H10Function (openCubeSet (originCube d m))), sigma0 * ∫ (x : Vec d), vecDot (v.grad x) (psi.grad x) ∂(centeredCubeDomain d m).normalizedVolume = -∫ (x : Vec d), vecDot (G x) (psi.grad x) ∂(centeredCubeDomain d m).normalizedVolume) : ∫ (x : Vec d), vecDot (u.grad x) (G x) ∂(centeredCubeDomain d m).normalizedVolume = ∫ (x : Vec d), vecDot (h x) (v.grad x) ∂(centeredCubeDomain d m).normalizedVolume

The same cross-pairing calculation on a centered cube with normalized volume. This is the form consumed by the finite-exponent supplied-solution predicate, so the below-two argument never needs to expose a normalization cancellation to a caller.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.integral_vecDot_vectorRadialTruncation_eq_truncatedMoment {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (q : ℝ) (hq : 1 < q) (n : ℕ) (F : α → Vec d) : ∫ (x : α), vecDot (F x) (vectorRadialTruncation q n F x) ∂μ = ∫ (x : α), if euclideanNorm (F x) ≤ ↑n then euclideanNorm (F x) ^ q else 0 ∂μ

The radial test field recovers the corresponding truncated gradient moment under any measure.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.lintegral_enorm_rpow_le_of_truncatedMoment {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {q : ℝ} {F : α → HilbertVec d} {A : ENNReal} (hF : MeasureTheory.AEStronglyMeasurable F μ) (htrunc : ∀ (n : ℕ), ∫⁻ (x : α), truncatedMoment q n F x ∂μ ≤ A) : ∫⁻ (x : α), ‖F x‖ₑ ^ q ∂μ ≤ A

Uniform estimates for radial truncations imply the full ENNReal moment, without presupposing the conclusion that the original field is in L^q.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.memLp_of_truncatedMoment_bound {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {q : ℝ} {F : α → HilbertVec d} {A : ENNReal} (hq : 0 < q) (hF : MeasureTheory.AEStronglyMeasurable F μ) (hA : A ≠ ⊤) (htrunc : ∀ (n : ℕ), ∫⁻ (x : α), truncatedMoment q n F x ∂μ ≤ A) : MeasureTheory.MemLp F (ENNReal.ofReal q) μ

A uniform bound for radial truncations supplies the missing L^q membership once its right-hand side is finite.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.eLpNorm_le_rpow_of_truncatedMoment {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {q : ℝ} {F : α → HilbertVec d} {A : ENNReal} (hq : 0 < q) (hF : MeasureTheory.AEStronglyMeasurable F μ) (htrunc : ∀ (n : ℕ), ∫⁻ (x : α), truncatedMoment q n F x ∂μ ≤ A) : MeasureTheory.eLpNorm F (ENNReal.ofReal q) μ ≤ A ^ q⁻¹

The corresponding direct norm consequence of the truncated-moment estimate.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.abs_integral_vecDot_le_eLpNorm_toReal_mul {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p r : ENNReal} [p.HolderConjugate r] {F G : α → Vec d} (hF : MeasureTheory.MemLp (fun (x : α) => HilbertVec.ofVec (F x)) p μ) (hG : MeasureTheory.MemLp (fun (x : α) => HilbertVec.ofVec (G x)) r μ) : |∫ (x : α), vecDot (F x) (G x) ∂μ| ≤ (MeasureTheory.eLpNorm (fun (x : α) => HilbertVec.ofVec (F x)) p μ).toReal * (MeasureTheory.eLpNorm (fun (x : α) => HilbertVec.ofVec (G x)) r μ).toReal

Hölder control of an integrable Euclidean dot-product integral, stated with the real values of the two finite eLpNorms.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.lintegral_truncatedMoment_eq_ofReal_integral {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {q : ℝ} {F : α → HilbertVec d} {n : ℕ} {k : α → ℝ} (hk : MeasureTheory.Integrable k μ) (hk0 : 0 ≤ᵐ[μ] k) (hpoint : ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (k x) = truncatedMoment q n F x) : ∫⁻ (x : α), truncatedMoment q n F x ∂μ = ENNReal.ofReal (∫ (x : α), k x ∂μ)

A real truncated-moment estimate transfers exactly to the ENNReal truncation used in monotone convergence.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.lintegral_enorm_rpow_le_of_real_truncated_bound {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {q : ℝ} {F : α → HilbertVec d} {A : ℝ} (hF : MeasureTheory.AEStronglyMeasurable F μ) (htrunc : ∀ (n : ℕ), ∃ (k : α → ℝ), MeasureTheory.Integrable k μ ∧ 0 ≤ᵐ[μ] k ∧ (∀ᵐ (x : α) ∂μ, ENNReal.ofReal (k x) = truncatedMoment q n F x) ∧ ∫ (x : α), k x ∂μ ≤ A) : ∫⁻ (x : α), ‖F x‖ₑ ^ q ∂μ ≤ ENNReal.ofReal A

A uniform real bound for integrable radial moments gives the full nonnegative ENNReal moment estimate.

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.cubeRadialTruncationL2LpField {d : ℕ} (Q : TriadicCube d) (q : FiniteLpExponent) (F : Vec d → Vec d) (hF : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => HilbertVec.ofVec (F x)) (volumeMeasureOn (openCubeSet Q))) (n : ℕ) : CubeEuclideanL2LpField Q q.conjugate

Package the radial truncation of a measurable vector field on a cube as simultaneous normalized L² and conjugate-L^p data.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.cubeRadialTruncation_memVectorL2 {d : ℕ} (Q : TriadicCube d) (q : FiniteLpExponent) (F : Vec d → Vec d) (hF : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => HilbertVec.ofVec (F x)) (volumeMeasureOn (openCubeSet Q))) (n : ℕ) : MemVectorL2 (openCubeSet Q) (cubeRadialTruncationL2LpField Q q F hF n).toField

The field-generic radial truncation has the raw vector L² membership required by the canonical adjoint solver.

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.centeredCubeRadialTruncationL2LpField {d : ℕ} (m : ℤ) (q : FiniteLpExponent) (u : H10Function (openCubeSet (originCube d m))) (n : ℕ) : CubeEuclideanL2LpField (originCube d m) q.conjugate

Package the radial truncation of the gradient of a centered-cube H¹₀ function as simultaneous normalized L² and conjugate-L^p data.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.centeredCube_radialTruncation_memVectorL2 {d : ℕ} (m : ℤ) (q : FiniteLpExponent) (u : H10Function (openCubeSet (originCube d m))) (n : ℕ) : MemVectorL2 (openCubeSet (originCube d m)) (centeredCubeRadialTruncationL2LpField m q u n).toField

The centered-cube radial truncation also has the raw vector L² membership required by the canonical adjoint solver.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.centeredCube_integrable_vecDot_of_memVectorL2 {d : ℕ} (m : ℤ) {F G : Vec d → Vec d} (hF : MemVectorL2 (openCubeSet (originCube d m)) F) (hG : MemVectorL2 (openCubeSet (originCube d m)) G) : MeasureTheory.Integrable (fun (x : Vec d) => vecDot (F x) (G x)) (centeredCubeDomain d m).normalizedVolume

Two raw vector L² fields on a centered cube have an integrable dot product for normalized cube volume.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.ofReal_vecDot_vectorRadialTruncation_eq_truncatedMoment {α : Type u_1} {d : ℕ} {q : ℝ} (hq : 1 < q) (n : ℕ) (F : α → Vec d) (x : α) : ENNReal.ofReal (vecDot (F x) (vectorRadialTruncation q n F x)) = truncatedMoment q n (fun (y : α) => HilbertVec.ofVec (F y)) x

The radial vector pairing is the corresponding ENNReal truncated moment.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.eLpNorm_hilbertRadialTruncation_rpow_conjugate_eq_truncatedMoment {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (q : FiniteLpExponent) (n : ℕ) (F : α → HilbertVec d) (hF : MeasureTheory.AEStronglyMeasurable F μ) : MeasureTheory.eLpNorm (hilbertRadialTruncation q.exponent.toReal n F) q.conjugate.exponent μ ^ q.conjugate.exponent.toReal = ∫⁻ (x : α), truncatedMoment q.exponent.toReal n F x ∂μ

The conjugate norm of a radial truncation has exactly the original truncated moment as its power.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.openCubeSetScalarDivergenceSolution_normalized_weak {d : ℕ} [NeZero d] (m : ℤ) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (openCubeSet (originCube d m)) G) (psi : H10Function (openCubeSet (originCube d m))) : sigma0 * ∫ (x : Vec d), vecDot ((openCubeSetScalarDivergenceSolution (originCube d m) hsigma0 G hG).grad x) (psi.grad x) ∂(centeredCubeDomain d m).normalizedVolume = -∫ (x : Vec d), vecDot (G x) (psi.grad x) ∂(centeredCubeDomain d m).normalizedVolume

The canonical raw-adjoint solver also satisfies the centered-cube volume-normalized weak equation. This is a one-way transport: it merely scales both sides and therefore requires neither a cancellation argument nor an additional nonzero hypothesis.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.openCubeSetScalarDivergenceSolution_cross_pairing {d : ℕ} [NeZero d] (Q : TriadicCube d) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (u : H10Function (openCubeSet Q)) (h G : Vec d → Vec d) (hu : ∀ (psi : H10Function (openCubeSet Q)), sigma0 * ∫ (x : Vec d) in openCubeSet Q, vecDot (u.grad x) (psi.grad x) = -∫ (x : Vec d) in openCubeSet Q, vecDot (h x) (psi.grad x)) (hG : MemVectorL2 (openCubeSet Q) G) : ∫ (x : Vec d) in openCubeSet Q, vecDot (u.grad x) (G x) = ∫ (x : Vec d) in openCubeSet Q, vecDot (h x) ((openCubeSetScalarDivergenceSolution Q hsigma0 G hG).grad x)

Specialization of scalarDivergence_cross_pairing to the canonical cube adjoint. The supplied solution is deliberately represented only by its raw weak equation, which lets the finite-q endpoint derive that fact internally from its own normalized predicate.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.openCubeSetScalarDivergenceSolution_normalized_cross_pairing {d : ℕ} [NeZero d] (m : ℤ) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (u : H10Function (openCubeSet (originCube d m))) (h G : Vec d → Vec d) (hu : ∀ (psi : H10Function (openCubeSet (originCube d m))), sigma0 * ∫ (x : Vec d), vecDot (u.grad x) (psi.grad x) ∂(centeredCubeDomain d m).normalizedVolume = -∫ (x : Vec d), vecDot (h x) (psi.grad x) ∂(centeredCubeDomain d m).normalizedVolume) (hG : MemVectorL2 (openCubeSet (originCube d m)) G) : ∫ (x : Vec d), vecDot (u.grad x) (G x) ∂(centeredCubeDomain d m).normalizedVolume = ∫ (x : Vec d), vecDot (h x) ((openCubeSetScalarDivergenceSolution (originCube d m) hsigma0 G hG).grad x) ∂(centeredCubeDomain d m).normalizedVolume

The canonical adjoint cross-pairing directly on the normalized centered cube. This combines the supplied normalized weak equation with the canonical normalized adjoint equation and is the exact bridge for the q < 2 proof.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.eLpNorm_le_of_truncated_cross_bound {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {q : ℝ} {F : α → HilbertVec d} {A : ENNReal} (hq : 1 < q) (hF : MeasureTheory.AEStronglyMeasurable F μ) (htrunc : ∀ (n : ℕ), ∫⁻ (x : α), truncatedMoment q n F x ∂μ ≠ ⊤ ∧ ∫⁻ (x : α), truncatedMoment q n F x ∂μ ≤ A * (∫⁻ (x : α), truncatedMoment q n F x ∂μ) ^ (1 - q⁻¹)) : MeasureTheory.eLpNorm F (ENNReal.ofReal q) μ ≤ A

The radial-truncation bootstrap: an estimate with one conjugate-norm factor on the right already gives the desired L^q bound.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.truncatedMoment_ne_top_of_memLp {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {q : ℝ} {F : α → HilbertVec d} (hq : 0 < q) (hF : MeasureTheory.MemLp F (ENNReal.ofReal q) μ) (n : ℕ) : ∫⁻ (x : α), truncatedMoment q n F x ∂μ ≠ ⊤

A truncated moment is finite whenever the full positive moment is finite.

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeH10ScalarDivergence_cz (d : ℕ) [NeZero d] (q : FiniteLpExponent) : ∃ 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

The supplied-solution cube Calderón--Zygmund estimate for every finite exponent. The q<2 branch is obtained by adjoint duality, the q=2 branch is the energy estimate, and the q>2 branch is the good-λ theorem.