LocalCancellation1.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SignedDisk.LocalCancellation.integrable_lip_mul line 20

lemma OAI.SignedDisk.LocalCancellation.lip_cancellation line 39

Source documentation

Cancellation against the actual integrable complex error density.

lemma lip_cancellation {b F : ℂ → ℂ} (hb : Integrable b) (hzero : ∫ y, b y = 0)
    {L : ℝ≥0} (hF : LipschitzWith L F) (z : ℂ) {s : ℝ}
    (hsupp : ∀ᵐ y, b y ≠ 0 → ‖y-z‖ ≤ s) :
    ‖∫ y, F y * b y‖ ≤ (L : ℝ) * s * ∫ y, ‖b y‖ := by
…

lemma OAI.SignedDisk.LocalCancellation.bounded_pairing line 60
lemma OAI.SignedDisk.LocalCancellation.min_one_le_rpow line 68
structure OAI.SignedDisk.LocalCancellation.ErrorPiece line 79
def OAI.SignedDisk.LocalCancellation.ErrorPiece.mass line 89
lemma OAI.SignedDisk.LocalCancellation.ErrorPiece.mass_nonneg line 91

lemma OAI.SignedDisk.LocalCancellation.piece_discount line 95

Source documentation

The single-piece interpolation discount, with no smoothness assumed on the density.

lemma piece_discount {Cs α δ C : ℝ} (b : ErrorPiece Cs)
    (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (hδ : 0 < δ) (hδ1 : δ ≤ 1)
    (hC : 1 ≤ C) {L : ℝ≥0} {F : ℂ → ℂ} (hF : LipschitzWith L F)
    (hFb : ∀ y, ‖F y‖ ≤ 1) (hLC : (L : ℝ) * Cs ≤ C / δ) :
    ‖∫ y, F y * b.density y‖ ≤ C * (b.size / δ) ^ α * b.mass := by
…

Mentions: OAI.SignedDisk.LocalCancellation.ErrorPiece

lemma OAI.SignedDisk.LocalCancellation.position_lipschitz line 127

Source documentation

Multiplication by the position keeps a bounded-support Lipschitz test Lipschitz.

lemma position_lipschitz {F : ℂ → ℂ} {L M R : ℝ≥0} (hF : LipschitzWith L F)
    (hM : ∀ y, ‖F y‖ ≤ M) (x : ℂ)
    (hR : ∀ y, F y ≠ 0 → ‖y-x‖ ≤ R) :
    LipschitzWith (R*L+M) (fun y => star (y-x) * F y) := by
…

def OAI.SignedDisk.LocalCancellation.correction line 157
lemma OAI.SignedDisk.LocalCancellation.correction_eq line 159
lemma OAI.SignedDisk.LocalCancellation.norm_correction line 169
lemma OAI.SignedDisk.LocalCancellation.correction_cap_bound line 173
lemma OAI.SignedDisk.LocalCancellation.correction_bounded line 183

lemma OAI.SignedDisk.LocalCancellation.corrected_lipschitz line 194

Source documentation

Global Lipschitz control of the corrected increment test.

lemma corrected_lipschitz {F : ℂ → ℂ} {L M R H : ℝ≥0} (hF : LipschitzWith L F)
    (hM : ∀ y, ‖F y‖ ≤ M) (x z : ℂ)
    (hR : ∀ y, F y ≠ 0 → ‖y-x‖ ≤ R) (hH : ‖(star (z-x))⁻¹‖ ≤ H) :
    LipschitzWith (L+H*(R*L+M)) (fun y => correction x z y * F y) := by
…

Mentions: OAI.SignedDisk.LocalCancellation.correction

def OAI.SignedDisk.LocalCancellation.errorPrice line 216
lemma OAI.SignedDisk.LocalCancellation.errorPrice_nonneg line 219
lemma OAI.SignedDisk.LocalCancellation.square_rpow line 223
lemma OAI.SignedDisk.LocalCancellation.coarse_mass_mul_le line 227
lemma OAI.SignedDisk.LocalCancellation.fine_size_sum_le line 244
lemma OAI.SignedDisk.LocalCancellation.total_pairing_discount line 272

lemma OAI.SignedDisk.LocalCancellation.fine_pairing_bound line 289

Source documentation

All fine errors together retain the stronger, summable power of the width.

lemma fine_pairing_bound {Cs α δ : ℝ} (b : ι → ErrorPiece Cs) (hCs : 0 ≤ Cs)
    (hα : α ≤ 1) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1)
    {L : ℝ≥0} {F : ℂ → ℂ} (hF : LipschitzWith L F) :
    ‖∑ d ∈ Finset.univ.filter (fun d => (b d).size < δ^2), ∫ y, F y*(b d).density y‖ ≤
      (L : ℝ)*Cs*δ^(2*(1-α))*errorPrice b α := by
