Documentation

The value of one competitor in the discrete cube vector K-functional.

Equations

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

Instances For

noncomputable def HCPolySupport.cubeVectorKFunctional {d : ℕ} (Q : TriadicCube d) (t : ℝ) (F : Vec d → Vec d) :

Discrete cube K-functional for vector fields, with t as the smoothing scale.

Equations

HCPolySupport.cubeVectorKFunctional Q t F = sInf (Set.range fun (G : HCPolySupport.CubeVectorH1Function Q) => HCPolySupport.cubeVectorKFunctionalCompetitorValue Q t F G)

Instances For

theorem HCPolySupport.cubeVectorKFunctionalCompetitorValue_nonneg {d : ℕ} (Q : TriadicCube d) (t : ℝ) (F : Vec d → Vec d) (G : CubeVectorH1Function Q) :

0 ≤ cubeVectorKFunctionalCompetitorValue Q t F G

theorem HCPolySupport.sqrt_overlappingPositiveDepthMean_le_mul_KFunctionalCompetitorValue {d : ℕ} {C : ℝ} (hC : 0 ≤ C) (hPoincare : CubeVectorH1OverlapPoincareEstimate d C) (Q : TriadicCube d) (F : Vec d → Vec d) (j : ℕ) (G : CubeVectorH1Function Q) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) :

√(cubeBesovOverlappingPositiveVectorDepthAverage Q F j) ≤ (8 * 3 ^ d + 2 * C ^ 2 + 1) * cubeVectorKFunctionalCompetitorValue Q (Real.rpow 3 (-↑j)) F G

theorem HCPolySupport.cubeVectorKFunctional_range_nonempty {d : ℕ} (Q : TriadicCube d) (t : ℝ) (F : Vec d → Vec d) :

(Set.range fun (G : CubeVectorH1Function Q) => cubeVectorKFunctionalCompetitorValue Q t F G).Nonempty

theorem HCPolySupport.cubeVectorKFunctional_range_bddBelow {d : ℕ} (Q : TriadicCube d) (t : ℝ) (F : Vec d → Vec d) :

BddBelow (Set.range fun (G : CubeVectorH1Function Q) => cubeVectorKFunctionalCompetitorValue Q t F G)

theorem HCPolySupport.cubeVectorKFunctional_nonneg {d : ℕ} (Q : TriadicCube d) (t : ℝ) (F : Vec d → Vec d) :

0 ≤ cubeVectorKFunctional Q t F

theorem HCPolySupport.cubeVectorKFunctional_le_competitor {d : ℕ} (Q : TriadicCube d) (t : ℝ) (F : Vec d → Vec d) (G : CubeVectorH1Function Q) :

cubeVectorKFunctional Q t F ≤ cubeVectorKFunctionalCompetitorValue Q t F G

theorem HCPolySupport.cubeVectorKFunctionalCompetitorValue_le_of_endpoint_bounds {d : ℕ} (Q : TriadicCube d) (t C : ℝ) (F H : Vec d → Vec d) (V G : CubeVectorH1Function Q) (hC : 0 ≤ C) (hL2 : (cubeLpNorm Q 2 fun (x : Vec d) => F x - V.toField x) ≤ C * cubeLpNorm Q 2 fun (x : Vec d) => H x - G.toField x) (hGrad : V.gradientCoordL2NormSum ≤ C * G.gradientCoordL2NormSum) :

cubeVectorKFunctionalCompetitorValue Q t F V ≤ C * cubeVectorKFunctionalCompetitorValue Q t H G

theorem HCPolySupport.cubeVectorKFunctional_le_of_forall_competitorValue_le {d : ℕ} (Q : TriadicCube d) (t C : ℝ) (F H : Vec d → Vec d) (hC : 0 ≤ C) (hcomp : ∀ (G : CubeVectorH1Function Q), ∃ (V : CubeVectorH1Function Q), cubeVectorKFunctionalCompetitorValue Q t F V ≤ C * cubeVectorKFunctionalCompetitorValue Q t H G) :

