OAI/Analysis/DiskMaximal/LocalPrices.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DyadicMajorant.price line 25

   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∞ :=
   …

2. lemma OAI.DyadicMajorant.measurable_price line 28
3. lemma OAI.DyadicMajorant.majorizes line 36
4. lemma OAI.DyadicMajorant.lintegral_price line 62
5. lemma OAI.DyadicMajorant.weighted_geometric_sum line 80
6. lemma OAI.DyadicMajorant.lintegral_price_geometric line 99
7. lemma OAI.LocalCancellation.errorPrice_zero line 123
8. lemma OAI.LocalCancellation.dyadic_ratio line 136
9. theorem OAI.LocalCancellation.size_majorant line 146

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

10. structure OAI.LocalCancellation.ConeDensity line 214

    Source documentation

    An integrable aggregate of vectors in a fixed acute cone. It covers the positive pieces by taking their sum; no direction is imposed on errors.

    structure ConeDensity (e : ℂ) (κ : ℝ) where
    …

11. lemma OAI.LocalCancellation.inner_unit_bound line 219
12. lemma OAI.LocalCancellation.negative_projection_le_norm line 222
13. lemma OAI.LocalCancellation.negative_projection_change line 226
14. lemma OAI.LocalCancellation.cone_pairing line 236
15. lemma OAI.LocalCancellation.cone_mass_of_nonpositive line 253

    Source documentation

    Nonpositive total projection bounds the weighted good mass by the error.

    lemma cone_mass_of_nonpositive {e : ℂ} {κ : ℝ} (a : ConeDensity e κ)
        (he : ‖e‖ = 1) (hκ : 0 < κ) {K : ℂ → ℝ} (hK : AEStronglyMeasurable K)
        (hK0 : ∀ y, 0 ≤ K y) (hK1 : ∀ y, K y ≤ 1) {p : ℂ}
        (hp : inner ℝ e ((∫ y, (K y : ℂ)*a.density y)+p) ≤ 0) :
        (∫ y, K y*‖a.density y‖) ≤ ‖p‖/κ := by
    …

    Mentions: OAI.LocalCancellation.ConeDensity

16. lemma OAI.LocalCancellation.crossing_interpolation line 267

    Source documentation

    Crossing the zero projection selects a genuine convex kernel, not an arbitrary discontinuous truncation.

    lemma crossing_interpolation (e p q : ℂ) (hq : inner ℝ e q < 0) :
        ∃ θ : ℝ, 0 ≤ θ ∧ θ ≤ 1 ∧
          inner ℝ e (θ • p+(1-θ) • q) ≤ 0 ∧
          max 0 (-inner ℝ e (θ • p+(1-θ) • q)) = max 0 (-inner ℝ e p) := by
    …

17. lemma OAI.LocalCancellation.cone_corrected_cap line 283

    Source documentation

    The cap cost of the good density is weighted interior mass, not its possibly enormous total mass.

    lemma cone_corrected_cap {a : ℂ → ℂ} (ha : Integrable a)
        {K L : ℂ → ℝ} (hK : AEStronglyMeasurable K) (hL : AEStronglyMeasurable L)
        (hK0 : ∀ y, 0 ≤ K y) (hK1 : ∀ y, K y ≤ 1)
        (hL0 : ∀ y, 0 ≤ L y) (hL1 : ∀ y, L y ≤ 1)
        {D : Set ℂ} (hD : MeasurableSet D) (hsupp : ∀ y, L y-K y ≠ 0 → y ∈ D)
        (x z : ℂ) {ρ : ℝ} (hρ : 0 ≤ ρ) (hz : (1 : ℝ)/2 ≤ ‖z-x‖)
        (hD3 : ∀ y ∈ D, ‖y-x‖ ≤ 3) :
        ‖∫ y, correction x z y*((L y : ℂ)-K y)*a y‖ ≤
          2*ρ*(∫ y, (L y+K y)*‖a y‖)+7*(∫ y in D \ Metric.ball z ρ, ‖a y‖) := by
    …

    Mentions: OAI.LocalCancellation.correction

