The consumer-facing Calderón--Zygmund decomposition certificate

The certificate records the maximal dyadic cubes and all estimates needed by the good/bad part argument. Its geometry is native to Vec3; no alternate Euclidean carrier is introduced.

instance CKN.Foundation.Euclidean.dyadicIndexCountable : Countable DyadicIndex

def CKN.Foundation.Euclidean.dyadicAncestor (Q : DyadicIndex) : ℕ → DyadicIndex

Iterated dyadic parent, with the original cube at generation zero.

Equations

• CKN.Foundation.Euclidean.dyadicAncestor Q 0 = Q
• CKN.Foundation.Euclidean.dyadicAncestor Q n.succ = CKN.Foundation.Euclidean.dyadicParent (CKN.Foundation.Euclidean.dyadicAncestor Q n)

def CKN.Foundation.Euclidean.dyadicCubeSet (Q : DyadicIndex) : Set Parabolic.Vec3

Half-open geometric cube represented by a dyadic index.

Equations

• CKN.Foundation.Euclidean.dyadicCubeSet Q = CKN.Foundation.Euclidean.dyadicCube Q.scale Q.corner

def CKN.Foundation.Euclidean.dyadicParentSet (Q : DyadicIndex) : Set Parabolic.Vec3

Geometric cube corresponding to the immediate dyadic parent.

Equations

• CKN.Foundation.Euclidean.dyadicParentSet Q = CKN.Foundation.Euclidean.dyadicCubeSet (CKN.Foundation.Euclidean.dyadicParent Q)

noncomputable def CKN.Foundation.Euclidean.dyadicAverage (F : Parabolic.Vec3 → ℝ) (Q : DyadicIndex) : ℝ

Signed average of a scalar function on a dyadic cube.

Equations

• CKN.Foundation.Euclidean.dyadicAverage F Q = ⨍ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Euclidean.dyadicCubeSet Q, F x

noncomputable def CKN.Foundation.Euclidean.dyadicAbsAverage (F : Parabolic.Vec3 → ℝ) (Q : DyadicIndex) : ℝ

Average absolute value on a dyadic cube, used in the stopping criterion.

Equations

• CKN.Foundation.Euclidean.dyadicAbsAverage F Q = ⨍ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Euclidean.dyadicCubeSet Q, |F x|

noncomputable def CKN.Foundation.Euclidean.dyadicL1Norm (F : Parabolic.Vec3 → ℝ) : ENNReal

Extended nonnegative integral of the absolute value for the dyadic decomposition.

Equations

• CKN.Foundation.Euclidean.dyadicL1Norm F = ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal |F x|

def CKN.Foundation.Euclidean.dyadicCubeMember (D : Set DyadicIndex) (x : Parabolic.Vec3) : Prop

Membership in the union of a chosen family of dyadic cubes.

Equations

• CKN.Foundation.Euclidean.dyadicCubeMember D x = ∃ Q ∈ D, x ∈ CKN.Foundation.Euclidean.dyadicCubeSet Q

noncomputable def CKN.Foundation.Euclidean.dyadicGoodPart (F : Parabolic.Vec3 → ℝ) (D : Set DyadicIndex) : Parabolic.Vec3 → ℝ

Good part obtained by replacing the function by its average on each selected cube.

Equations

• CKN.Foundation.Euclidean.dyadicGoodPart F D x = if hx : CKN.Foundation.Euclidean.dyadicCubeMember D x then CKN.Foundation.Euclidean.dyadicAverage F (Classical.choose hx) else F x

noncomputable def CKN.Foundation.Euclidean.dyadicBadPart (F : Parabolic.Vec3 → ℝ) (Q : DyadicIndex) : Parabolic.Vec3 → ℝ

Mean-zero bad part supported on one selected dyadic cube.

Equations

• CKN.Foundation.Euclidean.dyadicBadPart F Q = (CKN.Foundation.Euclidean.dyadicCubeSet Q).indicator fun (x : CKN.Foundation.Parabolic.Vec3) => F x - CKN.Foundation.Euclidean.dyadicAverage F Q

def CKN.Foundation.Euclidean.dyadicHigh (F : Parabolic.Vec3 → ℝ) (height : ℝ) (Q : DyadicIndex) : Prop

Stopping condition that the dyadic absolute average exceeds the chosen height.

Equations

• CKN.Foundation.Euclidean.dyadicHigh F height Q = (height < CKN.Foundation.Euclidean.dyadicAbsAverage F Q)

def CKN.Foundation.Euclidean.dyadicMaximalCubes (F : Parabolic.Vec3 → ℝ) (height : ℝ) : Set DyadicIndex

High-average cubes whose strict ancestors all fail the stopping condition.

Equations

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

theorem CKN.Foundation.Euclidean.abs_dyadicAverage_le_dyadicAbsAverage {F : Parabolic.Vec3 → ℝ} (Q : DyadicIndex) : |dyadicAverage F Q| ≤ dyadicAbsAverage F Q