cubeVectorKFunctional Q t F ≤ C * cubeVectorKFunctional Q t H

noncomputable def HCPolySupport.cubeKBesovVectorDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (j : ℕ) :

Depth-j K-functional contribution to the positive q = 2 scale.

Equations

HCPolySupport.cubeKBesovVectorDepthSeminorm Q s F j = Real.rpow 3 (s * ↑j) * HCPolySupport.cubeVectorKFunctional Q (Real.rpow 3 (-↑j)) F

Instances For

theorem HCPolySupport.cubeKBesovVectorDepthSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (j : ℕ) :

0 ≤ cubeKBesovVectorDepthSeminorm Q s F j

theorem HCPolySupport.sqrt_cubeBesovOverlappingPositiveVectorDepthAverage_le_mul_cubeVectorKFunctional {d : ℕ} (Q : TriadicCube d) (C : ℝ) (F : Vec d → Vec d) (j : ℕ) (hC : 0 ≤ C) (hcomp : ∀ (G : CubeVectorH1Function Q), √(cubeBesovOverlappingPositiveVectorDepthAverage Q F j) ≤ C * cubeVectorKFunctionalCompetitorValue Q (Real.rpow 3 (-↑j)) F G) :

√(cubeBesovOverlappingPositiveVectorDepthAverage Q F j) ≤ C * cubeVectorKFunctional Q (Real.rpow 3 (-↑j)) F

theorem HCPolySupport.overlappingPositiveDepthSeminorm_le_mul_KBesovVectorDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s C : ℝ) (F : Vec d → Vec d) (j : ℕ) (hC : 0 ≤ C) (hcomp : ∀ (G : CubeVectorH1Function Q), √(cubeBesovOverlappingPositiveVectorDepthAverage Q F j) ≤ C * cubeVectorKFunctionalCompetitorValue Q (Real.rpow 3 (-↑j)) F G) :

cubeBesovOverlappingPositiveVectorDepthSeminorm Q s F j ≤ C * cubeKBesovVectorDepthSeminorm Q s F j

theorem HCPolySupport.cubeKBesovVectorDepthSeminorm_le_of_kFunctional_le {d : ℕ} (Q : TriadicCube d) (s C : ℝ) (F G : Vec d → Vec d) (j : ℕ) (hK : cubeVectorKFunctional Q (Real.rpow 3 (-↑j)) F ≤ C * cubeVectorKFunctional Q (Real.rpow 3 (-↑j)) G) :

cubeKBesovVectorDepthSeminorm Q s F j ≤ C * cubeKBesovVectorDepthSeminorm Q s G j

noncomputable def HCPolySupport.cubeKBesovVectorPartialSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (F : Vec d → Vec d) :

Finite-depth discrete K-functional Besov seminorm.

Equations

HCPolySupport.cubeKBesovVectorPartialSeminormTwo Q s N F = √(∑ j ∈ Finset.range (N + 1), HCPolySupport.cubeKBesovVectorDepthSeminorm Q s F j ^ 2)

Instances For

theorem HCPolySupport.cubeKBesovVectorPartialSeminormTwo_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (F : Vec d → Vec d) :

0 ≤ cubeKBesovVectorPartialSeminormTwo Q s N F

theorem HCPolySupport.sq_cubeKBesovVectorPartialSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (F : Vec d → Vec d) :

cubeKBesovVectorPartialSeminormTwo Q s N F ^ 2 = ∑ j ∈ Finset.range (N + 1), cubeKBesovVectorDepthSeminorm Q s F j ^ 2

theorem HCPolySupport.cubeKBesovVectorPartialSeminormTwo_le_of_forall_depthSeminorm_le {d : ℕ} (Q : TriadicCube d) (s C : ℝ) (N : ℕ) (F G : Vec d → Vec d) (hC : 0 ≤ C) (hdepth : ∀ j ∈ Finset.range (N + 1), cubeKBesovVectorDepthSeminorm Q s F j ≤ C * cubeKBesovVectorDepthSeminorm Q s G j) :

