SourceLabeledMotion.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Local motion of the actual labeled interval sums after removing the common vertical carrier. The concentration estimate is used only on the vertical segment through the initial point; horizontal derivatives are unconditional.

theorem OAI.LipschitzHilbert.SlopeBox.weight_slope_coordinates_le line 22

Source documentation

Comparing the two normalized coordinates controls the actual top weight, including away from the significant region.

theorem weight_slope_coordinates_le (T : SlopeBox) {K D : ℝ}
    (hK : 0 < K) (hD : 0 ≤ D) (x0 x1 y0 y1 : ℝ) :
    T.weight K D (x1, y1 + T.slope*x1) ≤
      Real.exp ((D/K) * (|x1-x0|/T.length + |y1-y0|/T.width)) *
        T.weight K D (x0, y0 + T.slope*x0) := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox

theorem OAI.LipschitzHilbert.SlopeBox.weight_slope_coordinates_local line 69

Source documentation

Motion through one top length and width costs only a fixed factor.

theorem weight_slope_coordinates_local (T : SlopeBox) {K D : ℝ}
    (hK : 1 ≤ K) (hD : 0 ≤ D) {x0 x1 y0 y1 : ℝ}
    (hx : |x1-x0| ≤ T.length) (hy : |y1-y0| ≤ T.width) :
    T.weight K D (x1, y1 + T.slope*x1) ≤
      Real.exp (2*D) * T.weight K D (x0, y0 + T.slope*x0) := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox

theorem OAI.LipschitzHilbert.SourceLabeledLattice.rawInterval_horizontal_differentiable line 92
theorem OAI.LipschitzHilbert.SourceLabeledLattice.rawInterval_vertical_differentiable line 101

theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_labeled_interval_motion line 116

Source documentation

The established interval concentration at the initial point, together with the unconditional derivative bound, gives carrier-free local motion for the original physical analyzing coefficients.

theorem source_labeled_interval_motion (p : ℝ) (D B : ℕ) :
    ∃ L0 : ℝ, 1 ≤ L0 ∧ (B : ℝ) ≤ L0 ∧ ∀ L : ℝ, L0 ≤ L →
      ∀ (N : ℕ) (κ : Type) (Label : Fin N → Type) (Item : ∀ j, Label j → Type)
        [Fintype κ] [∀ j l, Fintype (Item j l)]
        (P : SourceLabeledLattice N κ Label Item)
        (_hcard : ∀ j, (P.labels j).card ≤ B), P.constant ≤ L^p →
      ∀ (alt : ∀ j (l : P.labels j), Item j l → κ → SchwartzMap (ℝ × ℝ) ℂ)
        (hAlt : ∀ j l u k, planarProfileConstant (alt j l u k) (2*P.order) ≤ P.profileBound)
        (T : SlopeBox) (K : ℝ), 1 ≤ K → SourceLabeledTopGeometry P T K D →
      ∀ (cutoff : Fin N → ℝ) (v : ℝ × ℝ → ℝ), Measurable v →
      ∀ (g : ℝ × ℝ → EuclideanSpace ℂ κ), Measurable g → (∀ z, ‖g z‖ ≤ 1) →
      ∀ (lower upper : ℕ), lower ≤ upper → ∀ r : ℝ, 0 < r →
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SourceLabeledTopGeometry