Packing.lean`

71 declarations, 0 contain sorry, 0 declared as axioms

def OAI.CommonPrices.sign line 57
lemma OAI.CommonPrices.sign_cases line 58
lemma OAI.CommonPrices.sign_sq line 59
def OAI.CommonPrices.cellPrice line 61
def OAI.CommonPrices.rootWeight line 64
lemma OAI.CommonPrices.rootWeight_nonneg line 66
abbrev OAI.CommonPrices.ErrorIndex line 69
def OAI.CommonPrices.smallPiece line 71
lemma OAI.CommonPrices.smallPiece_mass line 76
lemma OAI.CommonPrices.discounted_smallPiece_mass line 90
lemma OAI.CommonPrices.weighted_defect_sum line 106
lemma OAI.CommonPrices.smallPiece_price line 119
lemma OAI.CommonPrices.smallPiece_common_price line 133
def OAI.CommonPrices.goodRoots line 153
def OAI.CommonPrices.badRoots line 155
def OAI.CommonPrices.rootSum line 158
lemma OAI.CommonPrices.rootSum_integrable line 161
lemma OAI.CommonPrices.rootSum_partition line 165
lemma OAI.CommonPrices.rootSum_mass line 170

def OAI.CommonPrices.goodCone line 185

Source documentation

The actual normalized positive-cone part on one cell.

def goodCone {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
    (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℂ} (hh : Integrable h)
    (hsupp : ∀ y, h y ≠ 0 → ‖y‖ ≤ R) (k : ℕ) (p : ℂ) (S : Finset (Grid N))
    {n : ℂ} (hn : ‖n‖ = 1) {s : ℝ} (hs : s = 1 ∨ s = -1) : ConeDensity (axis n s) (1/2) where
…

def OAI.CommonPrices.badPrice line 205

def OAI.CommonPrices.badPiece line 209

Source documentation

Bad cone roots are exactly the unrestricted size-one part.

def badPiece {N : ℕ} {r : ℝ} (hr : 0 < r) {h : ℂ → ℂ} (hh : Integrable h)
    (k : ℕ) (p : ℂ) (S : Finset (Grid N)) (n : ℂ) : ErrorPiece 2 :=
…

lemma OAI.CommonPrices.badPiece_mass line 214
def OAI.CommonPrices.cellErrors line 224
lemma OAI.CommonPrices.cellErrors_price line 229
lemma OAI.CommonPrices.smallPiece_pair_sum line 247
lemma OAI.CommonPrices.smallPiece_sum line 255

theorem OAI.CommonPrices.cell_decomposition line 274

Source documentation

Exact cell decomposition before imposing the local partition-of-unity region. Both its scalar coordinates and all error densities are the actual finite dyadic construction.

theorem cell_decomposition {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
    (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℂ} (hh : Integrable h)
    (hsupp : ∀ y, h y ≠ 0 → ‖y‖ ≤ R) (k : ℕ) (p : ℂ) (S : Finset (Grid N))
    {n : ℂ} (hn : ‖n‖ = 1) {s : ℝ} (hs : s = 1 ∨ s = -1) (X : ℂ) :
    (goodCone hr hR hN hh hsupp k p S hn hs).density X+
      (∑ i, (cellErrors hr hh k p S n i).density X) =
      rescale p (scale r k) (fun y => (∑ q ∈ S, hat (scale r k) q y) • h y) X := by
…

Mentions: OAI.CommonPrices.goodCone, OAI.CommonPrices.cellErrors

lemma OAI.DirectionNeighbors.mem_window_comm line 296
lemma OAI.DirectionNeighbors.card_window line 299
def OAI.CommonPrices.cellRoots line 311
lemma OAI.CommonPrices.cellPrice_spatial line 314

theorem OAI.CommonPrices.cellPrice_budget line 336

Source documentation

The common geometric price has a genuine uniform spatial-and-scale budget, including every desired finite set of observation cells.

theorem cellPrice_budget {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
    (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℂ} (hh : Integrable h)
    (hsupp : ∀ y, h y ≠ 0 → ‖y‖ ≤ R) (m : ℕ) (P : ℕ → Finset (ℤ × ℤ)) :
    (∑ k ∈ range (m+1), ∑ p ∈ P k, cellPrice N r h k (cellRoots N p)) ≤
      1681*((fixedPalette.labels.card:ℝ)*2/(1-rho))*(∫ y, ‖h y‖) := by
…

Mentions: OAI.CommonPrices.cellPrice, OAI.CommonPrices.cellRoots, OAI.CommonPrices.rho

lemma OAI.ActualMarkTrees.nodeCharge_scale line 356
def OAI.ActualMarkTrees.spatialCharge line 376
lemma OAI.ActualMarkTrees.spatialCharge_cons line 379
lemma OAI.ActualMarkTrees.sum_nodeCharge line 383
lemma OAI.ActualMarkTrees.sum_energyCharge line 412
def OAI.ActualMarkTrees.particleSwitches line 430
Source documentation
Particle observations use the prescribed terminal vertex, not a hat-density surrogate. This is the frozen spatial location carried throughout the process.
```
def particleSwitches {N : ℕ} (h : ℂ → ℂ) (r : ℝ) (k : ℕ) (q : Grid N)
    (p : List (Grid N)) (b : ℕ) : ℝ :=
