OAI/Analysis/SignedDisk/LocalCancellation4.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SignedDisk.LocalCancellation.ConeDensity line 26

   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
   …

2. lemma OAI.SignedDisk.LocalCancellation.inner_unit_bound line 31
3. lemma OAI.SignedDisk.LocalCancellation.negative_projection_le_norm line 34
4. lemma OAI.SignedDisk.LocalCancellation.negative_projection_change line 38
5. lemma OAI.SignedDisk.LocalCancellation.cone_pairing line 48
6. lemma OAI.SignedDisk.LocalCancellation.cone_mass_of_nonpositive line 65

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

7. lemma OAI.SignedDisk.LocalCancellation.crossing_interpolation line 79

   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
   …

8. lemma OAI.SignedDisk.LocalCancellation.cone_corrected_cap line 95

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

9. lemma OAI.SignedDisk.LocalCancellation.corrected_error_bound line 148

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

10. lemma OAI.SignedDisk.LocalCancellation.increment_bound_general line 189
11. lemma OAI.SignedDisk.LocalCancellation.correction_kernel_bound line 218
12. lemma OAI.SignedDisk.LocalCancellation.corrected_inactive_bound line 227
13. lemma OAI.SignedDisk.last_active_bound line 249

    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
    …

14. lemma OAI.SignedDisk.last_active_limit line 278
15. lemma OAI.SignedDisk.LocalCancellation.real_weight_integrable line 291
16. lemma OAI.SignedDisk.LocalCancellation.real_weight_norm_integrable line 297
17. lemma OAI.SignedDisk.LocalCancellation.convex_pairing line 303
18. lemma OAI.SignedDisk.LocalCancellation.negative_gap_cap line 321

    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.SignedDisk.LocalCancellation.ConeDensity, OAI.SignedDisk.LocalCancellation.correction