Bounded-overlap integral estimates

The finite summation estimate used for the collar terms in eq:bu-gaussian-collar of the Escauriaza–Seregin–Šverák manuscript.

@[reducible, inline]

abbrev CKN.BUGaussianSpace : Type

The three-dimensional Gaussian spatial carrier used for the collar estimates.

Equations

• CKN.BUGaussianSpace = CKN.Foundation.Parabolic.L2Vec3

def CKN.buGaussianShell (ρ : ℝ) : Set BUGaussianSpace

The fixed-width spatial collar used in eq:bu-gaussian-collar (ESS).

Equations

• CKN.buGaussianShell ρ = {y : CKN.BUGaussianSpace | ρ - 1 < ‖y‖ ∧ ‖y‖ < ρ - 1 / 2}

theorem CKN.exists_buGaussian_shell_cover (ρ r : ℝ) (hr : 0 < r) (hrle : r ≤ 1 / 16) : ∃ (Y : Finset (Fin (Besicovitch.multiplicity BUGaussianSpace) × BUGaussianSpace)), (∀ p ∈ Y, ‖p.2‖ ≤ ρ - 1 / 2) ∧ (∀ y ∈ buGaussianShell ρ, ∃ p ∈ Y, dist y p.2 < r) ∧ (∀ p ∈ Y, Metric.ball p.2 (2 * r) ⊆ Metric.ball 0 ρ) ∧ ∀ (z : BUGaussianSpace), {p ∈ Y | dist z p.2 < 2 * r}.card ≤ Besicovitch.multiplicity BUGaussianSpace ^ 2

A finite shell cover whose doubled balls stay inside the localization ball. The overlap constant is Besicovitch.multiplicity squared and is independent of ρ and r.

def CKN.buGaussianTransitionShell (ρ : ℝ) : Set BUGaussianSpace

The closed transition annulus of the normalized Gaussian cutoff.

Equations

• CKN.buGaussianTransitionShell ρ = {y : CKN.BUGaussianSpace | 13 * ρ / 20 ≤ ‖y‖ ∧ ‖y‖ ≤ 3 * ρ / 4}

theorem CKN.exists_buGaussian_transition_cover (ρ r : ℝ) (hρ : 4 < ρ) (hr : 0 < r) (hrle : r ≤ 1 / 16) : ∃ (Y : Finset (Fin (Besicovitch.multiplicity BUGaussianSpace) × BUGaussianSpace)), (∀ p ∈ Y, ‖p.2‖ ≤ ρ - 1 / 2) ∧ (∀ p ∈ Y, 13 * ρ / 20 ≤ ‖p.2‖) ∧ (∀ y ∈ buGaussianTransitionShell ρ, ∃ p ∈ Y, dist y p.2 < r) ∧ (∀ p ∈ Y, Metric.ball p.2 (2 * r) ⊆ Metric.ball 0 ρ) ∧ ∀ (z : BUGaussianSpace), {p ∈ Y | dist z p.2 < 2 * r}.card ≤ Besicovitch.multiplicity BUGaussianSpace ^ 2

A finite cover of the closed transition annulus for the Gaussian cutoff. The overlap constant is Besicovitch.multiplicity squared.

theorem CKN.lintegral_sum_le_of_product_multiplicity_bound {α : Type u_1} {β : Type u_2} {ι : Type u_3} {κ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure (α × β)) (I : Finset ι) (J : Finset κ) (U : ι → Set α) (V : κ → Set β) (N K : ℕ) (f : α × β → ENNReal) (hf : AEMeasurable f μ) (hU : ∀ i ∈ I, MeasurableSet (U i)) (hV : ∀ j ∈ J, MeasurableSet (V j)) (hspace : ∀ (x : α), (∑ i ∈ I, if x ∈ U i then 1 else 0) ≤ N) (htime : ∀ (t : β), (∑ j ∈ J, if t ∈ V j then 1 else 0) ≤ K) : ∑ p ∈ I.product J, ∫⁻ (z : α × β) in U p.1 ×ˢ V p.2, f z ∂μ ≤ ↑(K * N) * ∫⁻ (z : α × β), f z ∂μ

Spatial and temporal overlap bounds multiply for a finite grid of product cells.

theorem CKN.integral_sum_le_of_product_multiplicity_bound {α : Type u_1} {β : Type u_2} {ι : Type u_3} {κ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure (α × β)) (I : Finset ι) (J : Finset κ) (U : ι → Set α) (V : κ → Set β) (N K : ℕ) (f : α × β → ℝ) (hf : MeasureTheory.Integrable f μ) (hfn : ∀ᵐ (z : α × β) ∂μ, 0 ≤ f z) (hU : ∀ i ∈ I, MeasurableSet (U i)) (hV : ∀ j ∈ J, MeasurableSet (V j)) (hspace : ∀ (x : α), (∑ i ∈ I, if x ∈ U i then 1 else 0) ≤ N) (htime : ∀ (t : β), (∑ j ∈ J, if t ∈ V j then 1 else 0) ≤ K) : ∑ p ∈ I.product J, ∫ (z : α × β) in U p.1 ×ˢ V p.2, f z ∂μ ≤ ↑(K * N) * ∫ (z : α × β), f z ∂μ

A real-valued nonnegative integrand obeys the same finite product overlap estimate, in the Bochner-integral form used by lem:caccioppoli.