cubeKBesovVectorPartialSeminormTwo Q s N F ≤ C * cubeKBesovVectorPartialSeminormTwo Q s N G

theorem HCPolySupport.cubeKBesovVectorPartialSeminormTwo_le_of_forall_kFunctional_le {d : ℕ} (Q : TriadicCube d) (s C : ℝ) (N : ℕ) (F G : Vec d → Vec d) (hC : 0 ≤ C) (hK : ∀ j ∈ Finset.range (N + 1), cubeVectorKFunctional Q (Real.rpow 3 (-↑j)) F ≤ C * cubeVectorKFunctional Q (Real.rpow 3 (-↑j)) G) :

cubeKBesovVectorPartialSeminormTwo Q s N F ≤ C * cubeKBesovVectorPartialSeminormTwo Q s N G

theorem HCPolySupport.overlappingPositivePartialSeminormTwo_le_mul_KPartialSeminormTwo_of_forall {d : ℕ} (Q : TriadicCube d) (s C : ℝ) (N : ℕ) (F : Vec d → Vec d) (hC : 0 ≤ C) (hdepth : ∀ j ∈ Finset.range (N + 1), cubeBesovOverlappingPositiveVectorDepthSeminorm Q s F j ≤ C * cubeKBesovVectorDepthSeminorm Q s F j) :

cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N F ≤ C * cubeKBesovVectorPartialSeminormTwo Q s N F

theorem HCPolySupport.overlappingPositivePartialSeminormTwo_le_mul_KPartialSeminormTwo {d : ℕ} (Q : TriadicCube d) (s C : ℝ) (N : ℕ) (F : Vec d → Vec d) (hC : 0 ≤ C) (hcomp : ∀ j ∈ Finset.range (N + 1), ∀ (G : CubeVectorH1Function Q), √(cubeBesovOverlappingPositiveVectorDepthAverage Q F j) ≤ C * cubeVectorKFunctionalCompetitorValue Q (Real.rpow 3 (-↑j)) F G) :

cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N F ≤ C * cubeKBesovVectorPartialSeminormTwo Q s N F

theorem HCPolySupport.overlappingPositivePartialSeminormTwo_le_mul_of_overlapPoincare {d : ℕ} {C : ℝ} (hC : 0 ≤ C) (hPoincare : CubeVectorH1OverlapPoincareEstimate d C) (Q : TriadicCube d) (s : ℝ) (N : ℕ) (F : Vec d → Vec d) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) :

cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N F ≤ (8 * 3 ^ d + 2 * C ^ 2 + 1) * cubeKBesovVectorPartialSeminormTwo Q s N F

theorem HCPolySupport.KPartialSeminormTwo_le_mul_overlappingPositivePartialSeminormTwo {d : ℕ} (Q : TriadicCube d) (s C : ℝ) (N : ℕ) (F : Vec d → Vec d) (hC : 0 ≤ C) (hdepth : ∀ j ∈ Finset.range (N + 1), cubeKBesovVectorDepthSeminorm Q s F j ≤ C * cubeBesovOverlappingPositiveVectorDepthSeminorm Q s F j) :

cubeKBesovVectorPartialSeminormTwo Q s N F ≤ C * cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N F

Assemble the reverse finite-level comparison from a depthwise K-functional bound by the corrected overlapping depth seminorm.

This is the square-sum part of the remaining interpolation proof. The hard analytic construction still has to provide the depthwise estimate, but once it does, no additional summability argument is needed.

noncomputable def HCPolySupport.cubeKBesovVectorSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) :

Full discrete K-functional Besov seminorm.

Equations

HCPolySupport.cubeKBesovVectorSeminormTwo Q s F = sSup (Set.range fun (N : ℕ) => HCPolySupport.cubeKBesovVectorPartialSeminormTwo Q s N F)

