DiskMaximalTools1.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SignedDisk.DiskMaximalTools.maximal_layer_coefficient line 24

theorem OAI.SignedDisk.DiskMaximalTools.strong_rationalMaximal line 44

Source documentation

A full strong p estimate from Vitali, truncation and Tonelli. No maximal inequality is supplied as an assumption. The real representative is controlled even before a separate almost-everywhere finiteness argument.

theorem strong_rationalMaximal {f : ℂ → ℝ} (hf : Measurable f)
    (hf0 : ∀ x, 0 ≤ f x) [IsFiniteMeasure (volume.withDensity (fun x => ENNReal.ofReal (f x)))]
    {p : ℝ} (hp : 1 < p) :
    (∫⁻ x, ENNReal.ofReal ((rationalMaximal (volume.withDensity (fun x => ENNReal.ofReal (f x))) x).toReal^p)) ≤
      ENNReal.ofReal (50*p*2^(p-1)/(p-1)) * (∫⁻ x, ENNReal.ofReal ((f x)^p)) := by
…

Mentions: OAI.SignedDisk.DiskMaximalTools.rationalMaximal

lemma OAI.SignedDisk.DiskMaximalTools.disk_average_le_rationalMaximal_exact line 98
theorem OAI.SignedDisk.DiskMaximalTools.all_radii_eq_rational line 143
Source documentation
Countability loses neither radii nor high values: the rational expression is exactly the centered disk maximal function of the measure.
```
theorem all_radii_eq_rational (ν : Measure ℂ) (x : ℂ) :
    (⨆ (r : ℝ) (_ : 0 < r), ν (ball x r)/volume (ball x r)) = rationalMaximal ν x := by
…
```
Mentions: OAI.SignedDisk.DiskMaximalTools.rationalMaximal
lemma OAI.SignedDisk.DiskMaximalTools.rationalMaximal_le_of_density_le line 159

theorem OAI.SignedDisk.ScalarCancellation.positive_residual line 185

Source documentation

A nonnegative scalar residual retaining exactly the net mass. Its removal has the exact cancellation defect as L1 cost.

theorem positive_residual {α : Type*} [MeasurableSpace α] {μ : Measure α}
    {h : α → ℝ} (hh : Integrable h μ) (hc : 0 ≤ ∫ x, h x ∂μ) :
    ∃ ρ : α → ℝ, Integrable ρ μ ∧ (∀ x, 0 ≤ ρ x) ∧
      (∀ x, ρ x ≤ max (h x) 0) ∧ (∫ x, ρ x ∂μ) = ∫ x, h x ∂μ ∧
      (∫ x, |h x-ρ x| ∂μ) = (∫ x, |h x| ∂μ) - ∫ x, h x ∂μ ∧
      (∀ x, h x = 0 → ρ x = 0) := by
…

theorem OAI.SignedDisk.ScalarCancellation.residual_split line 234

Source documentation

Every integrable scalar density splits into a constant-sign root and a zero-mass error, without replacing the actual terminal density by its mass.

theorem residual_split {α : Type*} [MeasurableSpace α] {μ : Measure α}
    {h : α → ℝ} (hh : Integrable h μ) :
    ∃ ρ β : α → ℝ, Integrable ρ μ ∧ Integrable β μ ∧
      (∀ x, h x = ρ x+β x) ∧ (∫ x, ρ x ∂μ) = ∫ x, h x ∂μ ∧
      (∫ x, β x ∂μ) = 0 ∧ (∫ x, |ρ x| ∂μ) = |∫ x, h x ∂μ| ∧
      (∫ x, |β x| ∂μ) = (∫ x, |h x| ∂μ)-|∫ x, h x ∂μ| ∧
      ((0 ≤ ∫ x, h x ∂μ) → ∀ x, 0 ≤ ρ x) ∧
      ((∫ x, h x ∂μ) < 0 → ∀ x, ρ x ≤ 0) ∧
      (∀ x, h x = 0 → ρ x = 0 ∧ β x = 0) := by
…

theorem OAI.SignedDisk.ScalarCancellation.refinement_residual line 275

Source documentation

One backward refinement step. The new cancelling piece has cost no larger than the scalar norm defect of the children; overlap can only lower this cost.

