OAI/Analysis/SignedDisk/ActualMarkTrees2.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedDisk.ActualMarkTrees.path_filtered_cost line 33
2. lemma OAI.SignedDisk.ActualMarkTrees.path_cellCost line 47
3. lemma OAI.SignedDisk.ActualMarkTrees.path_cellCost_sum line 85
4. def OAI.SignedDisk.ActualMarkTrees.packingCharge line 109
5. lemma OAI.SignedDisk.ActualMarkTrees.packingCharge_path line 112
6. lemma OAI.SignedDisk.ActualMarkTrees.tree_packing_bound line 142
7. def OAI.SignedDisk.ActualMarkTrees.packingConstant line 154
8. lemma OAI.SignedDisk.ActualMarkTrees.packingConstant_pos line 157
9. theorem OAI.SignedDisk.ActualMarkTrees.spatial_packing line 162
10. def OAI.SignedDisk.CommonPrices.rootMass line 198
11. lemma OAI.SignedDisk.CommonPrices.rootMass_nonneg line 200
12. def OAI.SignedDisk.CommonPrices.sizeErrors line 203
13. lemma OAI.SignedDisk.CommonPrices.sizeErrors_price line 209
14. lemma OAI.SignedDisk.CommonPrices.sizeErrors_gradient line 228
15. theorem OAI.SignedDisk.CommonPrices.size_cell_price line 245

    Source documentation

    The endpoint-bin gradient price, with all root terms retained rather than silently using the cone estimate at one-sided maximizing radii.

    theorem size_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) → ∀ (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,
            EndpointRadius (fun Y => g (point (scale r k) p+scale r k • Y)) X t →
            ENNReal.ofReal ‖∫ Y in Metric.ball X t,
              gradient (fun Z => g (point (scale r k) p+scale r k • Z)) Y‖ ≤ F X := by
    …

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

16. lemma OAI.SignedDisk.PlanePotential.green_restrict_density line 286
17. lemma OAI.SignedDisk.PlanePotential.green_root_lp_local line 295
18. lemma OAI.SignedDisk.PlanePotential.green_zero_piece_lp_ae line 322
19. theorem OAI.SignedDisk.PlanePotential.green_decomposition_norm_local line 355

    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.SignedDisk.PlanePotential.green

20. theorem OAI.SignedDisk.PlanePotential.exists_green_price line 385

    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.SignedDisk.PlanePotential.green