ScalarTrees.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ScalarCancellation.positive_residual line 30

Source documentation

A nonnegative scalar residual retaining exactly the net mass. Its removal has the exact cancellation defect as L1 cost.

theorem positive_residual {α : Type*} [MeasurableSpace α] {μ : Measure α}
    {h : α → ℝ} (hh : Integrable h μ) (hc : 0 ≤ ∫ x, h x ∂μ) :
    ∃ ρ : α → ℝ, Integrable ρ μ ∧ (∀ x, 0 ≤ ρ x) ∧
      (∀ x, ρ x ≤ max (h x) 0) ∧ (∫ x, ρ x ∂μ) = ∫ x, h x ∂μ ∧
      (∫ x, |h x-ρ x| ∂μ) = (∫ x, |h x| ∂μ) - ∫ x, h x ∂μ ∧
      (∀ x, h x = 0 → ρ x = 0) := by
…

theorem OAI.ScalarCancellation.residual_split line 79

Source documentation

Every integrable scalar density splits into a constant-sign root and a zero-mass error, without replacing the actual terminal density by its mass.

theorem residual_split {α : Type*} [MeasurableSpace α] {μ : Measure α}
    {h : α → ℝ} (hh : Integrable h μ) :
    ∃ ρ β : α → ℝ, Integrable ρ μ ∧ Integrable β μ ∧
      (∀ x, h x = ρ x+β x) ∧ (∫ x, ρ x ∂μ) = ∫ x, h x ∂μ ∧
      (∫ x, β x ∂μ) = 0 ∧ (∫ x, |ρ x| ∂μ) = |∫ x, h x ∂μ| ∧
      (∫ x, |β x| ∂μ) = (∫ x, |h x| ∂μ)-|∫ x, h x ∂μ| ∧
      ((0 ≤ ∫ x, h x ∂μ) → ∀ x, 0 ≤ ρ x) ∧
      ((∫ x, h x ∂μ) < 0 → ∀ x, ρ x ≤ 0) ∧
      (∀ x, h x = 0 → ρ x = 0 ∧ β x = 0) := by
…

theorem OAI.ScalarCancellation.refinement_residual line 120

Source documentation

One backward refinement step. The new cancelling piece has cost no larger than the scalar norm defect of the children; overlap can only lower this cost.