theorem refinement_residual {α ι : Type*} [MeasurableSpace α] {μ : Measure α}
    [Fintype ι] (w : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (ρ : ι → α → ℝ)
    (hρ : ∀ i, Integrable (ρ i) μ) :
    ∃ R β : α → ℝ, Integrable R μ ∧ Integrable β μ ∧
      (∀ x, (∑ i, w i*ρ i x) = R x+β x) ∧
      (∫ x, R x ∂μ) = ∑ i, w i*(∫ x, ρ i x ∂μ) ∧
      (∫ x, β x ∂μ) = 0 ∧
      (∫ x, |R x| ∂μ) = |∑ i, w i*(∫ x, ρ i x ∂μ)| ∧
      (∫ x, |β x| ∂μ) ≤
        (∑ i, w i*(∫ x, |ρ i x| ∂μ))-|∑ i, w i*(∫ x, ρ i x ∂μ)| ∧
      ((0 ≤ ∑ i, w i*(∫ x, ρ i x ∂μ)) → ∀ x, 0 ≤ R x) ∧
      (∀ x, (∀ i, w i*ρ i x = 0) → R x = 0 ∧ β x = 0) := by
…

def OAI.SignedDisk.ScalarCancellation.root line 321
Source documentation
Canonical positive/negative root selected from the proved scalar splitting, not an assumed decomposition.
```
def root (μ : Measure α) (f : α → ℝ) : α → ℝ := by
…
```
lemma OAI.SignedDisk.ScalarCancellation.root_spec line 325
def OAI.SignedDisk.ScalarCancellation.refined line 342
def OAI.SignedDisk.ScalarCancellation.roots line 346
def OAI.SignedDisk.ScalarCancellation.errors line 350
lemma OAI.SignedDisk.ScalarCancellation.refined_integrable line 354
lemma OAI.SignedDisk.ScalarCancellation.roots_integrable line 361
lemma OAI.SignedDisk.ScalarCancellation.roots_mass line 368
lemma OAI.SignedDisk.ScalarCancellation.roots_abs_mass line 379
lemma OAI.SignedDisk.ScalarCancellation.errors_integrable line 391
lemma OAI.SignedDisk.ScalarCancellation.errors_zero_mass line 400
theorem OAI.SignedDisk.ScalarCancellation.errors_cost line 417
Source documentation
The whole scalar cancellation tree is built by backward splitting. Each nonterminal zero-mass piece costs at most its positive refinement norm defect.
```
theorem errors_cost (w : ℕ → ι → ι → ℝ) (hw : ∀ k q s, 0 ≤ w k q s)
    {f : ι → α → ℝ} (hf : ∀ q, Integrable (f q) μ) (k : ℕ) (q : ι) :
    (∫ x, |errors μ w f (k+1) q x| ∂μ) ≤
      (∑ s, w k q s*|∫ x, refined w f k s x ∂μ|)-|∫ x, refined w f (k+1) q x ∂μ| := by
…
```
Mentions: OAI.SignedDisk.ScalarCancellation.errors, OAI.SignedDisk.ScalarCancellation.refined
lemma OAI.SignedDisk.ScalarCancellation.errors_terminal_cost line 442
lemma OAI.SignedDisk.ScalarCancellation.error_recurrence line 447

theorem OAI.SignedDisk.ScalarCancellation.roots_errors_support line 455

Source documentation

Support nesting is preserved by the new construction, even when child scalar masses vanish or overlapping densities cancel each other.

theorem roots_errors_support (w : ℕ → ι → ι → ℝ) {f : ι → α → ℝ}
    (hf : ∀ q, Integrable (f q) μ) (S : ℕ → ι → Set α)
    (hfS : ∀ q x, x ∉ S 0 q → f q x = 0)
    (hS : ∀ k q s, w k q s ≠ 0 → S k s ⊆ S (k+1) q) :
    ∀ k q x, x ∉ S k q → roots μ w f k q x = 0 ∧ errors μ w f k q x = 0 := by
…

Mentions: OAI.SignedDisk.ScalarCancellation.roots, OAI.SignedDisk.ScalarCancellation.errors