SpatialBudgets.lean`

69 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ActualLabels.row_change_le_rate line 57
lemma OAI.ActualLabels.observation_startReward_le line 65
def OAI.ActualLabels.boundaryCost line 89
lemma OAI.ActualLabels.boundaryCost_nonneg line 92
lemma OAI.ActualLabels.observation_boundaryReward_le line 100
lemma OAI.ActualLabels.boundary_reward_sum line 119
lemma OAI.SignedRuns.expected_start_sum_bound line 149
lemma OAI.SignedRuns.expected_boundary_sum_bound line 157
lemma OAI.SignedRuns.expected_span_sum line 175
def OAI.PhysicalCells.gridIndex line 191
lemma OAI.PhysicalCells.toUnit_point_re line 193
lemma OAI.PhysicalCells.toUnit_point_im line 198
lemma OAI.PhysicalCells.mem_index_cell line 203
lemma OAI.PhysicalCells.cells_cover line 213
lemma OAI.PhysicalCells.mem_cell_box line 218
lemma OAI.PhysicalCells.cell_subset_root_neighborhood line 231
lemma OAI.PhysicalCells.lintegral_le_cells line 244
lemma OAI.PhysicalCells.tsum_ofReal_le line 249

lemma OAI.PhysicalCells.integral_cell_budget line 260

Source documentation

Global integration over the actual full lattice. The budget is tested on arbitrary finite sets, so neither support cutoffs nor omitted cells enter.

lemma integral_cell_budget {r : ℝ} (hr : 0 < r) (F : ℂ → ℝ≥0∞)
    (B : (ℤ × ℤ) → ℝ) (hB : ∀ p, 0 ≤ B p) (A : ℝ)
    (hcell : ∀ p, (∫⁻ y in cell (point r p) r, F y) ≤ ENNReal.ofReal (B p))
    (hbudget : ∀ s : Finset (ℤ × ℤ), ∑ p ∈ s, B p ≤ A) :
    (∫⁻ y, F y) ≤ ENNReal.ofReal A :=
…

Mentions: OAI.PhysicalCells.cell

lemma OAI.CommonPrices.cellRoots_budget line 272
lemma OAI.CommonPrices.badPrice_nonneg line 289
lemma OAI.CommonPrices.badPrice_le_rootMass line 292
lemma OAI.ActualLabels.marginal_localSup_nonneg line 301
lemma OAI.ActualLabels.marginal_localSup_le_one line 305
lemma OAI.ActualLabels.marginal_localSup_bad_zero line 309

lemma OAI.ActualLabels.marginal_badPrice_bound line 326

Source documentation

The actual bad-root charge is paid by geometric energy, not a separately assumed probability budget.

lemma marginal_badPrice_bound {N : ℕ} (h : ℂ → ℂ) (r : ℕ → ℝ) (base : ℝ)
    (k j : ℕ) (hr : 0 < r k) (hrj : r k = scale base j) (p : ℤ × ℤ) (n : Label) :
    localSup (fun x => marginal h r k x n) (r k) p*badPrice h base j (cellRoots N p) n ≤
      1000000*∑ q ∈ cellRoots N p, scalarMass h (r k) q*energy h (r k) q := by
…

Mentions: OAI.ActualLabels.Label, OAI.ActualLabels.marginal

def OAI.PhysicalCells.patch line 362
Source documentation
Measurable full-lattice patch; no choice of maximizing radius occurs.
```
def patch (r : ℝ) (F : (ℤ × ℤ) → ℂ → ℝ≥0∞) (x : ℂ) : ℝ≥0∞ :=
…
```
lemma OAI.PhysicalCells.patch_measurable line 365
lemma OAI.PhysicalCells.le_patch line 369
lemma OAI.PhysicalCells.lintegral_patch line 374
lemma OAI.PhysicalCells.lintegral_patch_budget line 380
lemma OAI.PhysicalCells.patch_finite line 388
lemma OAI.PhysicalCells.patch_integrable line 394
lemma OAI.PhysicalCells.real_le_patch line 400

lemma OAI.PhysicalCells.weighted_patch_bound line 409

Source documentation

Take the cell supremum of a weight only after the local price has been proved. This is the common production rule for all three spatial budgets.

lemma weighted_patch_bound (r : ℝ) (F : (ℤ × ℤ) → ℂ → ℝ≥0∞) (hF : ∀ p, Measurable (F p))
    (W : ℂ → ℝ≥0∞) (hW : Measurable W) (A B : (ℤ × ℤ) → ℝ)
    (hA : ∀ p, 0 ≤ A p) (_hB : ∀ p, 0 ≤ B p)
    (hcell : ∀ p, (∫⁻ x in cell (point r p) r, F p x) ≤ ENNReal.ofReal (B p))
    (hWB : ∀ p x, x ∈ cell (point r p) r → W x ≤ ENNReal.ofReal (A p)) :
    (∫⁻ x, W x*patch r F x) ≤ ∑' p, ENNReal.ofReal (A p*B p) := by
…

Mentions: OAI.PhysicalCells.cell, OAI.PhysicalCells.patch

def OAI.ActualLabels.geometricRadii line 439
Source documentation
Global geometric extension of the finite descending radius grid.
```
def geometricRadii (base : ℝ) (m : ℕ) (k : ℕ) : ℝ := scale base m/(2:ℝ)^k
```
lemma OAI.ActualLabels.geometricRadii_pos line 440
lemma OAI.ActualLabels.geometricRadii_step line 442
lemma OAI.ActualLabels.geometricRadii_eq line 447
lemma OAI.ActualLabels.marginal_congr line 455
lemma OAI.ActualLabels.switchCost_congr line 462
lemma OAI.ActualLabels.derivativeCost_congr line 469
lemma OAI.ActualLabels.cellCost_congr line 476
lemma OAI.SignedRuns.run_cone_bound line 499

theorem OAI.SignedRuns.pointwise_signed_master line 530

Source documentation

Complete pointwise signed assembly, still retaining the divergence term. The remaining terms are exactly the direct directional and boundary costs.

theorem pointwise_signed_master {g : ℂ → ℝ} (h : ℂ → ℂ) {r : ℕ → ℝ}
    (hg : ContDiff ℝ 1 g) (hc : HasCompactSupport g)
    (hr : ∀ k, 0 < r k) (hstep : ∀ k, 2*r (k+1) = r k)
    (H : ℕ → Label → ℝ) (J : ℕ → ℝ) (hH : ∀ k n, 0 ≤ H k n) (hJ : ∀ k, 0 ≤ J k)
    (old : Label) (m : ℕ) (x : ℂ)
    (hd : ∀ i j, i ≤ j → DifferentiableAt ℝ (runEnvelope g r i j) x)
    (hinterior : ∀ k n t, PhysicalNeighborhoodRadius g (r k) x t →
      unfavorable n (gradient (fun y => signedAverage g y t) x) ≤ H k n)
    (hend : ∀ k t, PhysicalEndpointRadius g (r k) x t →
      ‖gradient (fun y => signedAverage g y t) x‖ ≤ J k) :
    ‖gradient (runEnvelope g r 0 m) x‖ ≤ 12*(
      leafSum (fun q => weight h r old x q*divergence (fun y => potential g r y q) x) (m+1) []+
…

Mentions: OAI.SignedRuns.runEnvelope, OAI.SignedRuns.unfavorable, OAI.SignedRuns.leafSum, OAI.SignedRuns.weight, OAI.SignedRuns.divergence, OAI.SignedRuns.potential

lemma OAI.PhysicalCells.center_mem_cell line 579
def OAI.PhysicalCells.cellSup line 581
lemma OAI.PhysicalCells.cellSup_le line 583
lemma OAI.PhysicalCells.le_cellSup line 588
lemma OAI.PhysicalCells.cellSup_nonneg line 591
def OAI.ActualLabels.pointCost line 599
def OAI.ActualLabels.costLimit line 602
lemma OAI.ActualLabels.costLimit_pos line 603
lemma OAI.ActualLabels.pointCost_nonneg line 604
lemma OAI.ActualLabels.pointCost_le line 607
lemma OAI.ActualLabels.pointCost_le_cellCost line 616
lemma OAI.ActualLabels.cellSup_pointCost_le line 627
lemma OAI.ActualLabels.cellSup_pointCost_nonneg line 634
lemma OAI.ActualLabels.cellSup_pointCost_uniform line 637
lemma OAI.ActualLabels.pointCost_cell_budget line 641
def OAI.CommonPrices.priceConstant line 662
lemma OAI.CommonPrices.priceConstant_nonneg line 663
lemma OAI.CommonPrices.cellPrice_nonneg line 666
lemma OAI.CommonPrices.rootMass_cell_budget line 670
lemma OAI.ActualLabels.geometricRadii_reverse line 680
lemma OAI.ActualLabels.pointCost_mass_budget line 684
lemma OAI.ActualLabels.pointCost_price_budget line 715
lemma OAI.ActualLabels.marginal_bad_budget line 737
lemma OAI.ActualLabels.marginal_price_budget line 768