18. lemma OAI.LocalCancellation.corrected_error_bound line 339

    Source documentation

    The error contribution to the corrected first active step; no moment cancellation for the errors alone is presumed.

    lemma corrected_error_bound {Cs α δ ρ : ℝ} (b : ι → ErrorPiece Cs) (hCs : 0 ≤ Cs)
        (hα : α ≤ 1) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (hρ : 0 ≤ ρ)
        {L : ℝ≥0} {F : ℂ → ℂ} (hF : LipschitzWith L F) {D : Set ℂ} (hD : MeasurableSet D)
        (hFb : ∀ y, ‖F y‖ ≤ 1) (hFD : ∀ y, F y ≠ 0 → y ∈ D) (x z : ℂ)
        (hz : (1 : ℝ)/2 ≤ ‖z-x‖) (hD3 : ∀ y ∈ D, ‖y-x‖ ≤ 3) :
        ‖∑ d, ∫ y, correction x z y*F y*(b d).density y‖ ≤
          2*ρ*coarseMass b δ univ+7*coarseMass b δ (D \ Metric.ball z ρ)+
          ((L : ℝ)+2*(3*(L : ℝ)+1))*Cs*δ^(2*(1-α))*errorPrice b α := by
    …

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

19. lemma OAI.LocalCancellation.increment_bound_general line 381
20. lemma OAI.LocalCancellation.correction_kernel_bound line 410
21. lemma OAI.LocalCancellation.corrected_inactive_bound line 419
22. lemma OAI.last_active_bound line 441

    Source documentation

    A finite last-active-index induction. Its hypotheses are local gaps, not an assumed global estimate, and no infinite list of active indices is chosen.

    lemma last_active_bound (active : ℕ → Prop) (N a : ℕ → ℝ) (B : ℝ)
        (ha : ∀ i, 0 ≤ a i)
        (hfirst : ∀ n, (∀ i < n, ¬active i) → N n ≤ B+∑ i ∈ Finset.range n, a i)
        (hgap : ∀ j n, j < n → active j → (∀ i, j < i → i < n → ¬active i) →
          N n ≤ N j+a j) : ∀ n, N n ≤ B+∑ i ∈ Finset.range n, a i := by
    …

23. lemma OAI.last_active_limit line 470
24. lemma OAI.LocalCancellation.real_weight_integrable line 483
25. lemma OAI.LocalCancellation.real_weight_norm_integrable line 489
26. lemma OAI.LocalCancellation.convex_pairing line 495
27. lemma OAI.LocalCancellation.negative_gap_cap line 513

    Source documentation

    Analytic comparison of two balanced mixtures at a negative later projection. The only error term is their fixed-correction difference.

    lemma negative_gap_cap {e : ℂ} {κ B ρ H : ℝ} (a : ConeDensity e κ)
        (he : ‖e‖ = 1) (hκ : 0 < κ) (hρ : 0 ≤ ρ)
        {K L : ℂ → ℝ} (hK : AEStronglyMeasurable K) (hL : AEStronglyMeasurable L)
        (hK0 : ∀ y, 0 ≤ K y) (hK1 : ∀ y, K y ≤ 1)
        (hL0 : ∀ y, 0 ≤ L y) (hL1 : ∀ y, L y ≤ 1)
        {D : Set ℂ} (hD : MeasurableSet D) (hsupp : ∀ y, L y-K y ≠ 0 → y ∈ D)
        (x z : ℂ) (hz : (1 : ℝ)/2 ≤ ‖z-x‖) (hD3 : ∀ y ∈ D, ‖y-x‖ ≤ 3)
        (hcap : (∫ y in D \ Metric.ball z ρ, ‖a.density y‖) ≤ H)
        {p q R : ℂ} (hp : ‖p‖ ≤ B) (hq : ‖q‖ ≤ B)
        (hneg : inner ℝ e ((∫ y, (L y : ℂ)*a.density y)+q) < 0)
        (hcor : ((∫ y, (L y : ℂ)*a.density y)+q)-((∫ y, (K y : ℂ)*a.density y)+p) =
          (∫ y, correction x z y*((L y : ℂ)-K y)*a.density y)+R) :
    …

    Mentions: OAI.LocalCancellation.ConeDensity, OAI.LocalCancellation.correction

28. lemma OAI.LocalCancellation.cone_negative_le_error line 606
29. lemma OAI.LocalCancellation.general_moment_integrable line 616
30. lemma OAI.LocalCancellation.correcting_pairing line 629
31. lemma OAI.LocalCancellation.general_kernel_pairing_sub line 646
32. lemma OAI.LocalCancellation.corrected_kernel_integrable line 657
33. lemma OAI.LocalCancellation.corrected_kernel_pairing_sub line 670
34. lemma OAI.LocalCancellation.interior_mass_le_kernel line 683