CommonPrices4.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SignedDisk.CommonPrices.physical_unfavorable_price line 34

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.SignedDisk.CommonPrices.badPrice, OAI.SignedDisk.CommonPrices.cellRoots, OAI.SignedDisk.CommonPrices.cellPrice

theorem OAI.SignedDisk.CommonPrices.physical_joint_price line 63

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.SignedDisk.CommonPrices.rootMass, OAI.SignedDisk.CommonPrices.cellRoots, OAI.SignedDisk.CommonPrices.cellPrice

lemma OAI.SignedDisk.PhysicalCells.real_weighted_patches line 108
lemma OAI.SignedDisk.CommonPrices.bad_total_level_budget line 135

theorem OAI.SignedDisk.CommonPrices.patched_unfavorable line 146

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
…

theorem OAI.SignedDisk.CommonPrices.patched_joint line 206

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) ≤
…

lemma OAI.SignedDisk.SignedRuns.master_from_patches line 273

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.SignedDisk.SignedRuns.unfavorable, OAI.SignedDisk.SignedRuns.runEnvelope

theorem OAI.SignedDisk.SignedRuns.smooth_compact_dyadic_band line 360

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.SignedDisk.SignedRuns.runEnvelope

def OAI.SignedDisk.WeakSobolev.HasGradient line 405
Source documentation
Directional, coordinate-free distributional gradient.
```
def HasGradient (f : E → ℝ) (g : E → E) : Prop :=
…
```
lemma OAI.SignedDisk.WeakSobolev.norm_convolution_le line 409
lemma OAI.SignedDisk.WeakSobolev.lipschitz_hasGradient line 422