SourceTiledLineIntegral.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Sum the source root-window estimates over the actual half-open tiling of a line. Local integrability comes from the marked-window theorem; it is not inferred from a vacuous Bochner-integral inequality.

def OAI.LipschitzHilbert.sourceLineTile line 18
theorem OAI.LipschitzHilbert.sourceLineTile_measurable line 20
theorem OAI.LipschitzHilbert.sourceLineTile_mem line 23
theorem OAI.LipschitzHilbert.sourceLineTile_pairwise line 31
theorem OAI.LipschitzHilbert.sourceLineTile_cover line 44
theorem OAI.LipschitzHilbert.sourceLineTile_length line 50
theorem OAI.LipschitzHilbert.finiteLineGrid_root_tile line 56

theorem OAI.LipschitzHilbert.source_tiled_line_integral line 64

Source documentation

Summable control of the local integrals gives global integrability and the same constant, with no dependence on the number of root windows.

theorem source_tiled_line_integral (H : ℝ) (hH : 0 < H) (f weight : ℝ → ℝ) (C : ℝ)
    (hf : ∀ x, 0 ≤ f x) (hw : Integrable weight volume)
    (hlocal : ∀ k : ℤ, IntegrableOn f (sourceLineTile H k) volume ∧
      (∫ x in sourceLineTile H k, f x) ≤ C*∫ x in sourceLineTile H k, weight x) :
    Integrable f volume ∧ (∫ x, f x) ≤ C*∫ x, weight x :=
…

Mentions: OAI.LipschitzHilbert.sourceLineTile

theorem OAI.LipschitzHilbert.SlopeBox.weight_line_integrable line 77
Source documentation
Every actual top-weight slice is integrable, including along a slope different from the top's own slope. Horizontal decay alone suffices.
```
theorem weight_line_integrable (T : SlopeBox) {K D : ℝ} (hK : 0 < K) (hD : 1 < D)
    (s y : ℝ) : Integrable (fun x => T.weight K D (x,y+s*x)) volume := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox

theorem OAI.LipschitzHilbert.source_top_tiled_line_integral line 106

Source documentation

Specialization to the original top weight removes the last auxiliary integrability premise in the source's whole-line gluing step.

theorem source_top_tiled_line_integral (T : SlopeBox) {K D : ℝ}
    (hK : 0 < K) (hD : 1 < D) (s y H C : ℝ) (hH : 0 < H)
    (f : ℝ → ℝ) (hf : ∀ x, 0 ≤ f x)
    (hlocal : ∀ k : ℤ, IntegrableOn f (sourceLineTile H k) volume ∧
      (∫ x in sourceLineTile H k, f x) ≤
        C*∫ x in sourceLineTile H k, T.weight K D (x,y+s*x)) :
    Integrable f volume ∧ (∫ x, f x) ≤ C*∫ x, T.weight K D (x,y+s*x) :=
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.sourceLineTile