OAI/Analysis/SignedDisk/AffineDensities1.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedDisk.AffineDensities.rescale line 32
  2. lemma OAI.SignedDisk.AffineDensities.integrable_rescale line 34
  3. lemma OAI.SignedDisk.AffineDensities.integral_affine line 37
  4. lemma OAI.SignedDisk.AffineDensities.integral_rescale line 43
  5. lemma OAI.SignedDisk.AffineDensities.mass_rescale line 49
  6. lemma OAI.SignedDisk.AffineDensities.rescale_support line 58
  7. lemma OAI.SignedDisk.PricePieces.error_support line 74
  8. lemma OAI.SignedDisk.PricePieces.scale_le line 80
  9. def OAI.SignedDisk.PricePieces.errorPiece line 84
  10. lemma OAI.SignedDisk.PricePieces.errorPiece_mass line 109
  11. def OAI.SignedDisk.LocalCancellation.ErrorPiece.weight line 128

    Source documentation

    Multiplication of an error density by a nonnegative path coefficient. Zero coefficients are retained as genuine zero-density pieces.

    def ErrorPiece.weight {Cs : ℝ} (b : ErrorPiece Cs) (w : ℝ) : ErrorPiece Cs where
…

    Mentions: OAI.SignedDisk.LocalCancellation.ErrorPiece

  12. lemma OAI.SignedDisk.LocalCancellation.ErrorPiece.mass_weight line 141
  13. def OAI.SignedDisk.LocalCancellation.unitPiece line 147

    Source documentation

    An unrestricted integrable root term is a legitimate size-one piece.

    def unitPiece (h : ℂ → ℂ) (hh : Integrable h) (Cs : ℝ) : ErrorPiece Cs where
…

    Mentions: OAI.SignedDisk.LocalCancellation.ErrorPiece

  14. lemma OAI.SignedDisk.LocalCancellation.cone_sum line 157
  15. def OAI.SignedDisk.PricePieces.rootVector line 172

    Source documentation

    The vector root comprises the two actual signed scalar surviving roots.

    def rootVector (N : ℕ) (r : ℝ) (h : ℂ → ℂ) (k : ℕ) (q : Grid N) (n : ℂ) (y : ℂ) : ℂ :=
…
  16. def OAI.SignedDisk.PricePieces.errorVector line 176
  17. lemma OAI.SignedDisk.PricePieces.vector_decomposition line 180
  18. lemma OAI.SignedDisk.PricePieces.rootVector_integrable line 194
  19. lemma OAI.SignedDisk.PricePieces.rootVector_cone line 198
  20. lemma OAI.SignedDisk.PricePieces.rootVector_mass line 207
  21. def OAI.SignedDisk.CommonPrices.rho line 230
  22. lemma OAI.SignedDisk.CommonPrices.rho_pos line 231
  23. lemma OAI.SignedDisk.CommonPrices.rho_lt_one line 232
  24. lemma OAI.SignedDisk.CommonPrices.scale_ratio line 234
  25. lemma OAI.SignedDisk.CommonPrices.scale_discount line 243
  26. def OAI.SignedDisk.CommonPrices.rootPrice line 252

    Source documentation

    A common root price sums the two exact coordinate defects for every member of one fixed finite palette; it does not depend on the active label.

    def rootPrice (N : ℕ) (r : ℝ) (h : ℂ → ℂ) (k : ℕ) (q : Grid N) : ℝ :=
…
  27. lemma OAI.SignedDisk.CommonPrices.scalarPrice_nonneg line 257
  28. lemma OAI.SignedDisk.CommonPrices.rootPrice_nonneg line 267
  29. lemma OAI.SignedDisk.CommonPrices.coordinate_total_le line 277
  30. lemma OAI.SignedDisk.CommonPrices.coordinate_price_budget line 283
  31. theorem OAI.SignedDisk.CommonPrices.rootPrice_budget line 298

    Source documentation

    The genuine all-label root price has a uniform total budget, including the terminal scalar splits at the finest scale.

    theorem rootPrice_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 : ℕ) :
    (∑ k ∈ range (m+1), ∑ q : Grid N, rootPrice N r h k q) ≤
      (2*(fixedPalette.labels.card:ℝ)*(1-rho)⁻¹)*(∫ x, ‖h x‖) := by
…

    Mentions: OAI.SignedDisk.CommonPrices.rootPrice, OAI.SignedDisk.CommonPrices.rho

  32. lemma OAI.SignedDisk.FiniteLabels.spatialRow_mixture line 324
  33. lemma OAI.SignedDisk.FiniteLabels.spatialRow_vanish line 334
  34. abbrev OAI.SignedDisk.ActualLabels.Label line 348
  35. instance OAI.SignedDisk.ActualLabels.(instance at line 349) line 349
  36. instance OAI.SignedDisk.ActualLabels.(instance at line 350) line 350
  37. lemma OAI.SignedDisk.ActualLabels.label_unit line 352
  38. def OAI.SignedDisk.ActualLabels.target line 354
  39. lemma OAI.SignedDisk.ActualLabels.target_close line 356
  40. def OAI.SignedDisk.ActualLabels.switchChance line 359
  41. lemma OAI.SignedDisk.ActualLabels.switchChance_nonneg line 361
  42. lemma OAI.SignedDisk.ActualLabels.switchChance_le_one line 363
  43. def OAI.SignedDisk.ActualLabels.row line 366
  44. def OAI.SignedDisk.ActualLabels.initial line 370
  45. lemma OAI.SignedDisk.ActualLabels.nearby_sample_close line 374
  46. lemma OAI.SignedDisk.ActualLabels.sampled_good line 383
  47. lemma OAI.SignedDisk.ActualLabels.retained_good line 395
  48. lemma OAI.SignedDisk.ActualLabels.initial_bad_zero line 408
  49. lemma OAI.SignedDisk.ActualLabels.row_bad_zero line 417
  50. def OAI.SignedDisk.ActualLabels.marginal line 433

    Source documentation

    The actual finite-state label marginal, with its scale-dependent spatial rows. This definition introduces no geometric or probabilistic hypothesis.

    def marginal (h : ℂ → ℂ) (r : ℕ → ℝ) : ℕ → ℂ → Law Label
  | 0,x => initial h (r 0) x
  | k+1,x => move (marginal h r k x) (row h (r (k+1)) x)

    Mentions: OAI.SignedDisk.ActualLabels.Label, OAI.SignedDisk.ActualLabels.initial, OAI.SignedDisk.ActualLabels.row

  51. theorem OAI.SignedDisk.ActualLabels.marginal_bad_zero line 437