OAI/Analysis/DiskMaximal/Potentials.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanePotential.green_restrict_density line 57
2. lemma OAI.PlanePotential.green_root_lp_local line 66
3. lemma OAI.PlanePotential.green_zero_piece_lp_ae line 93
4. theorem OAI.PlanePotential.green_decomposition_norm_local line 126

   Source documentation

   The local decomposition theorem does not demand artificial bounded support of the original densities: the actual Green kernel vanishes outside the observation ball.

   theorem green_decomposition_norm_local {ι : Type*} [Fintype ι]
       {ψ g : ℂ → ℝ} (hψ : Continuous ψ) (hψc : HasCompactSupport ψ)
       (hg : ContDiff ℝ 1 g) {D R X B : ℝ}
       (hD : ∀ y, ‖fderiv ℝ g y‖ ≤ D) (hψ1 : ∫ z, ψ z = 1)
       (hψs : ∀ z, ψ z ≠ 0 → ‖z‖ ≤ R) (hψB : ∀ z, |ψ z| ≤ B)
       (hRX : R ≤ X) (hM : 0 < R+X) (hB : 0 ≤ B) (hX : 0 < X)
       (β : ι → ℂ → ℂ) (hβ : ∀ i, Integrable (β i))
       (hdecomp : ∀ᵐ y, ‖y‖ ≤ X → gradient g y = ∑ i, β i y) :
       eLpNorm (fun x => g x-∫ z, ψ z*g z) (3/2) (volume.restrict {x : ℂ | ‖x‖ ≤ X}) ≤
         ∑ i, eLpNorm (fun x => ∫ y, ⟪green ψ x y,β i y⟫) (3/2)
           (volume.restrict {x : ℂ | ‖x‖ ≤ X}) := by
   …

   Mentions: OAI.PlanePotential.green

5. theorem OAI.PlanePotential.exists_green_price line 156

   Source documentation

   Uniform fractional small-support gain expressed in the common price exponent 1/100, including the unrestricted unit-size terms.

   theorem exists_green_price : ∃ (ψ : ℂ → ℝ) (C : ℝ), 0 < C ∧
       ContDiff ℝ ∞ ψ ∧ HasCompactSupport ψ ∧ (∫ z, ψ z) = 1 ∧
       (∀ z, ψ z ≠ 0 → ‖z‖ ≤ 1) ∧
       ∀ b : ErrorPiece 2,
         eLpNorm (fun x => ∫ y, ⟪green ψ x y,b.density y⟫) (3/2)
           (volume.restrict {x : ℂ | ‖x‖ ≤ 8}) ≤
           ENNReal.ofReal (C*b.size^(1/100:ℝ)*b.mass) := by
   …

   Mentions: OAI.PlanePotential.green

6. lemma OAI.DiskMaximalTools.strong_three_halves_norm line 215
7. lemma OAI.DiskMaximalTools.lintegral_le_three_halves_norm line 237
8. theorem OAI.PlanePotential.local_value_lp line 260

   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
   …

9. lemma OAI.DiskMoments.signedAverage_sub_const line 289
10. lemma OAI.DiskMoments.local_average_le line 303

    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.DiskMoments.signedAverage

11. theorem OAI.PlanePotential.local_value_majorant line 345

    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
    …

12. lemma OAI.AffineDensities.fderiv_affine_bound line 416
13. theorem OAI.CommonPrices.value_cell_price line 437

    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.CommonPrices.rootMass, OAI.CommonPrices.cellRoots, OAI.CommonPrices.cellPrice

14. def OAI.PhysicalCells.unitCell line 477
15. def OAI.PhysicalCells.toUnit line 478
16. def OAI.PhysicalCells.cell line 479
17. lemma OAI.PhysicalCells.unitCell_measurable line 481
18. lemma OAI.PhysicalCells.toUnit_continuous line 483
19. lemma OAI.PhysicalCells.cell_measurable line 484
20. lemma OAI.PhysicalCells.volume_unitCell line 486
21. lemma OAI.PhysicalCells.norm_unitCell line 494
22. lemma OAI.PhysicalCells.toUnit_affine line 498
23. lemma OAI.PhysicalCells.affine_toUnit line 500
24. lemma OAI.PhysicalCells.lintegral_smul line 503
25. lemma OAI.PhysicalCells.lintegral_toUnit line 511
26. lemma OAI.PhysicalCells.lintegral_cell line 520

    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.PhysicalCells.cell, OAI.PhysicalCells.unitCell

27. lemma OAI.PhysicalCells.cell_majorant line 531
28. lemma OAI.DiskMoments.signedAverage_affine line 538
29. lemma OAI.DiskMoments.gradient_signedAverage line 549
30. lemma OAI.DiskMoments.gradient_average_affine line 566
31. def OAI.DiskMoments.PhysicalNeighborhoodRadius line 578
32. def OAI.DiskMoments.PhysicalEndpointRadius line 581
33. lemma OAI.DiskMoments.neighborhoodRadius_affine line 584
34. lemma OAI.DiskMoments.endpointRadius_affine line 596
35. lemma OAI.PhysicalCells.derivative_majorant_integral line 614
36. lemma OAI.PhysicalCells.value_majorant_integral line 623
37. lemma OAI.DiskMoments.average_gradient_norm_le line 634
38. lemma OAI.DiskMoments.average_gradient_negative_le line 642
39. lemma OAI.DiskMoments.physical_gradient_norm_majorant line 653
40. lemma OAI.DiskMoments.physical_gradient_negative_majorant line 664
41. theorem OAI.CommonPrices.physical_directional_price line 681
42. theorem OAI.CommonPrices.physical_size_price line 717
43. theorem OAI.CommonPrices.physical_value_price line 753
44. lemma OAI.DiskMoments.signedAverage_abs_le line 783
45. def OAI.DiskMoments.oscillationSet line 794
46. def OAI.DiskMoments.oscillation line 796
47. lemma OAI.DiskMoments.oscillationSet_zero line 798
48. lemma OAI.DiskMoments.oscillationSet_bdd line 800
49. lemma OAI.DiskMoments.oscillation_nonneg line 809
50. lemma OAI.DiskMoments.le_oscillation line 812
51. lemma OAI.DiskMoments.oscillation_majorant line 816