OAI/Analysis/SignedDisk/DiskScales1.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedDisk.DiskScales.norm_geometric_rpow_lt line 21
2. lemma OAI.SignedDisk.DiskScales.raw_endpoint_tail_scaled line 24
3. lemma OAI.SignedDisk.DiskScales.geometric_tail_sum line 43
4. lemma OAI.SignedDisk.DiskScales.starting_width_tail line 64

   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
   …

5. lemma OAI.SignedDisk.DiskScales.size_start_identity line 82
6. lemma OAI.SignedDisk.DiskScales.exists_size_parameters line 106

   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
   …

7. def OAI.SignedDisk.DiskScales.sizeTailConstant line 128
8. lemma OAI.SignedDisk.DiskScales.sizeTailConstant_pos line 131
9. lemma OAI.SignedDisk.DiskScales.collapse_size_tail line 137
10. theorem OAI.SignedDisk.LocalCancellation.size_tail line 157

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

11. def OAI.SignedDisk.DyadicMajorant.price line 218

    Source documentation

    A Borel price built from exceptions, rather than a measurability-dependent selection of maximizing radii.

    def price (t : ℝ) (E : ℕ → Set X) (x : X) : ℝ≥0∞ :=
    …

12. lemma OAI.SignedDisk.DyadicMajorant.measurable_price line 221
13. lemma OAI.SignedDisk.DyadicMajorant.majorizes line 229
14. lemma OAI.SignedDisk.DyadicMajorant.lintegral_price line 255
15. lemma OAI.SignedDisk.DyadicMajorant.weighted_geometric_sum line 271
16. lemma OAI.SignedDisk.DyadicMajorant.lintegral_price_geometric line 290
17. lemma OAI.SignedDisk.LocalCancellation.errorPrice_zero line 314
18. lemma OAI.SignedDisk.LocalCancellation.dyadic_ratio line 327
19. theorem OAI.SignedDisk.LocalCancellation.size_majorant line 337

    Source documentation

    A simultaneous Borel integrable price for every admissible disk gradient. The constant is independent of the number of pieces.

    theorem size_majorant {Cs : ℝ} (hCs : 0 ≤ Cs) :
        ∃ C : ℝ, 0 < C ∧ ∀ {ι : Type*} [Fintype ι] (b : ι → ErrorPiece Cs)
          (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 → ∑ j, (b j).density y = gradient g y) →
              ∀ r, EndpointRadius g x r →
                ENNReal.ofReal ‖∫ y in Metric.ball x r, gradient g y‖ ≤ F x := by
    …

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