Coarse-graining support: Support.Besov.Negative.ExactDual

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

Exact dual-negative Besov kernel

This module records the three Chapter 1 negative Besov endpoint branches as duals of the exact overlapping positive Besov kernel. The source exponents remain real; their ENNReal images are used only for MemLp and the extended supremum which deliberately retains ∞.

noncomputable def HCPolySupport.exactDualConjExponent (p : ℝ) : ℝ

The finite real Hölder conjugate used by the exact dual branches.

Equations

• HCPolySupport.exactDualConjExponent p = p.conjExponent

theorem HCPolySupport.exactDualConjExponent_holder (p : ℝ) (hp : 1 < p) : p.HolderConjugate (exactDualConjExponent p)

theorem HCPolySupport.exactDualConjExponent_one_lt (p : ℝ) (hp : 1 < p) : 1 < exactDualConjExponent p

theorem HCPolySupport.exactDualConjExponent_one_le (p : ℝ) (hp : 1 < p) : 1 ≤ exactDualConjExponent p

theorem HCPolySupport.exactDualHolderConjugateENNReal (p : ℝ) (hp : 1 < p) : (ENNReal.ofReal p).HolderConjugate (ENNReal.ofReal (exactDualConjExponent p))

noncomputable def HCPolySupport.exactDualNormalizedPairing {d : ℕ} (Q : TriadicCube d) (f g : Vec d → ℝ) (_hfg : MeasureTheory.Integrable (fun (x : Vec d) => f x * g x) (normalizedCubeMeasure Q)) : ENNReal

The normalized absolute pairing used in the exact negative definitions. Its integrability proof is an explicit argument: no totalized integral is used as a substitute for the Hölder side condition.

Equations

• HCPolySupport.exactDualNormalizedPairing Q f g _hfg = ENNReal.ofReal |∫ (x : HCPolySupport.Vec d), f x * g x ∂HCPolySupport.normalizedCubeMeasure Q|

theorem HCPolySupport.exactDualNormalizedPairing_eq {d : ℕ} (Q : TriadicCube d) (f g : Vec d → ℝ) (hfg : MeasureTheory.Integrable (fun (x : Vec d) => f x * g x) (normalizedCubeMeasure Q)) : exactDualNormalizedPairing Q f g hfg = ENNReal.ofReal |∫ (x : Vec d), f x * g x ∂normalizedCubeMeasure Q|

noncomputable def HCPolySupport.exactDualPairingFromHolder {d : ℕ} (Q : TriadicCube d) (p : ℝ) (f g : Vec d → ℝ) (hp : 1 < p) (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g (ENNReal.ofReal (exactDualConjExponent p)) (normalizedCubeMeasure Q)) : ENNReal

The normalized absolute pairing obtained from the displayed Hölder data.

Equations

• HCPolySupport.exactDualPairingFromHolder Q p f g hp hf hg = HCPolySupport.exactDualNormalizedPairing Q f g ⋯

theorem HCPolySupport.exactDualPairingFromHolder_eq {d : ℕ} (Q : TriadicCube d) (p : ℝ) (f g : Vec d → ℝ) (hp : 1 < p) (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g (ENNReal.ofReal (exactDualConjExponent p)) (normalizedCubeMeasure Q)) : exactDualPairingFromHolder Q p f g hp hf hg = ENNReal.ofReal |∫ (x : Vec d), f x * g x ∂normalizedCubeMeasure Q|

