OAI/Analysis/DiskMaximal/Scales.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DiskScales.width line 22
2. lemma OAI.DiskScales.width_pos line 24
3. lemma OAI.DiskScales.width_le line 28
4. lemma OAI.DiskScales.width_succ line 32
5. lemma OAI.DiskScales.width_antitone line 36
6. lemma OAI.DiskScales.tendsto_width line 43
7. lemma OAI.DiskScales.width_rpow line 49
8. lemma OAI.DiskScales.ratio_norm_lt line 56
9. lemma OAI.DiskScales.summable_width_rpow line 60
10. lemma OAI.DiskScales.tsum_width_rpow line 65
11. lemma OAI.DiskScales.scaled_increment line 71
12. lemma OAI.DiskScales.exists_admissible_width line 109

    Source documentation

    A single small width works for both shell geometry and every smaller width.

    lemma exists_admissible_width : ∃ δ₀ : ℝ, 0 < δ₀ ∧ δ₀ ≤ 1/4 ∧
        ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ → δ ≤ (δ^(1/5 : ℝ))^2/1600 := by
    …

13. theorem OAI.LocalCancellation.size_sequence line 136

    Source documentation

    Uniform exceptional sets controlling a whole decreasing sequence of disk mixtures. Only active increments require the exact balanced moment.

    theorem size_sequence {Cs d t : ℝ} (b : ι → ErrorPiece Cs)
        (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 : ℕ, (
            (ENNReal.ofReal (t*(width d n)^(1/10 : ℝ)))⁻¹ ^ 2 *
              (ENNReal.ofReal (156*width d n/(width d n)^(1/5 : ℝ))*
                ENNReal.ofReal (coarseMass b (width d n) univ)*ENNReal.ofReal (coarseMass b (width d n) univ)) +
            (ENNReal.ofReal (t*(width d n)^(1/10 : ℝ)))⁻¹ *
              ((ENNReal.ofReal (6*Real.pi)*ENNReal.ofReal (2*(200*width d n/((width d n)^(1/5 : ℝ))^2)))*
                ENNReal.ofReal (coarseMass b (width d n) univ))) ∧
    …

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

14. def OAI.DiskGeometry.endpointFailure line 233
15. lemma OAI.DiskGeometry.endpoint_failure_bound line 237
16. lemma OAI.DiskGeometry.active_away_from_endpoints line 251
17. def OAI.DiskMoments.EndpointRadius line 268
18. lemma OAI.DiskMoments.endpoint_kernel line 274

    Source documentation

    Every band-maximizing or forced-endpoint radius has honest mixtures; balancing is imposed exactly when its width stays inside the band.

    lemma endpoint_kernel {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g) {x : ℂ} {r δ : ℝ}
        (hr : EndpointRadius g x r) (hδ : 0 < δ) (hδq : δ ≤ 1/4) :
        ∃ k : RadiusDensity (r-δ) (r+δ) ⟨216/δ, by positivity⟩,
          (1+δ ≤ r ∧ r+δ ≤ 2 →
            (∫ y, kernel k x y • (star (y-x)*gradient g y)) = 0) := by
    …

    Mentions: OAI.DiskMoments.EndpointRadius

19. lemma OAI.LocalCancellation.moment_pairing_integrable line 304
20. lemma OAI.LocalCancellation.moment_pairing_decomposition line 318

    Source documentation

    A local equality of genuine densities suffices for all supported moments.

    lemma moment_pairing_decomposition {Cs r δ : ℝ} (b : ι → ErrorPiece Cs)
        {M : ℝ≥0} (k : RadiusDensity (r-δ) (r+δ) M) (x : ℂ) {h : ℂ → ℂ}
        (hr : r+δ ≤ 3) (hh : ∀ᵐ y, y ∈ Metric.ball x 3 → ∑ j, (b j).density y = h y) :
        (∑ j, ∫ y, star (y-x)*(kernel k x y : ℂ)*(b j).density y) =
          ∫ y, kernel k x y • (star (y-x)*h y) := by
    …

    Mentions: OAI.LocalCancellation.ErrorPiece

21. lemma OAI.LocalCancellation.moment_difference_decomposition line 334
22. lemma OAI.LocalCancellation.ball_pairing_decomposition line 355
23. theorem OAI.LocalCancellation.size_endpoint_raw line 366

    Source documentation

    The full raw band-endpoint size estimate. All maxima and both forced radii are simultaneous, with no measurable radius selection required.

    theorem size_endpoint_raw {Cs d t : ℝ} (b : ι → ErrorPiece Cs)
        (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 : ℕ, (
            (ENNReal.ofReal (t*(width d n)^(1/10 : ℝ)))⁻¹ ^ 2 *
              (ENNReal.ofReal (156*width d n/(width d n)^(1/5 : ℝ))*
                ENNReal.ofReal (coarseMass b (width d n) univ)*ENNReal.ofReal (coarseMass b (width d n) univ)) +
            (ENNReal.ofReal (t*(width d n)^(1/10 : ℝ)))⁻¹ *
              ((ENNReal.ofReal (6*Real.pi)*ENNReal.ofReal (2*(200*width d n/((width d n)^(1/5 : ℝ))^2)))*
    …

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

24. lemma OAI.DiskScales.first_power_identity line 423
25. lemma OAI.DiskScales.second_power_identity line 433
26. lemma OAI.DiskScales.endpoint_power_identity line 443
27. lemma OAI.DiskScales.shell_tail_scaled line 451

    Source documentation

    The two geometric failure mechanisms have integrable superlevel powers.

    lemma shell_tail_scaled {A t δ M : ℝ} (hA : 0 ≤ A) (ht : 0 < t)
        (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hM0 : 0 ≤ M)
        (hM : M ≤ A*δ^(-(1/50 : ℝ))) :
        (ENNReal.ofReal (t*δ^(1/10 : ℝ)))⁻¹ ^ 2 *
          (ENNReal.ofReal (156*δ/δ^(1/5 : ℝ))*ENNReal.ofReal M*ENNReal.ofReal M) +
        (ENNReal.ofReal (t*δ^(1/10 : ℝ)))⁻¹ *
          ((ENNReal.ofReal (6*Real.pi)*ENNReal.ofReal (2*(200*δ/(δ^(1/5 : ℝ))^2)))*ENNReal.ofReal M) ≤
        ENNReal.ofReal (156*(A/t)^2*δ^(14/25 : ℝ)+2400*Real.pi*(A/t)*δ^(9/25 : ℝ)) := by
    …

28. lemma OAI.DiskScales.endpoint_tail_scaled line 493
29. lemma OAI.DiskScales.norm_geometric_rpow_lt line 512
30. lemma OAI.DiskScales.raw_endpoint_tail_scaled line 515
31. lemma OAI.DiskScales.geometric_tail_sum line 534
32. lemma OAI.DiskScales.starting_width_tail line 555

    Source documentation

    After the initial-width choice d=A/t, the failure exponents are strictly larger than one, rather than the nonintegrable weak-(1,1) exponent.

    lemma starting_width_tail {A t : ℝ} (hA : 0 < A) (ht : 0 < t) :
        156*(A/t)^2*(A/t)^(14/25 : ℝ)/(1-(1/2 : ℝ)^(14/25 : ℝ))+
          2424*Real.pi*(A/t)*(A/t)^(9/25 : ℝ)/(1-(1/2 : ℝ)^(9/25 : ℝ)) =
        (156/(1-(1/2 : ℝ)^(14/25 : ℝ)))*(A/t)^(64/25 : ℝ)+
          (2424*Real.pi/(1-(1/2 : ℝ)^(9/25 : ℝ)))*(A/t)^(34/25 : ℝ) := by
    …

33. lemma OAI.DiskScales.size_start_identity line 577
34. lemma OAI.DiskScales.exists_size_parameters line 601

    Source documentation

    One fixed small-width cutoff enforces geometry and the strict endpoint size threshold at every smaller positive width.

    lemma exists_size_parameters (Cs : ℝ) :
        ∃ d₀ : ℝ, 0 < d₀ ∧ d₀ ≤ 1/4 ∧
          (∀ δ : ℝ, 0 < δ → δ ≤ d₀ → δ ≤ (δ^(1/5 : ℝ))^2/1600) ∧
          (∀ δ : ℝ, 0 < δ → δ ≤ d₀ →
            (1+216*Cs)*δ^(99/100 : ℝ)+
              (16+4538*Cs)*δ^(1/10 : ℝ)/(1-(1/2 : ℝ)^(1/10 : ℝ)) ≤ 1) := by
    …

35. def OAI.DiskScales.sizeTailConstant line 627
36. lemma OAI.DiskScales.sizeTailConstant_pos line 630
37. lemma OAI.DiskScales.collapse_size_tail line 636
38. theorem OAI.LocalCancellation.size_tail line 656

    Source documentation

    The uniform integrable superlevel tail, with both forced band endpoints. The only decomposition assumption is equality of the specified densities on each observation disk. No direction positivity is needed for this size bound.

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

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