OAI/Analysis/DiskMaximal/Telescoping.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DiskScales.width_add line 22
2. lemma OAI.DiskScales.sum_width_tail line 26
3. lemma OAI.DiskScales.dist_width_tail line 35
4. lemma OAI.LocalCancellation.moment_kernel_pairing_sub line 50
5. lemma OAI.LocalCancellation.total_correction line 61
6. lemma OAI.LocalCancellation.balanced_kernel_gap_identity line 72
7. lemma OAI.LocalCancellation.kernel_error_bound line 114
8. lemma OAI.LocalCancellation.coarse_bound_scaled line 127
9. lemma OAI.LocalCancellation.scaled_ordinary_inactive line 133
10. lemma OAI.LocalCancellation.scaled_corrected_inactive line 148
11. lemma OAI.LocalCancellation.scaled_corrected_active line 163
12. lemma OAI.DiskScales.successor_discount line 181
13. lemma OAI.DiskScales.geometric_den_pos line 189
14. lemma OAI.DiskScales.coarse_error_scale line 192
15. lemma OAI.LocalCancellation.inactive_kernel_distance line 224
16. lemma OAI.LocalCancellation.kernel_gap_errors line 242
17. lemma OAI.LocalCancellation.corrected_kernel_gap line 289
18. def OAI.DiskScales.errorGapConstant line 338
19. def OAI.DiskScales.directionGapConstant line 341
20. lemma OAI.DiskScales.errorGapConstant_pos line 344
21. lemma OAI.DiskScales.directionGapConstant_ge line 349
22. lemma OAI.DiskScales.directionGapConstant_pos line 357
23. lemma OAI.DiskScales.direction_cap_scale line 362
24. lemma OAI.LocalCancellation.direction_sequence_point line 396

    Source documentation

    The full finite/infinite active-width argument at a fixed center. The cap premise is exactly the already proved shell concentration output, not a radius selection or a projection estimate.

    lemma direction_sequence_point {Cs κ d t r : ℝ} {e : ℂ} (a : ConeDensity e κ)
        (b : ι → ErrorPiece Cs) (he : ‖e‖ = 1) (hκ : 0 < κ)
        (hCs : 0 ≤ Cs) (hd : 0 < d) (hdq : d ≤ 1/4) (hr : r ∈ Icc (1 : ℝ) 2)
        (hAt : errorPrice b (1/100) ≤ t)
        (k : ∀ n : ℕ, RadiusDensity (r-width d n) (r+width d n)
          ⟨216/width d n, div_nonneg (by norm_num) (width_pos hd n).le⟩) (x : ℂ)
        (hM : ∀ n, (∫ y, star (y-x)*(kernel (k n) x y : ℂ)*a.density y)+
          (∑ v, ∫ y, star (y-x)*(kernel (k n) x y : ℂ)*(b v).density y) = 0)
        (hcap : ∀ j, t*(width d j)^(1/10 : ℝ) ≤ coarseMass b (width d j) (thinShell x r (width d j)) →
          (∫ y in Metric.ball x (r-width d j), ‖a.density y‖) ≤
            (errorGapConstant Cs/κ)*t*(width d j)^(-(1/50 : ℝ)) →
          ∃ z ∈ thinShell x r (width d j),
    …

    Mentions: OAI.LocalCancellation.ConeDensity, OAI.LocalCancellation.ErrorPiece, OAI.LocalCancellation.errorPrice, OAI.LocalCancellation.coarseMass

25. def OAI.LocalCancellation.directionShellBound line 531
26. theorem OAI.LocalCancellation.direction_sequence line 543

    Source documentation

    Radius-independent exceptional union for the full directional sequence. The cap property is produced by shell concentration for the actual densities.

    theorem direction_sequence {e : ℂ} {κ Cs d t : ℝ} (a : ConeDensity e κ)
        (b : ι → ErrorPiece Cs) (he : ‖e‖ = 1) (hκ : 0 < κ)
        (hCs : 0 ≤ Cs) (hd : 0 < d) (hdq : d ≤ 1/4)
        (hgeom : ∀ δ : ℝ, 0 < δ → δ ≤ d → δ ≤ (δ^(1/5 : ℝ))^2/1600)
        (ht : 0 < t) (hAt : errorPrice b (1/100) ≤ t) :
        ∃ E : Set ℂ, MeasurableSet E ∧
          volume E ≤ ∑' n : ℕ, directionShellBound b κ t (width d n) ∧
          ∀ x ∉ E, ∀ r ∈ Icc (1 : ℝ) 2,
            ∀ k : ∀ n : ℕ, RadiusDensity (r-width d n) (r+width d n)
              ⟨216/width d n, div_nonneg (by norm_num) (width_pos hd n).le⟩,
            (∀ n, (∫ y, star (y-x)*(kernel (k n) x y : ℂ)*a.density y)+
              (∑ v, ∫ y, star (y-x)*(kernel (k n) x y : ℂ)*(b v).density y) = 0) →
    …

    Mentions: OAI.LocalCancellation.ConeDensity, OAI.LocalCancellation.ErrorPiece, OAI.LocalCancellation.errorPrice, OAI.LocalCancellation.directionShellBound

27. def OAI.DiskMoments.NeighborhoodRadius line 597
28. lemma OAI.DiskMoments.neighborhood_kernel line 601
29. lemma OAI.LocalCancellation.mixed_moment_pairing_decomposition line 619
30. lemma OAI.LocalCancellation.mixed_ball_pairing_decomposition line 638
31. theorem OAI.LocalCancellation.direction_raw line 651

    Source documentation

    Directional estimate at all genuine neighborhood-maximizing radii, with only the original local density equality.

    theorem direction_raw {e : ℂ} {κ Cs d t : ℝ} (a : ConeDensity e κ)
        (b : ι → ErrorPiece Cs) (he : ‖e‖ = 1) (hκ : 0 < κ)
        (hCs : 0 ≤ Cs) (hd : 0 < d) (hdq : d ≤ 1/4)
        (hgeom : ∀ δ : ℝ, 0 < δ → δ ≤ d → δ ≤ (δ^(1/5 : ℝ))^2/1600)
        (ht : 0 < t) (hAt : errorPrice b (1/100) ≤ t)
        {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g) :
        ∃ E : Set ℂ, MeasurableSet E ∧
          volume E ≤ ∑' n : ℕ, directionShellBound b κ t (width d n) ∧
          ∀ x ∉ E,
            (∀ᵐ y, y ∈ Metric.ball x 3 → a.density y+∑ j, (b j).density y = gradient g y) →
            ∀ r, NeighborhoodRadius g x r →
            max 0 (-inner ℝ e (∫ y in Metric.ball x r, gradient g y)) ≤
    …

    Mentions: OAI.LocalCancellation.ConeDensity, OAI.LocalCancellation.ErrorPiece, OAI.LocalCancellation.errorPrice, OAI.LocalCancellation.directionShellBound

32. lemma OAI.DiskScales.third_power_identity line 680
33. lemma OAI.DiskScales.direction_shell_tail_scaled line 686
34. lemma OAI.DiskScales.direction_start_identity line 738
35. lemma OAI.DiskScales.exists_direction_parameters line 760
36. def OAI.DiskScales.directionTailConstant line 786
37. lemma OAI.DiskScales.directionTailConstant_pos line 788
38. theorem OAI.LocalCancellation.direction_tail line 801

    Source documentation

    A genuine superlevel bound with exponent 34/25 > 1 for all neighborhood maxima, independent of the number of positive or cancelling pieces.

    theorem direction_tail {Cs κ : ℝ} (hCs : 0 ≤ Cs) (hκ : 0 < κ) :
        ∃ L : ℝ, 1 ≤ L ∧ ∀ {ι : Type*} [Fintype ι] {e : ℂ} (a : ConeDensity e κ)
          (b : ι → ErrorPiece Cs), ‖e‖ = 1 →
          0 < errorPrice b (1/100) → ∀ t : ℝ, L*errorPrice b (1/100) ≤ t →
          ∀ g : ℂ → ℝ, ContDiff ℝ 1 g →
          ∃ E : Set ℂ, MeasurableSet E ∧
            volume E ≤ ENNReal.ofReal (directionTailConstant Cs κ*(errorPrice b (1/100)/t)^(34/25 : ℝ)) ∧
            ∀ x ∉ E,
              (∀ᵐ y, y ∈ Metric.ball x 3 → a.density y+∑ j, (b j).density y = gradient g y) →
              ∀ r, NeighborhoodRadius g x r →
                max 0 (-inner ℝ e (∫ y in Metric.ball x r, gradient g y)) ≤ t := by
    …

    Mentions: OAI.LocalCancellation.ConeDensity, OAI.LocalCancellation.ErrorPiece, OAI.LocalCancellation.errorPrice

39. lemma OAI.LocalCancellation.cone_ball_nonneg line 861
40. theorem OAI.LocalCancellation.direction_majorant line 870

    Source documentation

    Full Borel integrable directional price. This is the hard local cancellation estimate, not an assumed maximal-operator endpoint.

    theorem direction_majorant {Cs κ : ℝ} (hCs : 0 ≤ Cs) (hκ : 0 < κ) :
        ∃ C : ℝ, 0 < C ∧ ∀ {ι : Type*} [Fintype ι] {e : ℂ} (a : ConeDensity e κ)
          (b : ι → ErrorPiece Cs), ‖e‖ = 1 →
          ∀ g : ℂ → ℝ, ContDiff ℝ 1 g → ∀ Q : Set ℂ, volume Q ≤ ENNReal.ofReal 1 →
          ∃ F : ℂ → ℝ≥0∞, Measurable F ∧
            (∫⁻ x in Q, F x) ≤ ENNReal.ofReal (C*errorPrice b (1/100)) ∧
            ∀ x, (∀ᵐ y, y ∈ Metric.ball x 3 → a.density y+∑ j, (b j).density y = gradient g y) →
              ∀ r, NeighborhoodRadius g x r →
                ENNReal.ofReal (max 0 (-inner ℝ e (∫ y in Metric.ball x r, gradient g y))) ≤ F x := by
    …

    Mentions: OAI.LocalCancellation.ConeDensity, OAI.LocalCancellation.ErrorPiece, OAI.LocalCancellation.errorPrice