theorem HCPolySupport.exactDualPairingFromHolder_congr_ae {d : ℕ} (Q : TriadicCube d) (p : ℝ) (f f' g : Vec d → ℝ) (hp : 1 < p) (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) (normalizedCubeMeasure Q)) (hf' : MeasureTheory.MemLp f' (ENNReal.ofReal p) (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g (ENNReal.ofReal (exactDualConjExponent p)) (normalizedCubeMeasure Q)) (hff' : f =ᵐ[normalizedCubeMeasure Q] f') : exactDualPairingFromHolder Q p f g hp hf hg = exactDualPairingFromHolder Q p f' g hp hf' hg

structure HCPolySupport.ExactDualQOneParameters : Type

Negative q = 1 source parameters. The positive test space has q' = ∞, including the allowed s = 1 endpoint.

• s : ℝ

  Negative smoothness exponent.

• p : ℝ

  Data integrability exponent.

• s_pos : 0 < self.s
• s_le_one : self.s ≤ 1
• p_one_lt : 1 < self.p

structure HCPolySupport.ExactDualFiniteParameters : Type

Negative finite interior source parameters.

• s : ℝ

  Negative smoothness exponent.

• p : ℝ

  Data integrability exponent.

• q : ℝ

  Finite negative aggregation exponent.

• s_pos : 0 < self.s
• s_lt_one : self.s < 1
• p_one_lt : 1 < self.p
• q_one_lt : 1 < self.q

structure HCPolySupport.ExactDualTopParameters : Type

Negative q = ∞ source parameters. The positive test space has q' = 1.

• s : ℝ

  Negative smoothness exponent.

• p : ℝ

  Data integrability exponent.

• s_pos : 0 < self.s
• s_lt_one : self.s < 1
• p_one_lt : 1 < self.p

noncomputable def HCPolySupport.ExactDualQOneParameters.positiveParameters (P : ExactDualQOneParameters) : ExactOverlapTopParameters

The exact positive q' = infinity parameters used to test this branch.

Equations

• P.positiveParameters = { s := P.s, p := HCPolySupport.exactDualConjExponent P.p, admissible := ⋯ }

noncomputable def HCPolySupport.ExactDualFiniteParameters.positiveParameters (P : ExactDualFiniteParameters) : ExactOverlapFiniteParameters

The exact finite positive Hölder-conjugate test parameters.

Equations

• P.positiveParameters = { s := P.s, p := HCPolySupport.exactDualConjExponent P.p, q := HCPolySupport.exactDualConjExponent P.q, admissible := ⋯ }

noncomputable def HCPolySupport.ExactDualTopParameters.positiveParameters (P : ExactDualTopParameters) : ExactOverlapFiniteParameters

The exact positive q' = 1 test parameters.

Equations

• P.positiveParameters = { s := P.s, p := HCPolySupport.exactDualConjExponent P.p, q := 1, admissible := ⋯ }

theorem HCPolySupport.exactDualOverlapIntegrable {d : ℕ} (Q : TriadicCube d) (p : ℝ) (hp : 1 ≤ p) {g : Vec d → ℝ} (hg : MeasureTheory.MemLp g (ENNReal.ofReal p) (normalizedCubeMeasure Q)) : ExactOverlapIntegrable Q g

A positive parent MemLp certificate supplies every certified root and overlap-local integral required by the exact positive kernel.

structure HCPolySupport.ExactDualQOneFullTest {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) : Type

Full positive-top test functions for the negative q = 1 branch.

• g : Vec d → ℝ

  Test function.

• parentMemLp : MeasureTheory.MemLp self.g (ENNReal.ofReal (exactDualConjExponent P.p)) (normalizedCubeMeasure Q)
• norm_le_one : exactOverlapTopNorm P.positiveParameters Q self.g ⋯ ≤ 1

structure HCPolySupport.ExactDualQOneHattedTest {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) : Type

Mean-zero positive-top test functions for the hatted negative q = 1 branch.

• g : Vec d → ℝ

  Test function.

• parentMemLp : MeasureTheory.MemLp self.g (ENNReal.ofReal (exactDualConjExponent P.p)) (normalizedCubeMeasure Q)
• seminorm_le_one : exactOverlapTopSeminorm P.positiveParameters Q self.g ⋯ ≤ 1
• root_mean_zero : exactOverlapRootMean Q self.g ⋯ = 0

structure HCPolySupport.ExactDualFiniteFullTest {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) : Type

Full finite positive tests for the negative finite interior branch.

• g : Vec d → ℝ

  Test function.

• parentMemLp : MeasureTheory.MemLp self.g (ENNReal.ofReal (exactDualConjExponent P.p)) (normalizedCubeMeasure Q)
• norm_le_one : exactOverlapFiniteNorm P.positiveParameters Q self.g ⋯ ≤ 1

structure HCPolySupport.ExactDualFiniteHattedTest {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) : Type

Mean-zero finite positive tests for the hatted negative finite branch.

• g : Vec d → ℝ

  Test function.

• parentMemLp : MeasureTheory.MemLp self.g (ENNReal.ofReal (exactDualConjExponent P.p)) (normalizedCubeMeasure Q)
• seminorm_le_one : exactOverlapFiniteSeminorm P.positiveParameters Q self.g ⋯ ≤ 1
• root_mean_zero : exactOverlapRootMean Q self.g ⋯ = 0

structure HCPolySupport.ExactDualTopFullTest {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) : Type

Full finite positive tests with positive q' = 1 for the negative q = ∞ branch.

• g : Vec d → ℝ

  Test function.

• parentMemLp : MeasureTheory.MemLp self.g (ENNReal.ofReal (exactDualConjExponent P.p)) (normalizedCubeMeasure Q)
• norm_le_one : exactOverlapFiniteNorm P.positiveParameters Q self.g ⋯ ≤ 1

structure HCPolySupport.ExactDualTopHattedTest {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) : Type

Mean-zero finite positive tests with q' = 1 for the hatted negative q = ∞ branch.

• g : Vec d → ℝ

  Test function.

• parentMemLp : MeasureTheory.MemLp self.g (ENNReal.ofReal (exactDualConjExponent P.p)) (normalizedCubeMeasure Q)
• seminorm_le_one : exactOverlapFiniteSeminorm P.positiveParameters Q self.g ⋯ ≤ 1
• root_mean_zero : exactOverlapRootMean Q self.g ⋯ = 0

noncomputable def HCPolySupport.ExactDualQOneFullTest.pairing {d : ℕ} {P : ExactDualQOneParameters} {Q : TriadicCube d} {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (T : ExactDualQOneFullTest P Q) : ENNReal

The certified normalized pairing against a full q = 1 test.

Equations

• HCPolySupport.ExactDualQOneFullTest.pairing hf T = HCPolySupport.exactDualPairingFromHolder Q P.p f T.g ⋯ hf ⋯

noncomputable def HCPolySupport.ExactDualQOneHattedTest.pairing {d : ℕ} {P : ExactDualQOneParameters} {Q : TriadicCube d} {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (T : ExactDualQOneHattedTest P Q) : ENNReal

The certified normalized pairing against a hatted q = 1 test.

Equations

• HCPolySupport.ExactDualQOneHattedTest.pairing hf T = HCPolySupport.exactDualPairingFromHolder Q P.p f T.g ⋯ hf ⋯

noncomputable def HCPolySupport.ExactDualFiniteFullTest.pairing {d : ℕ} {P : ExactDualFiniteParameters} {Q : TriadicCube d} {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (T : ExactDualFiniteFullTest P Q) : ENNReal

The certified normalized pairing against a full finite test.

Equations

• HCPolySupport.ExactDualFiniteFullTest.pairing hf T = HCPolySupport.exactDualPairingFromHolder Q P.p f T.g ⋯ hf ⋯

noncomputable def HCPolySupport.ExactDualFiniteHattedTest.pairing {d : ℕ} {P : ExactDualFiniteParameters} {Q : TriadicCube d} {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (T : ExactDualFiniteHattedTest P Q) : ENNReal

The certified normalized pairing against a hatted finite test.

Equations

• HCPolySupport.ExactDualFiniteHattedTest.pairing hf T = HCPolySupport.exactDualPairingFromHolder Q P.p f T.g ⋯ hf ⋯

noncomputable def HCPolySupport.ExactDualTopFullTest.pairing {d : ℕ} {P : ExactDualTopParameters} {Q : TriadicCube d} {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (T : ExactDualTopFullTest P Q) : ENNReal

The certified normalized pairing against a full q = infinity test.

Equations

• HCPolySupport.ExactDualTopFullTest.pairing hf T = HCPolySupport.exactDualPairingFromHolder Q P.p f T.g ⋯ hf ⋯

noncomputable def HCPolySupport.ExactDualTopHattedTest.pairing {d : ℕ} {P : ExactDualTopParameters} {Q : TriadicCube d} {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (T : ExactDualTopHattedTest P Q) : ENNReal

The certified normalized pairing against a hatted q = infinity test.

Equations

• HCPolySupport.ExactDualTopHattedTest.pairing hf T = HCPolySupport.exactDualPairingFromHolder Q P.p f T.g ⋯ hf ⋯

noncomputable def HCPolySupport.exactDualQOneFullNorm {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : ENNReal

Exact negative q = 1 full dual norm.

Equations

• HCPolySupport.exactDualQOneFullNorm P Q f hf = ⨆ (T : HCPolySupport.ExactDualQOneFullTest P Q), HCPolySupport.ExactDualQOneFullTest.pairing hf T

noncomputable def HCPolySupport.exactDualQOneHattedSeminorm {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : ENNReal

Exact hatted negative q = 1 seminorm.

Equations

• HCPolySupport.exactDualQOneHattedSeminorm P Q f hf = ⨆ (T : HCPolySupport.ExactDualQOneHattedTest P Q), HCPolySupport.ExactDualQOneHattedTest.pairing hf T

noncomputable def HCPolySupport.exactDualFiniteFullNorm {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : ENNReal

Exact negative finite interior full dual norm.

Equations

• HCPolySupport.exactDualFiniteFullNorm P Q f hf = ⨆ (T : HCPolySupport.ExactDualFiniteFullTest P Q), HCPolySupport.ExactDualFiniteFullTest.pairing hf T

noncomputable def HCPolySupport.exactDualFiniteHattedSeminorm {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : ENNReal

Exact hatted negative finite interior seminorm.

Equations

• HCPolySupport.exactDualFiniteHattedSeminorm P Q f hf = ⨆ (T : HCPolySupport.ExactDualFiniteHattedTest P Q), HCPolySupport.ExactDualFiniteHattedTest.pairing hf T

noncomputable def HCPolySupport.exactDualTopFullNorm {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : ENNReal

Exact negative q = ∞ full dual norm.

Equations

• HCPolySupport.exactDualTopFullNorm P Q f hf = ⨆ (T : HCPolySupport.ExactDualTopFullTest P Q), HCPolySupport.ExactDualTopFullTest.pairing hf T

noncomputable def HCPolySupport.exactDualTopHattedSeminorm {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : ENNReal

Exact hatted negative q = ∞ seminorm.

Equations

• HCPolySupport.exactDualTopHattedSeminorm P Q f hf = ⨆ (T : HCPolySupport.ExactDualTopHattedTest P Q), HCPolySupport.ExactDualTopHattedTest.pairing hf T

theorem HCPolySupport.exactDualQOneFullNorm_eq {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : exactDualQOneFullNorm P Q f hf = ⨆ (T : ExactDualQOneFullTest P Q), ExactDualQOneFullTest.pairing hf T

theorem HCPolySupport.exactDualQOneHattedSeminorm_eq {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : exactDualQOneHattedSeminorm P Q f hf = ⨆ (T : ExactDualQOneHattedTest P Q), ExactDualQOneHattedTest.pairing hf T

theorem HCPolySupport.exactDualFiniteFullNorm_eq {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : exactDualFiniteFullNorm P Q f hf = ⨆ (T : ExactDualFiniteFullTest P Q), ExactDualFiniteFullTest.pairing hf T

theorem HCPolySupport.exactDualFiniteHattedSeminorm_eq {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : exactDualFiniteHattedSeminorm P Q f hf = ⨆ (T : ExactDualFiniteHattedTest P Q), ExactDualFiniteHattedTest.pairing hf T

theorem HCPolySupport.exactDualTopFullNorm_eq {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : exactDualTopFullNorm P Q f hf = ⨆ (T : ExactDualTopFullTest P Q), ExactDualTopFullTest.pairing hf T

theorem HCPolySupport.exactDualTopHattedSeminorm_eq {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : exactDualTopHattedSeminorm P Q f hf = ⨆ (T : ExactDualTopHattedTest P Q), ExactDualTopHattedTest.pairing hf T

theorem HCPolySupport.exactDualQOneFullNorm_congr_ae {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) {f f' : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (hff' : f =ᵐ[normalizedCubeMeasure Q] f') : exactDualQOneFullNorm P Q f hf = exactDualQOneFullNorm P Q f' ⋯

theorem HCPolySupport.exactDualQOneHattedSeminorm_congr_ae {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) {f f' : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (hff' : f =ᵐ[normalizedCubeMeasure Q] f') : exactDualQOneHattedSeminorm P Q f hf = exactDualQOneHattedSeminorm P Q f' ⋯

theorem HCPolySupport.exactDualFiniteFullNorm_congr_ae {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) {f f' : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (hff' : f =ᵐ[normalizedCubeMeasure Q] f') : exactDualFiniteFullNorm P Q f hf = exactDualFiniteFullNorm P Q f' ⋯

theorem HCPolySupport.exactDualFiniteHattedSeminorm_congr_ae {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) {f f' : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (hff' : f =ᵐ[normalizedCubeMeasure Q] f') : exactDualFiniteHattedSeminorm P Q f hf = exactDualFiniteHattedSeminorm P Q f' ⋯

theorem HCPolySupport.exactDualTopFullNorm_congr_ae {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) {f f' : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (hff' : f =ᵐ[normalizedCubeMeasure Q] f') : exactDualTopFullNorm P Q f hf = exactDualTopFullNorm P Q f' ⋯

theorem HCPolySupport.exactDualTopHattedSeminorm_congr_ae {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) {f f' : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (hff' : f =ᵐ[normalizedCubeMeasure Q] f') : exactDualTopHattedSeminorm P Q f hf = exactDualTopHattedSeminorm P Q f' ⋯

theorem HCPolySupport.exactDualFiniteSeminorm_zero {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) (hu : ExactOverlapIntegrable Q fun (x : Vec d) => 0) : exactOverlapFiniteSeminorm P Q (fun (x : Vec d) => 0) hu = 0

theorem HCPolySupport.exactDualTopSeminorm_zero {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) (hu : ExactOverlapIntegrable Q fun (x : Vec d) => 0) : exactOverlapTopSeminorm P Q (fun (x : Vec d) => 0) hu = 0

theorem HCPolySupport.exactDualFiniteNorm_zero {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) (hu : ExactOverlapIntegrable Q fun (x : Vec d) => 0) : exactOverlapFiniteNorm P Q (fun (x : Vec d) => 0) hu = 0

theorem HCPolySupport.exactDualTopNorm_zero {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) (hu : ExactOverlapIntegrable Q fun (x : Vec d) => 0) : exactOverlapTopNorm P Q (fun (x : Vec d) => 0) hu = 0

noncomputable def HCPolySupport.exactDualQOneFullZeroTest {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) : ExactDualQOneFullTest P Q

The zero full test in the exact q = 1 branch.

Equations

• HCPolySupport.exactDualQOneFullZeroTest P Q = { g := fun (x : HCPolySupport.Vec d) => 0, parentMemLp := ⋯, norm_le_one := ⋯ }

noncomputable def HCPolySupport.exactDualQOneHattedZeroTest {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) : ExactDualQOneHattedTest P Q

The zero hatted test in the exact q = 1 branch.

Equations

• HCPolySupport.exactDualQOneHattedZeroTest P Q = { g := fun (x : HCPolySupport.Vec d) => 0, parentMemLp := ⋯, seminorm_le_one := ⋯, root_mean_zero := ⋯ }

noncomputable def HCPolySupport.exactDualFiniteFullZeroTest {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) : ExactDualFiniteFullTest P Q

The zero full test in the finite interior branch.

Equations

• HCPolySupport.exactDualFiniteFullZeroTest P Q = { g := fun (x : HCPolySupport.Vec d) => 0, parentMemLp := ⋯, norm_le_one := ⋯ }

noncomputable def HCPolySupport.exactDualFiniteHattedZeroTest {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) : ExactDualFiniteHattedTest P Q

The zero hatted test in the finite interior branch.

Equations

• HCPolySupport.exactDualFiniteHattedZeroTest P Q = { g := fun (x : HCPolySupport.Vec d) => 0, parentMemLp := ⋯, seminorm_le_one := ⋯, root_mean_zero := ⋯ }

noncomputable def HCPolySupport.exactDualTopFullZeroTest {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) : ExactDualTopFullTest P Q

The zero full test in the q = infinity branch.

Equations

• HCPolySupport.exactDualTopFullZeroTest P Q = { g := fun (x : HCPolySupport.Vec d) => 0, parentMemLp := ⋯, norm_le_one := ⋯ }

noncomputable def HCPolySupport.exactDualTopHattedZeroTest {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) : ExactDualTopHattedTest P Q

The zero hatted test in the q = infinity branch.

Equations

• HCPolySupport.exactDualTopHattedZeroTest P Q = { g := fun (x : HCPolySupport.Vec d) => 0, parentMemLp := ⋯, seminorm_le_one := ⋯, root_mean_zero := ⋯ }

theorem HCPolySupport.exactDualQOneFullTest_nonempty {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) : Nonempty (ExactDualQOneFullTest P Q)

theorem HCPolySupport.exactDualQOneHattedTest_nonempty {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) : Nonempty (ExactDualQOneHattedTest P Q)

theorem HCPolySupport.exactDualFiniteFullTest_nonempty {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) : Nonempty (ExactDualFiniteFullTest P Q)

theorem HCPolySupport.exactDualFiniteHattedTest_nonempty {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) : Nonempty (ExactDualFiniteHattedTest P Q)

theorem HCPolySupport.exactDualTopFullTest_nonempty {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) : Nonempty (ExactDualTopFullTest P Q)

theorem HCPolySupport.exactDualTopHattedTest_nonempty {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) : Nonempty (ExactDualTopHattedTest P Q)

theorem HCPolySupport.exactDualZeroMemLp {d : ℕ} (Q : TriadicCube d) (p : ℝ) : MeasureTheory.MemLp (fun (x : Vec d) => 0) (ENNReal.ofReal p) (normalizedCubeMeasure Q)

The canonical parent-space certificate for zero data in any finite real exponent used by the exact dual objects.

theorem HCPolySupport.exactDualPairingFromHolder_zero_left {d : ℕ} (Q : TriadicCube d) (p : ℝ) (g : Vec d → ℝ) (hp : 1 < p) (hzero : MeasureTheory.MemLp (fun (x : Vec d) => 0) (ENNReal.ofReal p) (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g (ENNReal.ofReal (exactDualConjExponent p)) (normalizedCubeMeasure Q)) : exactDualPairingFromHolder Q p (fun (x : Vec d) => 0) g hp hzero hg = 0

theorem HCPolySupport.exactDualQOneFullNorm_zero {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) : exactDualQOneFullNorm P Q (fun (x : Vec d) => 0) ⋯ = 0

theorem HCPolySupport.exactDualQOneHattedSeminorm_zero {d : ℕ} (P : ExactDualQOneParameters) (Q : TriadicCube d) : exactDualQOneHattedSeminorm P Q (fun (x : Vec d) => 0) ⋯ = 0

theorem HCPolySupport.exactDualFiniteFullNorm_zero {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) : exactDualFiniteFullNorm P Q (fun (x : Vec d) => 0) ⋯ = 0

theorem HCPolySupport.exactDualFiniteHattedSeminorm_zero {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) : exactDualFiniteHattedSeminorm P Q (fun (x : Vec d) => 0) ⋯ = 0

theorem HCPolySupport.exactDualTopFullNorm_zero {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) : exactDualTopFullNorm P Q (fun (x : Vec d) => 0) ⋯ = 0

theorem HCPolySupport.exactDualTopHattedSeminorm_zero {d : ℕ} (P : ExactDualTopParameters) (Q : TriadicCube d) : exactDualTopHattedSeminorm P Q (fun (x : Vec d) => 0) ⋯ = 0