OAI/Analysis/SignedDisk/DiskMaximalTools2.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedDisk.DiskMaximalTools.strong_three_halves_norm line 32
2. lemma OAI.SignedDisk.DiskMaximalTools.lintegral_le_three_halves_norm line 54
3. theorem OAI.SignedDisk.PlanePotential.local_value_lp line 77

   Source documentation

   The complete local L^(3/2) value estimate for a genuine finite vector cancellation decomposition, with the common 1/100 price.

   theorem local_value_lp : ∃ C : ℝ, 0 < C ∧
       ∀ {ι : Type} [Fintype ι] (b : ι → ErrorPiece 2) {g : ℂ → ℝ},
       ContDiff ℝ 1 g → (∃ D : ℝ, ∀ y, ‖fderiv ℝ g y‖ ≤ D) →
       (∀ᵐ y, ‖y‖ ≤ 8 → gradient g y = ∑ i, (b i).density y) →
       ∃ c : ℝ, eLpNorm (fun x => g x-c) (3/2) (volume.restrict {x : ℂ | ‖x‖ ≤ 8}) ≤
         ENNReal.ofReal (C * errorPrice b (1/100)) := by
   …

4. lemma OAI.SignedDisk.DiskMoments.signedAverage_sub_const line 106
5. lemma OAI.SignedDisk.DiskMoments.local_average_le line 120

   Source documentation

   A true disk average of a continuous function is controlled by the local absolute-density maximal function. No maximizing-radius selection is used.

   lemma local_average_le {g : ℂ → ℝ} (hg : Continuous g) (c : ℝ)
       {x : ℂ} (hx : ‖x‖ ≤ 2) {t : ℝ} (ht : 0 < t) (ht4 : t ≤ 4) :
       ENNReal.ofReal |signedAverage g x t-c| ≤
         rationalMaximal (volume.withDensity (fun y => ENNReal.ofReal
           (({y : ℂ | ‖y‖ ≤ 8}.indicator (fun y => |g y-c|)) y))) x := by
   …

   Mentions: OAI.SignedDisk.DiskMoments.signedAverage

6. theorem OAI.SignedDisk.PlanePotential.local_value_majorant line 162

   Source documentation

   Full local value-oscillation price, for every pair of positive radii at most four. The measurable majorant is an actual centered Euclidean disk maximal function, not an assumed analytic input.

   theorem local_value_majorant : ∃ C : ℝ, 0 < C ∧
       ∀ {ι : Type} [Fintype ι] (b : ι → ErrorPiece 2) {g : ℂ → ℝ},
       ContDiff ℝ 1 g → (∃ D : ℝ, ∀ y, ‖fderiv ℝ g y‖ ≤ D) →
       (∀ᵐ y, ‖y‖ ≤ 8 → gradient g y = ∑ i, (b i).density y) →
       ∀ Q : Set ℂ, volume Q ≤ ENNReal.ofReal 1 →
       ∃ F : ℂ → ℝ≥0∞, Measurable F ∧
         (∫⁻ x in Q, F x) ≤ ENNReal.ofReal (C*errorPrice b (1/100)) ∧
         ∀ x, ‖x‖ ≤ 2 → ∀ t t', 0 < t → t ≤ 4 → 0 < t' → t' ≤ 4 →
           ENNReal.ofReal |signedAverage g x t-signedAverage g x t'| ≤ F x := by
   …

7. lemma OAI.SignedDisk.AffineDensities.fderiv_affine_bound line 234
8. theorem OAI.SignedDisk.CommonPrices.value_cell_price line 255

   Source documentation

   The actual common-price value estimate, including every terminal error and all roots. This is the third local analytic input to signed run assembly.

   theorem value_cell_price : ∃ C : ℝ, 0 < C ∧
       ∀ {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R) (hN : R/r+1 ≤ (N:ℝ))
       {g : ℂ → ℝ}, ContDiff ℝ 1 g → Integrable (gradient g) →
       (∀ y, gradient g y ≠ 0 → ‖y‖ ≤ R) →
       (∃ D : ℝ, ∀ y, ‖fderiv ℝ g y‖ ≤ D) → ∀ (k : ℕ) (p : ℤ × ℤ)
       {n : ℂ}, n ∈ fixedPalette.labels → ∀ Q : Set ℂ, volume Q ≤ ENNReal.ofReal 1 →
       ∃ F : ℂ → ℝ≥0∞, Measurable F ∧
         (∫⁻ X in Q, F X) ≤ ENNReal.ofReal (C*(scale r k)⁻¹*
           (rootMass (gradient g) r k (cellRoots N p)+cellPrice N r (gradient g) k (cellRoots N p))) ∧
         ∀ X, ‖X‖ ≤ 2 → ∀ t t', 0 < t → t ≤ 4 → 0 < t' → t' ≤ 4 →
           ENNReal.ofReal |signedAverage (fun Y => g (point (scale r k) p+scale r k • Y)) X t-
             signedAverage (fun Y => g (point (scale r k) p+scale r k • Y)) X t'| ≤ F X := by
   …

   Mentions: OAI.SignedDisk.CommonPrices.rootMass, OAI.SignedDisk.CommonPrices.cellRoots, OAI.SignedDisk.CommonPrices.cellPrice

9. def OAI.SignedDisk.PhysicalCells.unitCell line 295
10. def OAI.SignedDisk.PhysicalCells.toUnit line 296
11. def OAI.SignedDisk.PhysicalCells.cell line 297
12. lemma OAI.SignedDisk.PhysicalCells.unitCell_measurable line 299
13. lemma OAI.SignedDisk.PhysicalCells.toUnit_continuous line 301
14. lemma OAI.SignedDisk.PhysicalCells.cell_measurable line 302
15. lemma OAI.SignedDisk.PhysicalCells.volume_unitCell line 304
16. lemma OAI.SignedDisk.PhysicalCells.norm_unitCell line 312
17. lemma OAI.SignedDisk.PhysicalCells.toUnit_affine line 316
18. lemma OAI.SignedDisk.PhysicalCells.affine_toUnit line 318
19. lemma OAI.SignedDisk.PhysicalCells.lintegral_smul line 321
20. lemma OAI.SignedDisk.PhysicalCells.lintegral_toUnit line 329
21. lemma OAI.SignedDisk.PhysicalCells.lintegral_cell line 338

    Source documentation

    Exact physical-space change of variables, with the two-dimensional volume factor and no integrability or measurability assumptions on the majorant.

    lemma lintegral_cell (F : ℂ → ℝ≥0∞) (p : ℂ) {r : ℝ} (hr : r ≠ 0) :
        (∫⁻ y in cell p r, F y) = ENNReal.ofReal (r^2)*∫⁻ X in unitCell, F (p+r • X) := by
    …

    Mentions: OAI.SignedDisk.PhysicalCells.cell, OAI.SignedDisk.PhysicalCells.unitCell

22. lemma OAI.SignedDisk.PhysicalCells.cell_majorant line 349
23. lemma OAI.SignedDisk.DiskMoments.signedAverage_affine line 356
24. lemma OAI.SignedDisk.DiskMoments.gradient_signedAverage line 367
25. lemma OAI.SignedDisk.DiskMoments.gradient_average_affine line 384
26. def OAI.SignedDisk.DiskMoments.PhysicalNeighborhoodRadius line 396
27. def OAI.SignedDisk.DiskMoments.PhysicalEndpointRadius line 399
28. lemma OAI.SignedDisk.DiskMoments.neighborhoodRadius_affine line 402
29. lemma OAI.SignedDisk.DiskMoments.endpointRadius_affine line 414