theorem refinement_residual {α ι : Type*} [MeasurableSpace α] {μ : Measure α}
    [Fintype ι] (w : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (ρ : ι → α → ℝ)
    (hρ : ∀ i, Integrable (ρ i) μ) :
    ∃ R β : α → ℝ, Integrable R μ ∧ Integrable β μ ∧
      (∀ x, (∑ i, w i*ρ i x) = R x+β x) ∧
      (∫ x, R x ∂μ) = ∑ i, w i*(∫ x, ρ i x ∂μ) ∧
      (∫ x, β x ∂μ) = 0 ∧
      (∫ x, |R x| ∂μ) = |∑ i, w i*(∫ x, ρ i x ∂μ)| ∧
      (∫ x, |β x| ∂μ) ≤
        (∑ i, w i*(∫ x, |ρ i x| ∂μ))-|∑ i, w i*(∫ x, ρ i x ∂μ)| ∧
      ((0 ≤ ∑ i, w i*(∫ x, ρ i x ∂μ)) → ∀ x, 0 ≤ R x) ∧
      (∀ x, (∀ i, w i*ρ i x = 0) → R x = 0 ∧ β x = 0) := by
…

def OAI.ScalarCancellation.root line 169
Source documentation
Canonical positive/negative root selected from the proved scalar splitting, not an assumed decomposition.
```
def root (μ : Measure α) (f : α → ℝ) : α → ℝ := by
…
```
lemma OAI.ScalarCancellation.root_spec line 173
def OAI.ScalarCancellation.refined line 190
def OAI.ScalarCancellation.roots line 194
def OAI.ScalarCancellation.errors line 198
lemma OAI.ScalarCancellation.refined_integrable line 202
lemma OAI.ScalarCancellation.roots_integrable line 209
lemma OAI.ScalarCancellation.roots_mass line 216
lemma OAI.ScalarCancellation.roots_abs_mass line 227
lemma OAI.ScalarCancellation.errors_integrable line 239
lemma OAI.ScalarCancellation.errors_zero_mass line 248

theorem OAI.ScalarCancellation.errors_cost line 265

Source documentation

The whole scalar cancellation tree is built by backward splitting. Each nonterminal zero-mass piece costs at most its positive refinement norm defect.

theorem errors_cost (w : ℕ → ι → ι → ℝ) (hw : ∀ k q s, 0 ≤ w k q s)
    {f : ι → α → ℝ} (hf : ∀ q, Integrable (f q) μ) (k : ℕ) (q : ι) :
    (∫ x, |errors μ w f (k+1) q x| ∂μ) ≤
      (∑ s, w k q s*|∫ x, refined w f k s x ∂μ|)-|∫ x, refined w f (k+1) q x ∂μ| := by
…

Mentions: OAI.ScalarCancellation.errors, OAI.ScalarCancellation.refined

lemma OAI.ScalarCancellation.errors_terminal_cost line 290
lemma OAI.ScalarCancellation.error_recurrence line 295

theorem OAI.ScalarCancellation.roots_errors_support line 303

Source documentation

Support nesting is preserved by the new construction, even when child scalar masses vanish or overlapping densities cancel each other.

theorem roots_errors_support (w : ℕ → ι → ι → ℝ) {f : ι → α → ℝ}
    (hf : ∀ q, Integrable (f q) μ) (S : ℕ → ι → Set α)
    (hfS : ∀ q x, x ∉ S 0 q → f q x = 0)
    (hS : ∀ k q s, w k q s ≠ 0 → S k s ⊆ S (k+1) q) :
    ∀ k q x, x ∉ S k q → roots μ w f k q x = 0 ∧ errors μ w f k q x = 0 := by
…

Mentions: OAI.ScalarCancellation.roots, OAI.ScalarCancellation.errors

lemma OAI.ScalarCancellation.scalar_defect_sum line 334

theorem OAI.ScalarCancellation.errors_total_cost line 351

Source documentation

The total cancellation cost of all levels is bounded by the actual scalar input mass, independently of the number of refinement levels.

theorem errors_total_cost (w : ℕ → ι → ι → ℝ) (hw : ∀ k q s, 0 ≤ w k q s)
    (hcol : ∀ k s, ∑ q, w k q s = 1) {f : ι → α → ℝ}
    (hf : ∀ q, Integrable (f q) μ) (n : ℕ) :
    (∑ k ∈ range (n+1), ∑ q, ∫ x, |errors μ w f k q x| ∂μ) +
      (∑ q, |∫ x, refined w f n q x ∂μ|) ≤ ∑ q, ∫ x, |f q x| ∂μ := by
…

Mentions: OAI.ScalarCancellation.errors, OAI.ScalarCancellation.refined

lemma OAI.ScalarCancellation.errors_total_cost_le line 365

theorem OAI.ScalarCancellation.telescoped_decomposition line 376

Source documentation

Exact expansion in a coherent family of refinement coefficients. The finite zero-mass pieces are the explicitly constructed errors, not merely scalar mass certificates.

theorem telescoped_decomposition [DecidableEq ι] (w : ℕ → ι → ι → ℝ) (f : ι → α → ℝ)
    (Λ : ℕ → ℕ → ι → ι → ℝ)
    (hdiag : ∀ k q s, Λ k k q s = if q = s then 1 else 0)
    (hstep : ∀ k j q s, j ≤ k → Λ (k+1) j q s = ∑ a, w k q a*Λ k j a s)
    (k : ℕ) (q : ι) (x : α) :
    refined w f k q x = roots μ w f k q x +
      ∑ j ∈ range (k+1), ∑ s, Λ k j q s*errors μ w f j s x := by
…

Mentions: OAI.ScalarCancellation.refined, OAI.ScalarCancellation.roots, OAI.ScalarCancellation.errors