OAI/Analysis/SignedDisk/LocalCancellation3.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SignedDisk.LocalCancellation.size_sequence line 25

   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.SignedDisk.LocalCancellation.ErrorPiece, OAI.SignedDisk.LocalCancellation.errorPrice, OAI.SignedDisk.LocalCancellation.coarseMass

2. def OAI.SignedDisk.DiskGeometry.endpointFailure line 122
3. lemma OAI.SignedDisk.DiskGeometry.endpoint_failure_bound line 126
4. lemma OAI.SignedDisk.DiskGeometry.active_away_from_endpoints line 140
5. def OAI.SignedDisk.DiskMoments.EndpointRadius line 157
6. lemma OAI.SignedDisk.DiskMoments.endpoint_kernel line 163

   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.SignedDisk.DiskMoments.EndpointRadius

7. lemma OAI.SignedDisk.LocalCancellation.moment_pairing_integrable line 193
8. lemma OAI.SignedDisk.LocalCancellation.moment_pairing_decomposition line 207

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

9. lemma OAI.SignedDisk.LocalCancellation.moment_difference_decomposition line 223
10. lemma OAI.SignedDisk.LocalCancellation.ball_pairing_decomposition line 244
11. theorem OAI.SignedDisk.LocalCancellation.size_endpoint_raw line 255

    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.SignedDisk.LocalCancellation.ErrorPiece, OAI.SignedDisk.LocalCancellation.errorPrice, OAI.SignedDisk.LocalCancellation.coarseMass

12. lemma OAI.SignedDisk.DiskScales.first_power_identity line 312
13. lemma OAI.SignedDisk.DiskScales.second_power_identity line 322
14. lemma OAI.SignedDisk.DiskScales.endpoint_power_identity line 332
15. lemma OAI.SignedDisk.DiskScales.shell_tail_scaled line 340

    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
    …

16. lemma OAI.SignedDisk.DiskScales.endpoint_tail_scaled line 382