OAI/Analysis/SignedDisk/DiskScales2.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedDisk.DiskScales.errorGapConstant line 21
2. def OAI.SignedDisk.DiskScales.directionGapConstant line 24
3. lemma OAI.SignedDisk.DiskScales.errorGapConstant_pos line 27
4. lemma OAI.SignedDisk.DiskScales.directionGapConstant_ge line 32
5. lemma OAI.SignedDisk.DiskScales.directionGapConstant_pos line 40
6. lemma OAI.SignedDisk.DiskScales.direction_cap_scale line 45
7. lemma OAI.SignedDisk.LocalCancellation.direction_sequence_point line 79

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

8. def OAI.SignedDisk.LocalCancellation.directionShellBound line 208
9. theorem OAI.SignedDisk.LocalCancellation.direction_sequence line 220

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

10. def OAI.SignedDisk.DiskMoments.NeighborhoodRadius line 274
11. lemma OAI.SignedDisk.DiskMoments.neighborhood_kernel line 278
12. lemma OAI.SignedDisk.LocalCancellation.mixed_moment_pairing_decomposition line 296
13. lemma OAI.SignedDisk.LocalCancellation.mixed_ball_pairing_decomposition line 315
14. theorem OAI.SignedDisk.LocalCancellation.direction_raw line 328

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

15. lemma OAI.SignedDisk.DiskScales.third_power_identity line 357
16. lemma OAI.SignedDisk.DiskScales.direction_shell_tail_scaled line 363
17. lemma OAI.SignedDisk.DiskScales.direction_start_identity line 415
18. lemma OAI.SignedDisk.DiskScales.exists_direction_parameters line 437