LocalPredictionAssembly.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Assemble independently chosen current-cell predictors into the actual finite line-mesh majorant for a good-path product.

def OAI.LipschitzHilbert.FiniteLineGrid.patchedFactor line 17
theorem OAI.LipschitzHilbert.FiniteLineGrid.patchedFactor_constant line 20
theorem OAI.LipschitzHilbert.FiniteLineGrid.patchedFactor_average line 31

theorem OAI.LipschitzHilbert.lineCellMajorant_of_local_predictions line 51

Source documentation

The predictor at each coarse cell is patched by its actual mesh index. The accumulated error is paid once through its sum, including on a good set.

theorem lineCellMajorant_of_local_predictions
    (g : FiniteLineGrid) (T : SlopeBox) (K D y E : ℝ) (hK : 0 < K)
    (good : Set ℝ) (beta error : ℕ → ℝ → ℝ)
    (F : ℕ → Fin (g.branching ^ g.depth) → ℝ → ℝ)
    (hF0 : ∀ n < g.depth, ∀ i x, 0 ≤ F n i x)
    (hconstant : ∀ n < g.depth, ∀ i x z,
      g.index (n + 1) x = g.index (n + 1) z → F n i x = F n i z)
    (haverage : ∀ n < g.depth, ∀ i,
      (∫ x in {x | g.index n x = i}, F n i x ∂volume.restrict g.root) ≤
        (volume.restrict g.root).real {x | g.index n x = i})
    (hbeta : ∀ x ∈ g.root ∩ good, ∀ n < g.depth, 0 ≤ beta n x)
    (hcomparison : ∀ x ∈ g.root ∩ good, ∀ n < g.depth,
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.SlopeBox