Instances For

theorem HCPolySupport.cubeKBesovVectorSeminormTwo_le_of_partialBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) {B : ℝ} (hB : ∀ (N : ℕ), cubeKBesovVectorPartialSeminormTwo Q s N F ≤ B) :

cubeKBesovVectorSeminormTwo Q s F ≤ B

theorem HCPolySupport.cubeKBesovVectorPartialSeminormTwo_le_seminorm_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeKBesovVectorPartialSeminormTwo Q s N F)) (N : ℕ) :

cubeKBesovVectorPartialSeminormTwo Q s N F ≤ cubeKBesovVectorSeminormTwo Q s F

theorem HCPolySupport.cubeKBesovVectorSeminormTwo_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeKBesovVectorPartialSeminormTwo Q s N F)) :

0 ≤ cubeKBesovVectorSeminormTwo Q s F

theorem HCPolySupport.cubeKBesovVectorSeminormTwo_le_of_forall_partialSeminormTwo_le {d : ℕ} (Q : TriadicCube d) (s C : ℝ) (F G : Vec d → Vec d) (hC : 0 ≤ C) (hG_bdd : BddAbove (Set.range fun (N : ℕ) => cubeKBesovVectorPartialSeminormTwo Q s N G)) (hpartial : ∀ (N : ℕ), cubeKBesovVectorPartialSeminormTwo Q s N F ≤ C * cubeKBesovVectorPartialSeminormTwo Q s N G) :

cubeKBesovVectorSeminormTwo Q s F ≤ C * cubeKBesovVectorSeminormTwo Q s G

theorem HCPolySupport.cubeKBesovVectorSeminormTwo_le_of_forall_kFunctional_le {d : ℕ} (Q : TriadicCube d) (s C : ℝ) (F G : Vec d → Vec d) (hC : 0 ≤ C) (hG_bdd : BddAbove (Set.range fun (N : ℕ) => cubeKBesovVectorPartialSeminormTwo Q s N G)) (hK : ∀ (j : ℕ), cubeVectorKFunctional Q (Real.rpow 3 (-↑j)) F ≤ C * cubeVectorKFunctional Q (Real.rpow 3 (-↑j)) G) :

cubeKBesovVectorSeminormTwo Q s F ≤ C * cubeKBesovVectorSeminormTwo Q s G

noncomputable def HCPolySupport.cubeKBesovVectorNormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) :

Full discrete K-functional Besov norm with the same mean term as the note-normalized positive triadic norm.

Equations

HCPolySupport.cubeKBesovVectorNormTwo Q s F = √(HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec Q F)) + HCPolySupport.cubeKBesovVectorSeminormTwo Q s F

Instances For

theorem HCPolySupport.cubeKBesovVectorNormTwo_le_of_average_and_seminorm {d : ℕ} (Q : TriadicCube d) (s C : ℝ) (F G : Vec d → Vec d) (havg : √(vecNormSq (cubeAverageVec Q F)) ≤ C * √(vecNormSq (cubeAverageVec Q G))) (hsemi : cubeKBesovVectorSeminormTwo Q s F ≤ C * cubeKBesovVectorSeminormTwo Q s G) :

cubeKBesovVectorNormTwo Q s F ≤ C * cubeKBesovVectorNormTwo Q s G

noncomputable def HCPolySupport.cubeKBesovNormModel (d : ℕ) :

CubeKBesovNormModel d

The canonical K-functional Besov norm model used by the revised proof.

Equations

HCPolySupport.cubeKBesovNormModel d Q s F = HCPolySupport.cubeKBesovVectorNormTwo Q s F

Instances For

def HCPolySupport.CubeKBesovOverlappingEquivalence {d : ℕ} (K : CubeKBesovNormModel d) :

Pure function-space bridge between a K-functional Besov norm and the corrected overlapping positive B^s_{2,2} norm.

Equations

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

Instances For

