MonotoneWeightVariation.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Variation of the smooth factors on monotone argument intervals

theorem OAI.Ostmann.discreteVariation_comp_monotone line 11
def OAI.Ostmann.clipRealInterval line 34
theorem OAI.Ostmann.clipRealInterval_bounds line 36
theorem OAI.Ostmann.clipRealInterval_monotone line 40
theorem OAI.Ostmann.compact_weight_clip line 46
Source documentation
Compact support allows clipping an unbounded monotone argument before applying the Lipschitz estimate. The cost depends on the support width.
```
theorem compact_weight_clip (Φ : ℝ → ℂ) (lo hi : ℝ) (h : lo ≤ hi)
    (hlo : Φ lo = 0) (hhi : Φ hi = 0)
    (hout : ∀ x, x < lo ∨ hi < x → Φ x = 0) (x : ℝ) :
    Φ (clipRealInterval lo hi x) = Φ x := by
…
```
Mentions: OAI.Ostmann.clipRealInterval
theorem OAI.Ostmann.discreteVariation_comp_compact_monotone line 62
theorem OAI.Ostmann.discreteVariation_comp_compact_antitone line 80

theorem OAI.Ostmann.discreteVariation_comp_monotoneOn line 100

Source documentation

Only bounds on the actual compact argument interval are needed.

theorem discreteVariation_comp_monotoneOn (Φ : ℝ → ℂ) (u : ℕ → ℝ)
    (lo hi B D : ℝ) (N : ℕ) (hD : 0 ≤ D)
    (hbound : ∀ x ∈ Set.Icc lo hi, ‖Φ x‖ ≤ B)
    (hlip : ∀ x ∈ Set.Icc lo hi, ∀ y ∈ Set.Icc lo hi,
      ‖Φ x - Φ y‖ ≤ D * |x - y|)
    (hrange : ∀ j ≤ N - 1, u j ∈ Set.Icc lo hi)
    (hmono : ∀ j < N - 1, u j ≤ u (j + 1)) :
    discreteVariation (fun j => Φ (u j)) N ≤ B + D * (hi - lo) := by
…

Mentions: OAI.Ostmann.discreteVariation

theorem OAI.Ostmann.discreteVariation_comp_antitoneOn line 125