OAI/Analysis/DiskMaximal/BandBounds.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ActualLabels.spatialPriceConstant line 57
2. lemma OAI.ActualLabels.spatialPriceConstant_pos line 58
3. def OAI.ActualLabels.directPriceConstant line 65
4. lemma OAI.ActualLabels.directPriceConstant_pos line 66
5. lemma OAI.ActualLabels.pointCost_total_budget line 71
6. lemma OAI.ActualLabels.marginal_total_budget line 84
7. lemma OAI.CommonPrices.cellPrice_level_budget line 100
8. lemma OAI.CommonPrices.total_level_budget line 110
9. lemma OAI.ActualLabels.gradient_measurable line 121
10. lemma OAI.ActualLabels.marginal_continuous line 124
11. lemma OAI.ActualLabels.rate_continuous line 134
12. lemma OAI.ActualLabels.switchCost_continuous line 140
13. lemma OAI.ActualLabels.derivativeCost_measurable line 148
14. lemma OAI.ActualLabels.filt_measurable line 162
15. lemma OAI.ActualLabels.pointCost_measurable line 168
16. lemma OAI.PhysicalCells.sum_tsum_ofReal_le line 181
17. lemma OAI.PhysicalCells.integrated_weighted_patches line 192
18. lemma OAI.GeometricFilter.radius_convolution line 209
19. lemma OAI.SignedRuns.total_divergence_integrable line 227
20. lemma OAI.SignedRuns.total_flux_integrable line 239
21. lemma OAI.SignedRuns.band_gradient_integrable line 249
22. theorem OAI.SignedRuns.integrated_signed_master line 261

    Source documentation

    Integration of the signed master, with its actual history law. The only remaining inputs here are actual analytic majorants and their integrals; no unsigned sum of run gradients is introduced.

    theorem integrated_signed_master {g : ℂ → ℝ} (h : ℂ → ℂ) {r : ℕ → ℝ}
        (hg : ContDiff ℝ 1 g) (hc : HasCompactSupport g)
        (hr : ∀ k, 0 < r k) (hstep : ∀ k, 2*r (k+1) = r k)
        (H : ℕ → Label → ℂ → ℝ) (J : ℕ → ℂ → ℝ)
        (hH : ∀ k n x, 0 ≤ H k n x) (hJ : ∀ k x, 0 ≤ J k x)
        (old : Label) (m : ℕ)
        (hinterior : ∀ᵐ x, ∀ k n t, PhysicalNeighborhoodRadius g (r k) x t →
          unfavorable n (gradient (fun y => signedAverage g y t) x) ≤ H k n x)
        (hend : ∀ᵐ x, ∀ k t, PhysicalEndpointRadius g (r k) x t →
          ‖gradient (fun y => signedAverage g y t) x‖ ≤ J k x)
        (hvalue : ∀ᵐ x, ∀ k t t', 0 < t → t ≤ 4*r k → 0 < t' → t' ≤ 4*r k →
          |signedAverage g x t-signedAverage g x t'| ≤ r k*J k x)
    …

    Mentions: OAI.SignedRuns.unfavorable

23. theorem OAI.CommonPrices.physical_unfavorable_price line 343

    Source documentation

    Combine the two actual signed directional prices; the labels are unchanged.

    theorem physical_unfavorable_price : ∃ C : ℝ, 0 < C ∧
        ∀ {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R) (hN : R/r+1 ≤ (N:ℝ))
        {g : ℂ → ℝ}, ContDiff ℝ 1 g → Integrable (gradient g) →
        (∀ y, gradient g y ≠ 0 → ‖y‖ ≤ R) →
        (∃ D : ℝ, ∀ y, ‖fderiv ℝ g y‖ ≤ D) → ∀ (k : ℕ) (p : ℤ × ℤ) (n : Label),
        ∃ F : ℂ → ℝ≥0∞, Measurable F ∧
          (∫⁻ y in cell (point (scale r k) p) (scale r k), F y) ≤ ENNReal.ofReal
            (C*(badPrice (gradient g) r k (cellRoots N p) n+cellPrice N r (gradient g) k (cellRoots N p))) ∧
          ∀ y ∈ cell (point (scale r k) p) (scale r k), ∀ t,
            PhysicalNeighborhoodRadius g (scale r k) y t →
            ENNReal.ofReal (unfavorable n (gradient (fun z => signedAverage g z t) y)) ≤ F y := by
    …

    Mentions: OAI.CommonPrices.badPrice, OAI.CommonPrices.cellRoots, OAI.CommonPrices.cellPrice

24. theorem OAI.CommonPrices.physical_joint_price line 372

    Source documentation

    A single actual endpoint price pays both the gradient and the normalized oscillation. It is introduced before any spatial supremum is taken.

    theorem physical_joint_price : ∃ C : ℝ, 0 < C ∧
        ∀ {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R) (hN : R/r+1 ≤ (N:ℝ))
        {g : ℂ → ℝ}, ContDiff ℝ 1 g → Integrable (gradient g) →
        (∀ y, gradient g y ≠ 0 → ‖y‖ ≤ R) →
        (∃ D : ℝ, ∀ y, ‖fderiv ℝ g y‖ ≤ D) → ∀ (k : ℕ) (p : ℤ × ℤ) (n : Label),
        ∃ F : ℂ → ℝ≥0∞, Measurable F ∧
          (∫⁻ y in cell (point (scale r k) p) (scale r k), F y) ≤ ENNReal.ofReal
            (C*(rootMass (gradient g) r k (cellRoots N p)+cellPrice N r (gradient g) k (cellRoots N p))) ∧
          (∀ y ∈ cell (point (scale r k) p) (scale r k), ∀ t,
            PhysicalEndpointRadius g (scale r k) y t →
            ENNReal.ofReal ‖gradient (fun z => signedAverage g z t) y‖ ≤ F y) ∧
          (∀ y ∈ cell (point (scale r k) p) (scale r k), ∀ t t',
    …

    Mentions: OAI.CommonPrices.rootMass, OAI.CommonPrices.cellRoots, OAI.CommonPrices.cellPrice

25. lemma OAI.PhysicalCells.real_weighted_patches line 417
26. lemma OAI.CommonPrices.bad_total_level_budget line 444
27. theorem OAI.CommonPrices.patched_unfavorable line 455

    Source documentation

    Actual full-lattice unfavorable prices, with the genuine marginal law.

    theorem patched_unfavorable : ∃ C : ℝ, 0 < C ∧
        ∀ {N : ℕ} {base R : ℝ} (hb : 0 < base) (hR : 0 ≤ R) (hN : R/base+1 ≤ (N:ℝ))
        {g : ℂ → ℝ}, ContDiff ℝ 1 g → Integrable (gradient g) →
        (∀ y, gradient g y ≠ 0 → ‖y‖ ≤ R) →
        (∃ D : ℝ, ∀ y, ‖fderiv ℝ g y‖ ≤ D) →
        ∃ H : ℕ → Label → ℂ → ℝ,
          (∀ j n x, 0 ≤ H j n x) ∧ (∀ j n, Integrable (H j n)) ∧
          (∀ᵐ x, ∀ j n t, PhysicalNeighborhoodRadius g (scale base j) x t →
            unfavorable n (gradient (fun y => signedAverage g y t) x) ≤ H j n x) ∧
          (∀ m n, (∑ j ∈ range (m+1), ∫ x, marginal (gradient g) (geometricRadii base m) (m-j) x n*H j n x) ≤
            C*(∫ y, ‖gradient g y‖)) := by
    …

28. theorem OAI.CommonPrices.patched_joint line 519

    Source documentation

    Actual endpoint/value weights charged simultaneously at every level.

    theorem patched_joint : ∃ C : ℝ, 0 < C ∧
        ∀ {N : ℕ} {base R : ℝ} (hb : 0 < base) (hR : 0 ≤ R) (hN : R/base+1 ≤ (N:ℝ))
        {g : ℂ → ℝ}, ContDiff ℝ 1 g → Integrable (gradient g) →
        (∀ y, gradient g y ≠ 0 → ‖y‖ ≤ R) →
        (∃ D : ℝ, ∀ y, ‖fderiv ℝ g y‖ ≤ D) →
        ∃ J : ℕ → ℂ → ℝ,
          (∀ j x, 0 ≤ J j x) ∧ (∀ j, Integrable (J j)) ∧
          (∀ᵐ x, ∀ j t, PhysicalEndpointRadius g (scale base j) x t →
            ‖gradient (fun y => signedAverage g y t) x‖ ≤ J j x) ∧
          (∀ᵐ x, ∀ j t t', 0 < t → t ≤ 4*scale base j → 0 < t' → t' ≤ 4*scale base j →
            |signedAverage g x t-signedAverage g x t'| ≤ scale base j*J j x) ∧
          (∀ m, (∑ j ∈ range (m+1), ∫ x, pointCost (gradient g) (geometricRadii base m) x m (m-j)*J j x) ≤
    …

29. lemma OAI.SignedRuns.master_from_patches line 586

    Source documentation

    Reverse the spatial scale index and fill unused indices with genuine global Lipschitz bounds. Only the physical prices at indices at most m are integrated.

    lemma master_from_patches {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g) (hc : HasCompactSupport g)
        {base : ℝ} (hb : 0 < base) (m : ℕ)
        (H : ℕ → Label → ℂ → ℝ) (J : ℕ → ℂ → ℝ)
        (hH : ∀ j n x, 0 ≤ H j n x) (hJ : ∀ j x, 0 ≤ J j x)
        (hHi : ∀ j n, Integrable (H j n)) (hJi : ∀ j, Integrable (J j))
        (hinterior : ∀ᵐ x, ∀ j n t, PhysicalNeighborhoodRadius g (scale base j) x t →
          unfavorable n (gradient (fun y => signedAverage g y t) x) ≤ H j n x)
        (hend : ∀ᵐ x, ∀ j t, PhysicalEndpointRadius g (scale base j) x t →
          ‖gradient (fun y => signedAverage g y t) x‖ ≤ J j x)
        (hvalue : ∀ᵐ x, ∀ j t t', 0 < t → t ≤ 4*scale base j → 0 < t' → t' ≤ 4*scale base j →
          |signedAverage g x t-signedAverage g x t'| ≤ scale base j*J j x) :
        (∫ x, ‖gradient (runEnvelope g (geometricRadii base m) 0 m) x‖) ≤
    …

    Mentions: OAI.SignedRuns.unfavorable, OAI.SignedRuns.runEnvelope

30. theorem OAI.SignedRuns.smooth_compact_dyadic_band line 673

    Source documentation

    The genuine smooth signed dyadic finite-band estimate. No probability, common-price, local analytic estimate, or total variation bound is assumed.

    theorem smooth_compact_dyadic_band : ∃ C : ℝ, 0 < C ∧
        ∀ {g : ℂ → ℝ}, ContDiff ℝ 1 g → HasCompactSupport g →
        ∀ {base : ℝ}, 0 < base → ∀ m : ℕ,
        (∫ x, ‖gradient (runEnvelope g (geometricRadii base m) 0 m) x‖) ≤ C*(∫ x, ‖gradient g x‖) := by
    …

    Mentions: OAI.SignedRuns.runEnvelope