def HCPolySupport.CubeKBesovDirichletRegularity {d : ℕ} (K : CubeKBesovNormModel d) :

K-functional regularity estimate for the Dirichlet divergence solution operator. This is the PDE-plus-K-functional part of the revised proof, before the pure norm-equivalence bridge back to the triadic Besov norm.

Equations

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

Instances For

def HCPolySupport.CubeKBesovDirichletRegularityUniform {d : ℕ} (K : CubeKBesovNormModel d) (C : ℝ) :

Uniform-in-s version of CubeKBesovDirichletRegularity. This is the form needed by downstream arguments which must track the entire s-profile instead of choosing a fresh constant after s has been fixed.

Equations

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

Instances For

CubeKBesovDirichletRegularity K

theorem HCPolySupport.CubeKBesovDirichletRegularityUniform.to_dirichletRegularity {d : ℕ} {K : CubeKBesovNormModel d} {C : ℝ} (h : CubeKBesovDirichletRegularityUniform K C) :

def HCPolySupport.CubeKBesovInputBoundednessOfOverlappingHRegularity (d : ℕ) :

Boundedness bridge needed to read the sSup defining the K-functional Besov seminorm as a genuine supremum for inputs known to have the corrected overlapping positive Besov regularity.

Equations

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

Instances For

def HCPolySupport.CubeKBesovPartialBoundByOverlappingPositive (d : ℕ) :

Finite-level pure K/overlapping comparison strong enough to make the sSup-based K-functional seminorm honest on every datum with overlapping positive Besov regularity.

This is the boundedness half of the pure Besov theory in a form that avoids talking about the full K-seminorm before boundedness has been established.

Equations

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

Instances For

def HCPolySupport.CubeKBesovPartialBoundByOverlappingPositiveUniform (d : ℕ) (C : ℝ) :

Uniform-in-s finite-level K/overlap comparison.

Equations

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

Instances For

CubeKBesovPartialBoundByOverlappingPositive d

theorem HCPolySupport.CubeKBesovPartialBoundByOverlappingPositiveUniform.to_partialBound {d : ℕ} {C : ℝ} (h : CubeKBesovPartialBoundByOverlappingPositiveUniform d C) :

def HCPolySupport.CubeKBesovOverlapAveragingCompetitorEstimate (d : ℕ) (C : ℝ) :

One-depth competitor estimate expected from the overlap averaging operator.

For every parent cube, field, and depth, there is an H¹ competitor whose residual and scaled gradient are both controlled by the corrected overlapping oscillation at that depth.

Equations

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

Instances For

def HCPolySupport.CubeKBesovDepthBoundByOverlappingPositive (d : ℕ) :

Depthwise reverse K/overlap estimate supplied by the planned smoothing operator.

This is now the precise analytic target for the hard interpolation step: build an H¹ competitor at scale 3^{-j} whose K-functional value is controlled by the corrected overlapping oscillation at the same depth.

Equations

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

Instances For

def HCPolySupport.CubeKBesovDepthBoundByOverlappingPositiveUniform (d : ℕ) (C : ℝ) :

Uniform-in-s depthwise K/overlap comparison.

Equations

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

Instances For

CubeKBesovDepthBoundByOverlappingPositive d

theorem HCPolySupport.CubeKBesovDepthBoundByOverlappingPositiveUniform.to_depthBound {d : ℕ} {C : ℝ} (h : CubeKBesovDepthBoundByOverlappingPositiveUniform d C) :

theorem HCPolySupport.cubeKBesovDepthBoundByOverlappingPositiveUniform_of_overlapAveragingCompetitorEstimate {d : ℕ} {C : ℝ} (hC : 0 ≤ C) (hcomp : CubeKBesovOverlapAveragingCompetitorEstimate d C) :

CubeKBesovDepthBoundByOverlappingPositiveUniform d (2 * C)

Uniform residual-plus-gradient control implies the uniform depthwise K/overlap estimate.