…
```
theorem OAI.ActualMarkTrees.particle_switch_bound line 434

theorem OAI.ActualMarkTrees.forest_switch_budget line 455

Source documentation

The switch budget for the actual finite spatial forest, with every birth population included and frozen terminal positions observed.

theorem forest_switch_budget {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
    (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℂ} (hh : Integrable h)
    (hsupp : ∀ y, h y ≠ 0 → ‖y‖ ≤ R) (k : ℕ) :
    (∑ q : Grid N, particleEval (tree (fun q => vectorMass h r q) k 1 q)
      (particleSwitches h r k q)) ≤
      (2560004+2000000*(576*(4097:ℝ)^2))*(∫ y, ‖h y‖) := by
…

Mentions: OAI.ActualMarkTrees.tree, OAI.ActualMarkTrees.particleSwitches

lemma OAI.FiniteLabels.expect_const line 474
lemma OAI.FiniteLabels.expect_mul line 476
lemma OAI.FiniteLabels.expect_mono line 479
lemma OAI.FiniteLabels.expect_le_const line 481
lemma OAI.FiniteLabels.expect_compare line 483
def OAI.ActualLabels.comparisonConstant line 494
lemma OAI.ActualLabels.comparisonConstant_ge line 495
lemma OAI.ActualLabels.comparisonConstant_pos line 498
lemma OAI.ActualLabels.comparisonConstant_one line 499
def OAI.ActualLabels.rowDerivative line 501
def OAI.ActualLabels.derivativeCost line 503
lemma OAI.ActualLabels.rowDerivative_nonneg line 507
lemma OAI.ActualLabels.rowDerivative_uniform line 509
lemma OAI.ActualLabels.initial_distance line 517
lemma OAI.ActualLabels.derivativeCost_uniform line 528
lemma OAI.ActualLabels.rate_local line 539
lemma OAI.ActualLabels.row_local_distance line 551
lemma OAI.ActualLabels.row_local_derivative line 572
lemma OAI.AffineDensities.gradient_affine line 591
lemma OAI.DyadicHats.vector_partition_grid line 606
lemma OAI.CommonPrices.hat_mem_cellRoots line 623
lemma OAI.CommonPrices.cell_partition line 640
lemma OAI.CommonPrices.cell_decomposition_gradient line 652

theorem OAI.CommonPrices.directional_cell_price line 666

Source documentation

The hard directional local price, instantiated with the actual common-price cone decomposition on the actual neighboring grid roots.

theorem directional_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 → ∀ {s : ℝ}, (s = 1 ∨ s = -1) →
    ∀ Q : Set ℂ, volume Q ≤ ENNReal.ofReal 1 →
    ∃ F : ℂ → ℝ≥0∞, Measurable F ∧
      (∫⁻ X in Q, F X) ≤ ENNReal.ofReal (C*(scale r k)⁻¹*
        (badPrice (gradient g) r k (cellRoots N p) n+cellPrice N r (gradient g) k (cellRoots N p))) ∧
      ∀ X, ‖X‖ ≤ 2 → ∀ t,
        NeighborhoodRadius (fun Y => g (point (scale r k) p+scale r k • Y)) X t →
        ENNReal.ofReal (max 0 (-inner ℝ (axis n s)
…

Mentions: OAI.CommonPrices.badPrice, OAI.CommonPrices.cellRoots, OAI.CommonPrices.cellPrice

def OAI.ActualLabels.energyRate line 711
lemma OAI.ActualLabels.energyRate_nonneg line 713
lemma OAI.ActualLabels.energyRate_le_five line 715

theorem OAI.ActualLabels.marginal_spatial_distance line 724

Source documentation

Spatial comparison of the actual marginal laws. No independent coupling or pointwise uniform distribution of labels is assumed.

theorem marginal_spatial_distance (h : ℂ → ℂ) (r : ℕ → ℝ) (q : ℕ → ℤ × ℤ)
    (x y : ℂ) (j : ℕ) (hr : ∀ i ≤ j, 0 < r i)
    (hx : ∀ i ≤ j, boxNorm (x-point (r i) (q i)) < 199*r i)
    (hy : ∀ i ≤ j, boxNorm (y-point (r i) (q i)) < 199*r i) :
    l1dist (marginal h r j x) (marginal h r j y) ≤
      comparisonConstant*‖x-y‖*∑ i ∈ range (j+1), energyRate h r q y i/r i := by
…

Mentions: OAI.ActualLabels.marginal, OAI.ActualLabels.comparisonConstant, OAI.ActualLabels.energyRate

lemma OAI.ActualLabels.switchCost_spatial line 762
lemma OAI.ActualLabels.derivativeCost_spatial line 776