OAI/Analysis/SignedDisk/FiniteLabels1.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedDisk.FiniteLabels.delta_diff_le_one line 34
2. def OAI.SignedDisk.FiniteLabels.spatialRow line 39

   Source documentation

   The actual locally finite transition row on the entire spatial grid.

   def spatialRow (old : ι) (target : ℤ × ℤ → ι) (p : ℤ × ℤ → ℝ)
       (hp0 : ∀ z, 0 ≤ p z) (hp1 : ∀ z, p z ≤ 1) (r : ℝ) (x : ℂ) : Law ι where
   …

   Mentions: OAI.SignedDisk.FiniteLabels.Law

3. lemma OAI.SignedDisk.FiniteLabels.spatialRow_formula line 56
4. lemma OAI.SignedDisk.FiniteLabels.spatialRow_component_lipschitz line 61
5. lemma OAI.SignedDisk.FiniteLabels.spatialRow_distance line 72
6. lemma OAI.SignedDisk.DyadicHats.interpolate_congr_on line 92
7. lemma OAI.SignedDisk.DyadicHats.interpolate_mono_on line 100
8. lemma OAI.SignedDisk.DyadicHats.hat_vertex_local line 108
9. lemma OAI.SignedDisk.DyadicHats.continuous_boxNorm line 116
10. lemma OAI.SignedDisk.DyadicHats.local_neighborhood line 119
11. def OAI.SignedDisk.DyadicHats.truncate line 124
12. lemma OAI.SignedDisk.DyadicHats.truncate_nonneg line 127
13. lemma OAI.SignedDisk.DyadicHats.truncate_le line 129
14. lemma OAI.SignedDisk.DyadicHats.interpolate_truncate line 132
15. lemma OAI.SignedDisk.FiniteLabels.spatialRow_truncate line 147
16. lemma OAI.SignedDisk.FiniteLabels.spatialRow_local_distance line 159
17. lemma OAI.SignedDisk.FiniteLabels.spatialRow_local_derivative line 172

    Source documentation

    The derivative cost is bounded by the local switched mass, with a constant fixed by the finite palette, rather than by the number of scales or vertices.

    lemma spatialRow_local_derivative (old : ι) (target : ℤ × ℤ → ι) (p : ℤ × ℤ → ℝ)
        (hp0 : ∀ z, 0 ≤ p z) (hp1 : ∀ z, p z ≤ 1) {r B : ℝ} (hr : 0 < r) (hB : 0 ≤ B)
        {q x : ℂ} (hx : boxNorm (x-q) < 199*r)
        (hpB : ∀ z, boxNorm (point r z-q) ≤ 200*r → p z ≤ B) :
        r*∑ j : ι, ‖gradient (fun y => spatialRow old target p hp0 hp1 r y j) x‖ ≤
          16*(Fintype.card ι:ℝ)*B := by
    …

    Mentions: OAI.SignedDisk.FiniteLabels.spatialRow

18. def OAI.SignedDisk.FiniteLabels.probability line 196
19. def OAI.SignedDisk.FiniteLabels.amplitude line 197
20. lemma OAI.SignedDisk.FiniteLabels.probability_formula line 199
21. lemma OAI.SignedDisk.FiniteLabels.amplitude_nonneg line 203
22. lemma OAI.SignedDisk.FiniteLabels.amplitude_le_one line 205
23. lemma OAI.SignedDisk.FiniteLabels.probability_nonneg line 206
24. lemma OAI.SignedDisk.FiniteLabels.probability_le_one line 207
25. lemma OAI.SignedDisk.FiniteLabels.probability_eq_square line 209
26. lemma OAI.SignedDisk.FiniteLabels.amplitude_lipschitz line 218
27. lemma OAI.SignedDisk.FiniteLabels.probability_compare line 240
28. lemma OAI.SignedDisk.FiniteLabels.probability_norm_compare line 250
29. lemma OAI.SignedDisk.FiniteLabels.probability_eq_zero line 261
30. lemma OAI.SignedDisk.FiniteLabels.probability_lt_one_iff line 265
31. lemma OAI.SignedDisk.FiniteLabels.interpolate_const_mul line 285
32. lemma OAI.SignedDisk.FiniteLabels.norm_sub_sq_le_four line 289
33. def OAI.SignedDisk.FiniteLabels.switchRate line 296
34. lemma OAI.SignedDisk.FiniteLabels.switchRate_nonneg line 299
35. lemma OAI.SignedDisk.FiniteLabels.switchRate_le_one line 301
36. lemma OAI.SignedDisk.FiniteLabels.probability_le_rate_energy line 306

    Source documentation

    The row-rate comparison is produced from the literal quadratic probability and the actual partition of unity, uniformly over all nearby grid vertices.

    lemma probability_le_rate_energy {τ r E : ℝ} (hτ : 0 < τ) (hr : 0 < r)
        (Θ : ℤ × ℤ → ℂ) (n θ q y : ℂ) (hy : boxNorm (y-q) < 199*r)
        (hE : ∀ z, boxNorm (point r z-q) ≤ 200*r → ‖Θ z-θ‖^2 ≤ E)
        (z : ℤ × ℤ) (hz : boxNorm (point r z-q) ≤ 200*r) :
        probability τ ‖n-Θ z‖ ≤ 2*switchRate τ r Θ n y+8*τ⁻¹^2*E := by
    …

    Mentions: OAI.SignedDisk.FiniteLabels.probability, OAI.SignedDisk.FiniteLabels.switchRate

37. lemma OAI.SignedDisk.FiniteLabels.switchRate_local_compare line 323
38. def OAI.SignedDisk.FiniteLabels.spatialSwitchRow line 338
39. lemma OAI.SignedDisk.FiniteLabels.spatialSwitchRow_local_distance line 343
40. lemma OAI.SignedDisk.FiniteLabels.spatialSwitchRow_local_derivative line 355
41. lemma OAI.SignedDisk.DyadicHats.hat_at_point line 371
42. lemma OAI.SignedDisk.DyadicHats.hat_vertex_bound line 383
43. lemma OAI.SignedDisk.DyadicHats.velocity_bound_on_grid line 401