Consumer-facing Calderón--Zygmund bounds

The endpoint assembly is conditional only on the two endpoint estimates. The declarations here put its 3 / 2 and 6 / 5 specializations into the norm conventions used by the pressure consumers. The pressure identification is kept as an explicit a.e. input until the distributional identification and the endpoint estimates are available together.

noncomputable def CKN.Foundation.Euclidean.czP1Constant (A₁ A₂ : ℝ) : ℝ

The real-valued operator constant at exponent 3 / 2.

Equations

• CKN.Foundation.Euclidean.czP1Constant A₁ A₂ = (ENNReal.ofReal (CKN.Foundation.Euclidean.rieszSecondInterpolationConstant A₁ A₂ (3 / 2)) ^ (2 / 3)).toReal

noncomputable def CKN.Foundation.Euclidean.czGradientComponentConstant (A₁ A₂ : ℝ) : ℝ

The real-valued component constant at exponent 6 / 5.

Equations

• CKN.Foundation.Euclidean.czGradientComponentConstant A₁ A₂ = (ENNReal.ofReal (CKN.Foundation.Euclidean.rieszSecondInterpolationConstant A₁ A₂ (6 / 5)) ^ (5 / 6)).toReal

theorem CKN.Foundation.Euclidean.lpNorm_bound_of_eLpNorm {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {p : ℝ} {K : ENNReal} (hK : K ≠ ⊤) {g : Parabolic.Vec3 → ℝ} (hgmem : MeasureTheory.MemLp g (ENNReal.ofReal p) MeasureTheory.volume) (hbound : MeasureTheory.eLpNorm (T g) (ENNReal.ofReal p) MeasureTheory.volume ≤ K * MeasureTheory.eLpNorm g (ENNReal.ofReal p) MeasureTheory.volume) : MeasureTheory.lpNorm (T g) (ENNReal.ofReal p) MeasureTheory.volume ≤ K.toReal * MeasureTheory.lpNorm g (ENNReal.ofReal p) MeasureTheory.volume

theorem CKN.Foundation.Euclidean.eLpNorm_bound_of_l2_interpolation {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ p : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable g → MeasureTheory.MemLp g 2 MeasureTheory.volume → ∀ᵐ (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable (T f)) (hweak : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |T f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (hstrong : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ 2 ≤ ENNReal.ofReal (A₂ ^ 2) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ 2) (hA₁ : 0 ≤ A₁) (hp1 : 1 < p) (hp2 : p < 2) {g : Parabolic.Vec3 → ℝ} (hg : Measurable g) (hgp : MeasureTheory.MemLp g (ENNReal.ofReal p) MeasureTheory.volume) (hg₂ : MeasureTheory.MemLp g 2 MeasureTheory.volume) : MeasureTheory.eLpNorm (T g) (ENNReal.ofReal p) MeasureTheory.volume ≤ ENNReal.ofReal (rieszSecondInterpolationConstant A₁ A₂ p) ^ (1 / p) * MeasureTheory.eLpNorm g (ENNReal.ofReal p) MeasureTheory.volume

noncomputable def CKN.Foundation.Euclidean.l2ExtensionInput {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ p : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable g → MeasureTheory.MemLp g 2 MeasureTheory.volume → ∀ᵐ (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable (T f)) (hweak : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |T f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (hstrong : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ 2 ≤ ENNReal.ofReal (A₂ ^ 2) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ 2) (hA₁ : 0 ≤ A₁) (hp1 : 1 < p) (hp2 : p < 2) (hcongr : ∀ {f g : Parabolic.Vec3 → ℝ}, MeasureTheory.MemLp f 2 MeasureTheory.volume → MeasureTheory.MemLp g 2 MeasureTheory.volume → f =ᵐ[MeasureTheory.volume] g → T f =ᵐ[MeasureTheory.volume] T g) (hadd : ∀ {f g : Parabolic.Vec3 → ℝ}, MeasureTheory.MemLp f 2 MeasureTheory.volume → MeasureTheory.MemLp g 2 MeasureTheory.volume → T (f + g) =ᵐ[MeasureTheory.volume] T f + T g) (hsmul : ∀ (c : ℝ) {f : Parabolic.Vec3 → ℝ}, MeasureTheory.MemLp f 2 MeasureTheory.volume → T (c • f) =ᵐ[MeasureTheory.volume] c • T f) (hK : ENNReal.ofReal (rieszSecondInterpolationConstant A₁ A₂ p) ^ (1 / p) ≠ ⊤) : LpExtensionInput (ENNReal.ofReal p) (ENNReal.ofReal (rieszSecondInterpolationConstant A₁ A₂ p) ^ (1 / p)).toReal

Build extension data from subadditivity, weak-(1,1), measurability and an L² bound.

Equations

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

noncomputable def CKN.Foundation.Euclidean.rieszSecondExtensionInput {i j : Fin 3} {p A₁ : ℝ} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (hA₁ : 0 ≤ A₁) (hp1 : 1 < p) (hp2 : p < 2) (hK : ENNReal.ofReal (rieszSecondInterpolationConstant A₁ 1 p) ^ (1 / p) ≠ ⊤) : LpExtensionInput (ENNReal.ofReal p) (ENNReal.ofReal (rieszSecondInterpolationConstant A₁ 1 p) ^ (1 / p)).toReal

Extension data for a second Riesz transform obtained by interpolation below exponent two.

Equations

• CKN.Foundation.Euclidean.rieszSecondExtensionInput hL2 hWeak11 hA₁ hp1 hp2 hK = CKN.Foundation.Euclidean.l2ExtensionInput ⋯ ⋯ hWeak11 ⋯ hA₁ hp1 hp2 ⋯ ⋯ ⋯ hK

noncomputable def CKN.Foundation.Euclidean.rieszSecondP1ExtensionInput {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) : LpExtensionInput (ENNReal.ofReal (3 / 2)) (czP1Constant rieszSecondWeakTypeConstant 1)

The extension input for the scalar pressure operator at exponent 3 / 2.

Equations

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

noncomputable def CKN.Foundation.Euclidean.rieszSecondGradientExtensionInput {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) : LpExtensionInput (ENNReal.ofReal (6 / 5)) (czGradientComponentConstant rieszSecondWeakTypeConstant 1)

The extension input for one scalar gradient component at exponent 6 / 5.

Equations

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

noncomputable def CKN.Foundation.Euclidean.rieszSecondP1ExtensionOperator {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (f : Parabolic.Vec3 → ℝ) : Parabolic.Vec3 → ℝ

The scalar pressure operator after completion from the L2 carrier.

Equations

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

theorem CKN.Foundation.Euclidean.rieszSecondP1Extension_memLp {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) : HasCompactSupport f → MeasureTheory.MemLp (rieszSecondP1ExtensionOperator hL2 hWeak11 f) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

One completed scalar pressure output is in L^(3/2).

theorem CKN.Foundation.Euclidean.rieszSecondP1Extension_toLp_bound {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hfc : HasCompactSupport f) : ‖MeasureTheory.MemLp.toLp (rieszSecondP1ExtensionOperator hL2 hWeak11 f) ⋯‖ ≤ czP1Constant rieszSecondWeakTypeConstant 1 * ‖MeasureTheory.MemLp.toLp f hf‖

The real norm bound for the completed scalar pressure operator.

noncomputable def CKN.Foundation.Euclidean.rieszSecondGradientExtensionOperator {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (f : Parabolic.Vec3 → ℝ) : Parabolic.Vec3 → ℝ

The indexed completed operator at exponent 6 / 5.

Equations

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

theorem CKN.Foundation.Euclidean.rieszSecondGradientExtension_memLp {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) : HasCompactSupport f → MeasureTheory.MemLp (rieszSecondGradientExtensionOperator hL2 hWeak11 f) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

One completed indexed output is in L^(6/5).

theorem CKN.Foundation.Euclidean.rieszSecondGradientExtension_toLp_bound {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hfc : HasCompactSupport f) : ‖MeasureTheory.MemLp.toLp (rieszSecondGradientExtensionOperator hL2 hWeak11 f) ⋯‖ ≤ czGradientComponentConstant rieszSecondWeakTypeConstant 1 * ‖MeasureTheory.MemLp.toLp f hf‖

The real norm bound for one completed indexed output.

theorem CKN.Foundation.Euclidean.cz_p1_bound {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → Measurable (T f)) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |T f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (hL2 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ 2 ≤ ENNReal.ofReal (A₂ ^ 2) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ 2) (hA₁ : 0 ≤ A₁) {g : Parabolic.Vec3 → ℝ} (hg : Measurable g) (hgmem : MeasureTheory.MemLp g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) : HasCompactSupport g → MeasureTheory.lpNorm (T g) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ czP1Constant A₁ A₂ * MeasureTheory.lpNorm g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

The canonical L^(3/2) Calderón--Zygmund bound for one scalar component.

theorem CKN.Foundation.Euclidean.hCZ_p1_of_cz_p1_bound {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {p₁ g : Parabolic.Vec3 → ℝ} {C_CZ C₁₁ E : ℝ} (hT : ∀ (f : Parabolic.Vec3 → ℝ), MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) MeasureTheory.volume → HasCompactSupport f → MeasureTheory.lpNorm (T f) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C_CZ * MeasureTheory.lpNorm f (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hg : MeasureTheory.MemLp g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hgc : HasCompactSupport g) (hident : p₁ =ᵐ[MeasureTheory.volume] T g) (hsource : MeasureTheory.lpNorm g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ E ^ (2 / 3)) (hC_CZ : 0 ≤ C_CZ) (hconst : C_CZ ≤ C₁₁) (hE : 0 ≤ E) : MeasureTheory.lpNorm p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C₁₁ * E ^ (2 / 3)

The global hCZ_p1 consumer shape after the a.e. identification of p₁. The three consumer files use this bound as their common source estimate.

theorem CKN.Foundation.Euclidean.hCZ_p1_of_slice_operator_bound {η : Parabolic.Vec3 → ℝ} {u : Parabolic.ParabolicPoint → Parabolic.Vec3} {c : ℝ → Parabolic.Vec3} {p : Parabolic.ParabolicPoint → ℝ} {f : Parabolic.ParabolicPoint → Parabolic.Vec3} {Du : Parabolic.ParabolicPoint → Fin 3 → Parabolic.Vec3} {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {G : Parabolic.ParabolicPoint → Parabolic.Vec3 → ℝ} {z : Parabolic.ParabolicPoint} {r ρ C₁₂ : ℝ} (hident : (fun (w : Parabolic.ParabolicPoint) => pressureP1 η u c p f w.2 w.1) =ᵐ[MeasureTheory.volume.restrict (Parabolic.parabolicCylinder z.1 z.2 r)] fun (w : Parabolic.ParabolicPoint) => T (G w) w.1) (hsource : ENNReal.ofReal (r ^ (-4 / 3)) * MeasureTheory.eLpNorm' (fun (w : Parabolic.ParabolicPoint) => T (G w) w.1) (3 / 2) (MeasureTheory.volume.restrict (Parabolic.parabolicCylinder z.1 z.2 r)) ≤ ENNReal.ofReal (C₁₂ * (r / ρ)⁻¹ * alpha u z ρ * beta u Du z ρ)) : ENNReal.ofReal (r ^ (-4 / 3)) * MeasureTheory.eLpNorm' (fun (w : Parabolic.ParabolicPoint) => pressureP1 η u c p f w.2 w.1) (3 / 2) (MeasureTheory.volume.restrict (Parabolic.parabolicCylinder z.1 z.2 r)) ≤ ENNReal.ofReal (C₁₂ * (r / ρ)⁻¹ * alpha u z ρ * beta u Du z ρ)

Transport a slice estimate for T to the exact pressure-decay hCZ_p1.

The old literal representative is not used for the global gradient bound. The selected weak field is the signed indexed extension; its distributional characterization is supplied by the weak-gradient consumer and by the pairing-transfer theorem for the extension.

def CKN.Foundation.Euclidean.HasCZGradientOperatorBound (T : Fin 3 → Fin 3 → (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ) (C_CZ : ℝ) : Prop

The norm-only gradient-bound predicate for a selected indexed operator.

Equations

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

noncomputable def CKN.Foundation.Euclidean.rieszSecondWeakGradientExtensionOperator (hL2 : (i j : Fin 3) → RieszSecondL2Input i j) (hWeak11 : ∀ (i j : Fin 3) (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator (hL2 i j) f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (i : Fin 3) (G : Parabolic.Vec3 → ℝ) : Parabolic.Vec3 → Parabolic.Vec3

The signed weak-gradient operator selected from the pressure extension.

Equations

• CKN.Foundation.Euclidean.rieszSecondWeakGradientExtensionOperator hL2 hWeak11 i G x j = -CKN.Foundation.Euclidean.rieszSecondGradientExtensionOperator (hL2 i j) ⋯ G x

theorem CKN.Foundation.Euclidean.rieszSecondWeakGradientExtensionOperator_memLp (hL2 : (i j : Fin 3) → RieszSecondL2Input i j) (hWeak11 : ∀ (i j : Fin 3) (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator (hL2 i j) f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) {i : Fin 3} {G : Parabolic.Vec3 → ℝ} (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hGc : HasCompactSupport G) : MeasureTheory.MemLp (rieszSecondWeakGradientExtensionOperator hL2 hWeak11 i G) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

The selected weak-gradient field has the indexed L^(6/5) membership.

theorem CKN.Foundation.Euclidean.rieszSecondWeakGradientExtensionOperator_eLpNorm_le (hL2 : (i j : Fin 3) → RieszSecondL2Input i j) (hWeak11 : ∀ (i j : Fin 3) (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator (hL2 i j) f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) {i : Fin 3} {G : Parabolic.Vec3 → ℝ} (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hGc : HasCompactSupport G) : MeasureTheory.eLpNorm (rieszSecondWeakGradientExtensionOperator hL2 hWeak11 i G) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal (3 * czGradientComponentConstant rieszSecondWeakTypeConstant 1) * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

The selected weak-gradient field has the component-summed L^(6/5) bound.

theorem CKN.Foundation.Euclidean.hCZ_grad_of_component_bounds {T : Fin 3 → Fin 3 → (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {Ccomp C_CZ : ℝ} : 0 ≤ Ccomp → ∀ (hconst : 3 * Ccomp ≤ C_CZ) (hcomponent : ∀ (i j : Fin 3) (G : Parabolic.Vec3 → ℝ), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → MeasureTheory.eLpNorm (T i j G) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal Ccomp * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume), HasCZGradientOperatorBound T C_CZ

Aggregate indexed component bounds into the selected vector-valued predicate.

theorem CKN.Foundation.Euclidean.hCZ_grad_of_rieszSecond_inputs {T : Fin 3 → Fin 3 → (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {Ccomp C_CZ : ℝ} (hCcomp : 0 ≤ Ccomp) (hconst : 3 * Ccomp ≤ C_CZ) (hcomponent : ∀ (i j : Fin 3) (G : Parabolic.Vec3 → ℝ), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → MeasureTheory.eLpNorm (T i j G) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal Ccomp * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) : HasCZGradientOperatorBound T C_CZ

Assemble the selected gradient bound without a classical representative premise.