…

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

def OAI.SignedDisk.LocalCancellation.densityMeasure line 320
Source documentation
Norm total-variation measure of an actual complex density.
```
def densityMeasure (b : ℂ → ℂ) : Measure ℂ := volume.withDensity (fun y => ENNReal.ofReal ‖b y‖)
```
lemma OAI.SignedDisk.LocalCancellation.densityMeasure_apply line 322
lemma OAI.SignedDisk.LocalCancellation.densityMeasure_univ line 328
lemma OAI.SignedDisk.LocalCancellation.densityMeasure_finite line 332

lemma OAI.SignedDisk.LocalCancellation.pairing_majorant line 338

Source documentation

A cap decomposition bound, with all integrals over genuine densities.

lemma pairing_majorant {b F : ℂ → ℂ} (hb : Integrable b) {A : Set ℂ}
    (hA : MeasurableSet A) (c d : ℝ)
    (hF : ∀ y, ‖F y‖ ≤ c + d*A.indicator (fun _ => (1 : ℝ)) y) :
    ‖∫ y, F y*b y‖ ≤ c*(∫ y, ‖b y‖)+d*(∫ y in A, ‖b y‖) := by
…

lemma OAI.SignedDisk.LocalCancellation.moment_correction line 360

Source documentation

Cancellation of an exact complex moment allows an off-center correction.

lemma moment_correction {b F : ℂ → ℂ} (x z : ℂ)
    (hF : Integrable (fun y => F y*b y))
    (hM : Integrable (fun y => star (y-x)*F y*b y))
    (hzero : ∫ y, star (y-x)*F y*b y = 0) :
    (∫ y, F y*b y) = ∫ y, (1-star (y-x)/star (z-x))*F y*b y := by
…

lemma OAI.SignedDisk.LocalCancellation.corrected_pairing_cap line 372
lemma OAI.SignedDisk.LocalCancellation.supported_pairing line 396
def OAI.SignedDisk.LocalCancellation.coarseMeasure line 410
def OAI.SignedDisk.LocalCancellation.coarseMass line 413
lemma OAI.SignedDisk.LocalCancellation.coarseMass_nonneg line 416
lemma OAI.SignedDisk.LocalCancellation.coarseMeasure_apply line 419
instance OAI.SignedDisk.LocalCancellation.coarseMeasure_finite line 426
lemma OAI.SignedDisk.LocalCancellation.coarseMass_univ line 432
lemma OAI.SignedDisk.LocalCancellation.coarseMass_bound line 436

lemma OAI.SignedDisk.LocalCancellation.increment_bound line 442

Source documentation

The uncorrected increment costs only shell mass plus the fine-error discount.

lemma increment_bound {Cs α δ : ℝ} (b : ι → ErrorPiece Cs) (hCs : 0 ≤ Cs)
    (hα : α ≤ 1) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1)
    {L : ℝ≥0} {F : ℂ → ℂ} (hF : LipschitzWith L F) {D : Set ℂ} (hD : MeasurableSet D)
    (hFb : ∀ y, ‖F y‖ ≤ 1) (hFD : ∀ y, F y ≠ 0 → y ∈ D) :
    ‖∑ d, ∫ y, F y*(b d).density y‖ ≤
      coarseMass b δ D+(L : ℝ)*Cs*δ^(2*(1-α))*errorPrice b α := by
…

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