OAI/Analysis/SignedDisk/CommonPrices3.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedDisk.CommonPrices.priceConstant line 33
  2. lemma OAI.SignedDisk.CommonPrices.priceConstant_nonneg line 34
  3. lemma OAI.SignedDisk.CommonPrices.cellPrice_nonneg line 37
  4. lemma OAI.SignedDisk.CommonPrices.rootMass_cell_budget line 41
  5. lemma OAI.SignedDisk.ActualLabels.geometricRadii_reverse line 51
  6. lemma OAI.SignedDisk.ActualLabels.pointCost_mass_budget line 55
  7. lemma OAI.SignedDisk.ActualLabels.pointCost_price_budget line 86
  8. lemma OAI.SignedDisk.ActualLabels.marginal_bad_budget line 108
  9. lemma OAI.SignedDisk.ActualLabels.marginal_price_budget line 139
  10. def OAI.SignedDisk.ActualLabels.spatialPriceConstant line 158
  11. lemma OAI.SignedDisk.ActualLabels.spatialPriceConstant_pos line 159
  12. def OAI.SignedDisk.ActualLabels.directPriceConstant line 166
  13. lemma OAI.SignedDisk.ActualLabels.directPriceConstant_pos line 167
  14. lemma OAI.SignedDisk.ActualLabels.pointCost_total_budget line 172
  15. lemma OAI.SignedDisk.ActualLabels.marginal_total_budget line 185
  16. lemma OAI.SignedDisk.CommonPrices.cellPrice_level_budget line 201
  17. lemma OAI.SignedDisk.CommonPrices.total_level_budget line 211
  18. lemma OAI.SignedDisk.ActualLabels.gradient_measurable line 222
  19. lemma OAI.SignedDisk.ActualLabels.marginal_continuous line 225
  20. lemma OAI.SignedDisk.ActualLabels.rate_continuous line 235
  21. lemma OAI.SignedDisk.ActualLabels.switchCost_continuous line 241
  22. lemma OAI.SignedDisk.ActualLabels.derivativeCost_measurable line 249
  23. lemma OAI.SignedDisk.ActualLabels.filt_measurable line 263
  24. lemma OAI.SignedDisk.ActualLabels.pointCost_measurable line 269
  25. lemma OAI.SignedDisk.PhysicalCells.sum_tsum_ofReal_le line 282
  26. lemma OAI.SignedDisk.PhysicalCells.integrated_weighted_patches line 293
  27. lemma OAI.SignedDisk.GeometricFilter.radius_convolution line 310
  28. lemma OAI.SignedDisk.SignedRuns.total_divergence_integrable line 328
  29. lemma OAI.SignedDisk.SignedRuns.total_flux_integrable line 340
  30. lemma OAI.SignedDisk.SignedRuns.band_gradient_integrable line 350
  31. theorem OAI.SignedDisk.SignedRuns.integrated_signed_master line 362

    Source documentation

    Integration of the signed master, with its actual history law. The only remaining inputs here are actual analytic majorants and their integrals; no unsigned sum of run gradients is introduced.

    theorem integrated_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 x, 0 ≤ H k n x) (hJ : ∀ k x, 0 ≤ J k x)
    (old : Label) (m : ℕ)
    (hinterior : ∀ᵐ x, ∀ k n t, PhysicalNeighborhoodRadius g (r k) x t →
      unfavorable n (gradient (fun y => signedAverage g y t) x) ≤ H k n x)
    (hend : ∀ᵐ x, ∀ k t, PhysicalEndpointRadius g (r k) x t →
      ‖gradient (fun y => signedAverage g y t) x‖ ≤ J k x)
    (hvalue : ∀ᵐ x, ∀ k t t', 0 < t → t ≤ 4*r k → 0 < t' → t' ≤ 4*r k →
      |signedAverage g x t-signedAverage g x t'| ≤ r k*J k x)
…

    Mentions: OAI.SignedDisk.SignedRuns.unfavorable