OAI/Analysis/DiskMaximal/Prices.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarCancellation.roots_nonneg_of_mass line 56
2. lemma OAI.ConeScalar.scalar_integrable line 74
3. lemma OAI.ConeScalar.scalar_support line 76
4. lemma OAI.ConeScalar.scalar_mass line 80
5. lemma OAI.ConeScalar.coordinate_mass_nonneg line 85
6. lemma OAI.ConeScalar.good_root_nonneg line 93
7. lemma OAI.ConeScalar.root_mass_norm line 104
8. lemma OAI.ConeScalar.root_vector_integrable line 113
9. lemma OAI.ConeScalar.root_bound line 118
10. lemma OAI.ConeScalar.pair_cone line 128
11. def OAI.AffineDensities.rescale line 146
12. lemma OAI.AffineDensities.integrable_rescale line 148
13. lemma OAI.AffineDensities.integral_affine line 151
14. lemma OAI.AffineDensities.integral_rescale line 157
15. lemma OAI.AffineDensities.mass_rescale line 163
16. lemma OAI.AffineDensities.rescale_support line 172
17. lemma OAI.PricePieces.error_support line 188
18. lemma OAI.PricePieces.scale_le line 194
19. def OAI.PricePieces.errorPiece line 198
20. lemma OAI.PricePieces.errorPiece_mass line 223
21. def OAI.LocalCancellation.ErrorPiece.weight line 242

    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.LocalCancellation.ErrorPiece

22. lemma OAI.LocalCancellation.ErrorPiece.mass_weight line 255
23. def OAI.LocalCancellation.unitPiece line 261

    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.LocalCancellation.ErrorPiece

24. lemma OAI.LocalCancellation.cone_sum line 271
25. def OAI.PricePieces.rootVector line 286

    Source documentation

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

    def rootVector (N : ℕ) (r : ℝ) (h : ℂ → ℂ) (k : ℕ) (q : Grid N) (n : ℂ) (y : ℂ) : ℂ :=
    …

26. def OAI.PricePieces.errorVector line 290
27. lemma OAI.PricePieces.vector_decomposition line 294
28. lemma OAI.PricePieces.rootVector_integrable line 308
29. lemma OAI.PricePieces.rootVector_cone line 312
30. lemma OAI.PricePieces.rootVector_mass line 321
31. def OAI.CommonPrices.rho line 344
32. lemma OAI.CommonPrices.rho_pos line 345
33. lemma OAI.CommonPrices.rho_lt_one line 346
34. lemma OAI.CommonPrices.scale_ratio line 348
35. lemma OAI.CommonPrices.scale_discount line 357
36. def OAI.CommonPrices.rootPrice line 366

    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) : ℝ :=
    …

37. lemma OAI.CommonPrices.scalarPrice_nonneg line 371
38. lemma OAI.CommonPrices.rootPrice_nonneg line 381
39. lemma OAI.CommonPrices.coordinate_total_le line 391
40. lemma OAI.CommonPrices.coordinate_price_budget line 397
41. theorem OAI.CommonPrices.rootPrice_budget line 412

    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.CommonPrices.rootPrice, OAI.CommonPrices.rho