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

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

Finite-exponent duality support for cube Calderón--Zygmund estimates

This file contains the measure-theoretic support for the 1 < q < 2 duality step. It deliberately does not state a Calderón--Zygmund estimate: it only packages the radial truncations, Hölder pairing, and monotone-convergence facts that will be consumed once the supplied-solution q > 2 estimate is available.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.conjugate_toReal_gt_two_of_lt_two (q : FiniteLpExponent) (hq : q.exponent.toReal < 2) : 2 < q.conjugate.exponent.toReal

If a finite exponent lies strictly between one and two, its finite Hölder conjugate is strictly bigger than two.

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.hilbertRadialTruncation {α : Type u_1} {d : ℕ} (q : ℝ) (n : ℕ) (F : α → HilbertVec d) : α → HilbertVec d

The bounded radial test field used in the q < 2 duality argument. The cutoff is by the Euclidean Hilbert norm, so the field remains a valid datum for the H¹₀ adjoint solver.

Equations

• HCPolySupport.CubeCalderonZygmund.INTERNAL.hilbertRadialTruncation q n F = {x : α | ‖F x‖ ≤ ↑n}.indicator fun (x : α) => ‖F x‖ ^ (q - 2) • F x

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.vectorRadialTruncation {α : Type u_1} {d : ℕ} (q : ℝ) (n : ℕ) (F : α → Vec d) : α → Vec d

The algebraic-vector spelling of hilbertRadialTruncation, suitable for the divergence solver API.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.aestronglyMeasurable_hilbertRadialTruncation {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {q : ℝ} {n : ℕ} {F : α → HilbertVec d} (hF : MeasureTheory.AEStronglyMeasurable F μ) : MeasureTheory.AEStronglyMeasurable (hilbertRadialTruncation q n F) μ

The radial truncation is a.e. strongly measurable.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.norm_hilbertRadialTruncation {α : Type u_1} {d : ℕ} {q : ℝ} (hq : 1 < q) (n : ℕ) (F : α → HilbertVec d) (x : α) : ‖hilbertRadialTruncation q n F x‖ = if ‖F x‖ ≤ ↑n then ‖F x‖ ^ (q - 1) else 0

Pointwise Euclidean norm identity for the bounded radial test field.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.inner_hilbertRadialTruncation_self {α : Type u_1} {d : ℕ} {q : ℝ} (hq : 1 < q) (n : ℕ) (F : α → HilbertVec d) (x : α) : inner ℝ (hilbertRadialTruncation q n F x) (F x) = if ‖F x‖ ≤ ↑n then ‖F x‖ ^ q else 0

Pairing the radial test field with the original field recovers the truncated q-power.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.norm_hilbertRadialTruncation_rpow_conjugate {α : Type u_1} {d : ℕ} (q : FiniteLpExponent) (n : ℕ) (F : α → HilbertVec d) (x : α) : ‖hilbertRadialTruncation q.exponent.toReal n F x‖ ^ q.conjugate.exponent.toReal = if ‖F x‖ ≤ ↑n then ‖F x‖ ^ q.exponent.toReal else 0

Raising the radial test field's norm to the Hölder-conjugate exponent recovers the same truncated q-power.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.vecDot_vectorRadialTruncation_self {α : Type u_1} {d : ℕ} {q : ℝ} (hq : 1 < q) (n : ℕ) (F : α → Vec d) (x : α) : vecDot (vectorRadialTruncation q n F x) (F x) = if euclideanNorm (F x) ≤ ↑n then euclideanNorm (F x) ^ q else 0

The algebraic-vector version of the radial pairing identity.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.eLpNorm_vecDot_le_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 μ) : MeasureTheory.eLpNorm (fun (x : α) => vecDot (F x) (G x)) 1 μ ≤ MeasureTheory.eLpNorm (fun (x : α) => HilbertVec.ofVec (F x)) p μ * MeasureTheory.eLpNorm (fun (x : α) => HilbertVec.ofVec (G x)) r μ

Vector-valued Hölder, in the exact eLpNorm form needed to bound the cross weak pairing in the low-exponent duality argument.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.norm_hilbertRadialTruncation_le {α : Type u_1} {d : ℕ} {q : ℝ} (hq : 1 < q) (n : ℕ) (F : α → HilbertVec d) (x : α) : ‖hilbertRadialTruncation q n F x‖ ≤ ↑n ^ (q - 1)

The bounded radial test field has the expected uniform pointwise bound.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.memLp_hilbertRadialTruncation {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {p : ENNReal} {q : ℝ} (hq : 1 < q) (n : ℕ) {F : α → HilbertVec d} (hF : MeasureTheory.AEStronglyMeasurable F μ) : MeasureTheory.MemLp (hilbertRadialTruncation q n F) p μ

On a finite measure, every radial truncation belongs to every finite Lᵖ space, in particular to L² and to the conjugate exponent.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.aestronglyMeasurable_vectorRadialTruncation {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {q : ℝ} {n : ℕ} {F : α → Vec d} (hF : MeasureTheory.AEStronglyMeasurable (fun (x : α) => HilbertVec.ofVec (F x)) μ) : MeasureTheory.AEStronglyMeasurable (vectorRadialTruncation q n F) μ

The algebraic-vector radial truncation is a.e. strongly measurable.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.memVectorL2_vectorRadialTruncation {d : ℕ} (U : Set (Vec d)) [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {q : ℝ} (hq : 1 < q) (n : ℕ) (F : Vec d → Vec d) (hF : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => HilbertVec.ofVec (F x)) (volumeMeasureOn U)) : MemVectorL2 U (vectorRadialTruncation q n F)

The vector radial truncation has a direct L² membership form for the adjoint divergence solver.

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.truncatedMoment {α : Type u_1} {d : ℕ} (q : ℝ) (n : ℕ) (F : α → HilbertVec d) : α → ENNReal

The truncated q-moment integrand used for monotone convergence.

Equations

• HCPolySupport.CubeCalderonZygmund.INTERNAL.truncatedMoment q n F = {x : α | ‖F x‖ ≤ ↑n}.indicator fun (x : α) => ‖F x‖ₑ ^ q

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.aemeasurable_truncatedMoment {α : Type u_1} {d : ℕ} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {q : ℝ} {n : ℕ} {F : α → HilbertVec d} (hF : MeasureTheory.AEStronglyMeasurable F μ) : AEMeasurable (truncatedMoment q n F) μ

The truncated moment integrands are a.e. measurable.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.monotone_truncatedMoment {α : Type u_1} {d : ℕ} {q : ℝ} (F : α → HilbertVec d) (x : α) : Monotone fun (n : ℕ) => truncatedMoment q n F x

At each point, increasing the truncation level increases the truncated moment, provided the moment exponent is nonnegative.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.iSup_truncatedMoment_eq_enorm_rpow {α : Type u_1} {d : ℕ} {q : ℝ} (F : α → HilbertVec d) (x : α) : ⨆ (n : ℕ), truncatedMoment q n F x = ‖F x‖ₑ ^ q

The pointwise supremum of all truncated moments is the full moment.

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

Monotone convergence in the precise truncated-moment form used by the low-exponent duality argument.