LineWeightAverage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Nested line averaging against the manuscript's actual top weight.

theorem OAI.LipschitzHilbert.SlopeBox.continuous_weight line 19

theorem OAI.LipschitzHilbert.SlopeBox.line_weight_comparable line 32

Source documentation

The top weight is comparable on a reference-line cell no longer than the top. The constant depends only on the fixed decay exponent.

theorem line_weight_comparable (T : SlopeBox) (origin transverse x : ℝ)
    {K D H : ℝ} (hK : 1 ≤ K) (hD : 0 ≤ D) (hH : H ≤ T.length)
    (hx : x ∈ Ico origin (origin + H)) :
    Real.exp (-D) * T.weight K D (origin, transverse + T.slope * origin) ≤
      T.weight K D (x, transverse + T.slope * x) ∧
    T.weight K D (x, transverse + T.slope * x) ≤
      Real.exp D * T.weight K D (origin, transverse + T.slope * origin) := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SlopeBox.transverse

theorem OAI.LipschitzHilbert.FiniteLineGrid.top_weight_average line 66

Source documentation

The actual mesh product may be averaged against a top's decaying weight. No cellwise weight-comparison hypothesis remains in the result.

theorem top_weight_average (g : FiniteLineGrid) (T : SlopeBox) (y : ℝ)
    {K D : ℝ} (hK : 1 ≤ K) (hD : 0 ≤ D) (hwidth : g.width ≤ T.length)
    (Γ : ℕ → ℝ → ℝ)
    (hΓ : ∀ n < g.depth, ∀ x, 0 ≤ Γ n x)
    (hconstant : ∀ n < g.depth, ∀ x z,
      g.index (n + 1) x = g.index (n + 1) z → Γ n x = Γ n z)
    (haverage : ∀ n < g.depth, ∀ i : Fin (g.branching ^ g.depth),
      (∫ x in {x | g.index n x = i}, Γ n x ∂volume.restrict g.root) ≤
        (volume.restrict g.root).real {x | g.index n x = i}) :
    Integrable (fun x => T.weight K D (x, y + T.slope * x) *
      ∏ n ∈ Finset.range g.depth, Γ n x) (volume.restrict g.root) ∧
    (∫ x in g.root, T.weight K D (x, y + T.slope * x) *
…

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