OAI/Analysis/SignedDisk/DyadicHats2.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedDisk.DyadicHats.step_support line 35
2. def OAI.SignedDisk.DyadicHats.weights line 50
3. def OAI.SignedDisk.DyadicHats.pieces line 51
4. def OAI.SignedDisk.DyadicHats.densityRoot line 53
5. def OAI.SignedDisk.DyadicHats.densityError line 55
6. lemma OAI.SignedDisk.DyadicHats.pieces_integrable line 58
7. lemma OAI.SignedDisk.DyadicHats.refined_eq_density line 61
8. lemma OAI.SignedDisk.DyadicHats.densityRoot_integrable line 71
9. lemma OAI.SignedDisk.DyadicHats.densityError_integrable line 74
10. lemma OAI.SignedDisk.DyadicHats.densityError_zero_mass line 77
11. lemma OAI.SignedDisk.DyadicHats.densityRoot_mass line 81
12. lemma OAI.SignedDisk.DyadicHats.densityRoot_abs_mass line 88
13. lemma OAI.SignedDisk.DyadicHats.density_support line 95
14. def OAI.SignedDisk.DyadicHats.densityDefect line 107
15. lemma OAI.SignedDisk.DyadicHats.densityError_cost line 112
16. lemma OAI.SignedDisk.DyadicHats.densityError_total_cost line 132
17. def OAI.SignedDisk.DyadicHats.coeff line 155

    Source documentation

    Coherent refinement coefficients, evaluated by exact positive matrix composition on the finite box. These are not row-stochastic transitions.

    def coeff (N : ℕ) : ℕ → Grid N → Grid N → ℝ
      | 0,p,q => if p=q then 1 else 0
      | d+1,p,q => ∑ a : Grid N, step p a*coeff N d a q

    Mentions: OAI.SignedDisk.DyadicHats.Grid, OAI.SignedDisk.DyadicHats.step

18. lemma OAI.SignedDisk.DyadicHats.coeff_nonneg line 159
19. lemma OAI.SignedDisk.DyadicHats.coeff_column line 164
20. theorem OAI.SignedDisk.DyadicHats.density_decomposition line 175

    Source documentation

    All lower-level error densities, with their actual coherent coefficients, reconstruct the genuine coarse hat density exactly.

    theorem density_decomposition {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
        (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℝ} (hs : ∀ y, h y ≠ 0 → ‖y‖ ≤ R)
        (k : ℕ) (q : Grid N) (x : ℂ) :
        hat (scale r k) q x*h x = densityRoot N r h k q x+
          ∑ j ∈ range (k+1), ∑ s : Grid N, coeff N (k-j) q s*densityError N r h j s x := by
    …

    Mentions: OAI.SignedDisk.DyadicHats.Grid, OAI.SignedDisk.DyadicHats.hat, OAI.SignedDisk.DyadicHats.scale, OAI.SignedDisk.DyadicHats.densityRoot, OAI.SignedDisk.DyadicHats.coeff, OAI.SignedDisk.DyadicHats.densityError

21. lemma OAI.SignedDisk.DyadicHats.terminal_abs_sum line 189
22. lemma OAI.SignedDisk.DyadicHats.densityDefect_sum_succ line 201
23. theorem OAI.SignedDisk.DyadicHats.densityDefect_budget_eq line 213

    Source documentation

    Exact telescoping of the literal scalar defects, including the finest terminal split. No depth-dependent or terminal remainder is discarded.

    theorem densityDefect_budget_eq {N : ℕ} {r R : ℝ} (hr : 0 < r)
        (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℝ} (hh : Integrable h)
        (hs : ∀ y, h y ≠ 0 → ‖y‖ ≤ R) (n : ℕ) :
        (∑ k ∈ range (n+1), ∑ q : Grid N, densityDefect N r h k q) =
          ((∫ x, |h x|)-(∑ q : Grid N, |∫ x, hat (scale r n) q x*h x|))/2 := by
    …

    Mentions: OAI.SignedDisk.DyadicHats.Grid, OAI.SignedDisk.DyadicHats.densityDefect, OAI.SignedDisk.DyadicHats.hat, OAI.SignedDisk.DyadicHats.scale

24. lemma OAI.SignedDisk.DyadicHats.densityDefect_nonneg line 228
25. lemma OAI.SignedDisk.DyadicHats.densityDefect_budget line 236
26. def OAI.SignedDisk.DyadicHats.scalarPrice line 246

    Source documentation

    The common scalar price assigned to a root. The geometric discount is applied at the actual birth scale of each zero-mass error.

    def scalarPrice (N : ℕ) (r : ℝ) (h : ℂ → ℝ) (ρ : ℝ) (k : ℕ) (q : Grid N) : ℝ :=
    …

    Mentions: OAI.SignedDisk.DyadicHats.Grid

27. lemma OAI.SignedDisk.DyadicHats.scalarPrice_sum line 249
28. lemma OAI.SignedDisk.DyadicHats.discount_recurrence line 262
29. lemma OAI.SignedDisk.DyadicHats.triangle_discount_bound line 274
30. theorem OAI.SignedDisk.DyadicHats.scalarPrice_budget line 296
31. def OAI.SignedDisk.DyadicHats.activeIndices line 309
32. lemma OAI.SignedDisk.DyadicHats.hat_zero_of_not_active line 312
33. lemma OAI.SignedDisk.DyadicHats.activeIndices_card line 323
34. lemma OAI.SignedDisk.DyadicHats.summable_weighted_hat line 329
35. def OAI.SignedDisk.DyadicHats.interpolate line 336

    Source documentation

    The literal locally finite tent interpolation, indexed by the whole grid.

    def interpolate (r : ℝ) (f : ℤ × ℤ → ℝ) (x : ℂ) : ℝ := ∑' p, hat r p x*f p

    Mentions: OAI.SignedDisk.DyadicHats.hat

36. lemma OAI.SignedDisk.DyadicHats.interpolate_eq_sum line 338
37. lemma OAI.SignedDisk.DyadicHats.interpolate_add line 345
38. lemma OAI.SignedDisk.DyadicHats.interpolate_sub line 349
39. lemma OAI.SignedDisk.DyadicHats.interpolate_mul_const line 353
40. lemma OAI.SignedDisk.DyadicHats.interpolate_const line 356
41. lemma OAI.SignedDisk.DyadicHats.interpolate_nonneg line 358
42. lemma OAI.SignedDisk.DyadicHats.interpolate_mono line 360
43. lemma OAI.SignedDisk.DyadicHats.interpolate_le_const line 364
44. lemma OAI.SignedDisk.DyadicHats.interpolate_finset_sum line 367
45. theorem OAI.SignedDisk.DyadicHats.interpolate_lipschitz line 375

    Source documentation

    Only eight tents can contribute to a difference of two interpolated values. This is the quantitative global Lipschitz bound with no grid cardinality loss.

    theorem interpolate_lipschitz {r B : ℝ} (hr : 0 < r) (hB : 0 ≤ B)
        {f : ℤ × ℤ → ℝ} (hf : ∀ p, |f p| ≤ B) :
        LipschitzWith (Real.toNNReal (16*B/r)) (interpolate r f) := by
    …

    Mentions: OAI.SignedDisk.DyadicHats.interpolate