theorem CKN.Foundation.Euclidean.dyadicMaximalCubes_spec {F : Parabolic.Vec3 → ℝ} (hF : MeasureTheory.Integrable F MeasureTheory.volume) {height : ℝ} (hheight : 0 < height) : have D := dyadicMaximalCubes F height; D.Countable ∧ D.Pairwise (Function.onFun Disjoint dyadicCubeSet) ∧ (∀ Q ∈ D, height < dyadicAbsAverage F Q) ∧ (∀ Q ∈ D, dyadicAbsAverage F Q ≤ 8 * height) ∧ (∀ Q ∈ D, dyadicAbsAverage F (dyadicParent Q) ≤ height) ∧ ∑' (Q : { Q : DyadicIndex // Q ∈ D }), MeasureTheory.volume (dyadicCubeSet ↑Q) ≤ dyadicL1Norm F / ENNReal.ofReal height ∧ (∀ᵐ (x : Parabolic.Vec3), x ∉ ⋃ Q ∈ D, dyadicCubeSet Q → |F x| ≤ height) ∧ ∀ᵐ (x : Parabolic.Vec3), |dyadicGoodPart F D x| ≤ 8 * height

structure CKN.Foundation.Euclidean.CZDecomposition (F : Parabolic.Vec3 → ℝ) (height : ℝ) : Type

Dyadic Calderón–Zygmund decomposition with quantitative good and bad part estimates.

• height_pos : 0 < height
• integrable : MeasureTheory.Integrable F MeasureTheory.volume
• cubes : Set DyadicIndex

  Selected dyadic cubes supporting the bad pieces of the decomposition.

• cubes_countable : self.cubes.Countable
• cubes_pairwise_disjoint : self.cubes.Pairwise (Function.onFun Disjoint dyadicCubeSet)
• cube_average_gt (Q : DyadicIndex) : Q ∈ self.cubes → height < dyadicAbsAverage F Q
• cube_average_le (Q : DyadicIndex) : Q ∈ self.cubes → dyadicAbsAverage F Q ≤ 8 * height
• parent_average_le (Q : DyadicIndex) : Q ∈ self.cubes → dyadicAbsAverage F (dyadicParent Q) ≤ height
• cube_volume_sum_le : ∑' (Q : { Q : DyadicIndex // Q ∈ self.cubes }), MeasureTheory.volume (dyadicCubeSet ↑Q) ≤ dyadicL1Norm F / ENNReal.ofReal height
• off_cubes_le_ae : ∀ᵐ (x : Parabolic.Vec3), x ∉ ⋃ Q ∈ self.cubes, dyadicCubeSet Q → |F x| ≤ height
• good_part_bound_ae : ∀ᵐ (x : Parabolic.Vec3), |dyadicGoodPart F self.cubes x| ≤ 8 * height
• good_part_l1_le : ∫⁻ (x : Parabolic.Vec3), ENNReal.ofReal |dyadicGoodPart F self.cubes x| ≤ dyadicL1Norm F
• bad_part_mean_zero (Q : DyadicIndex) : Q ∈ self.cubes → ∫ (x : Parabolic.Vec3) in dyadicCubeSet Q, dyadicBadPart F Q x = 0
• bad_part_l1_sum_le : ∑' (Q : { Q : DyadicIndex // Q ∈ self.cubes }), ∫⁻ (x : Parabolic.Vec3) in dyadicCubeSet ↑Q, ENNReal.ofReal |dyadicBadPart F (↑Q) x| ≤ 2 * dyadicL1Norm F

theorem CKN.Foundation.Euclidean.dyadicGoodPart_eq_of_not_mem {F : Parabolic.Vec3 → ℝ} {D : Set DyadicIndex} {x : Parabolic.Vec3} (hx : ¬dyadicCubeMember D x) : dyadicGoodPart F D x = F x

theorem CKN.Foundation.Euclidean.dyadicBadPart_support_subset {F : Parabolic.Vec3 → ℝ} (Q : DyadicIndex) : Function.support (dyadicBadPart F Q) ⊆ dyadicCubeSet Q

theorem CKN.Foundation.Euclidean.CZDecomposition.off_cubes_bound {F : Parabolic.Vec3 → ℝ} {height : ℝ} (D : CZDecomposition F height) : ∀ᵐ (x : Parabolic.Vec3), x ∉ ⋃ Q ∈ D.cubes, dyadicCubeSet Q → |F x| ≤ height

theorem CKN.Foundation.Euclidean.CZDecomposition.good_part_bound {F : Parabolic.Vec3 → ℝ} {height : ℝ} (D : CZDecomposition F height) : ∀ᵐ (x : Parabolic.Vec3), |dyadicGoodPart F D.cubes x| ≤ 8 * height

theorem CKN.Foundation.Euclidean.CZDecomposition.bad_part_mean {F : Parabolic.Vec3 → ℝ} {height : ℝ} (D : CZDecomposition F height) {Q : DyadicIndex} (hQ : Q ∈ D.cubes) : ∫ (x : Parabolic.Vec3) in dyadicCubeSet Q, dyadicBadPart F Q x = 0