Clipping.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PlanarL1.Clipping.envelope line 15
Source documentation
The literal capped frontier extension; the empty frontier contributes +infinity before taking the minimum, so the finite result is the cap.
```
noncomputable def envelope (S : Set X) (s : X → ℝ) (cap t : ℝ) (x : X) : ℝ := by
…
```
lemma OAI.PlanarL1.Clipping.envelope_le_cap line 19
lemma OAI.PlanarL1.Clipping.cost_continuousOn line 27
lemma OAI.PlanarL1.Clipping.inf_attained line 31
lemma OAI.PlanarL1.Clipping.envelope_le_cost line 42
lemma OAI.PlanarL1.Clipping.envelope_frontier line 50
lemma OAI.PlanarL1.Clipping.envelope_cases line 54
lemma OAI.PlanarL1.Clipping.envelope_one_sided line 67
lemma OAI.PlanarL1.Clipping.envelope_lipschitz line 78
def OAI.PlanarL1.Clipping.clip line 89
Source documentation
Single kept-cell clipping, before chart identifiers/rebasing.
```
noncomputable def clip (s F H : X → ℝ) (x : X) : ℝ := max (s x) (min (F x) (H x))
```
lemma OAI.PlanarL1.Clipping.clip_lipschitz line 91
lemma OAI.PlanarL1.Clipping.clip_unchanged line 98
lemma OAI.PlanarL1.Clipping.clip_movement line 106

lemma OAI.PlanarL1.Clipping.raise_or_descending_endpoint line 116

Source documentation

The source main raise-or-descend alternative, including the empty frontier. The radius interval is obtained from actual radial padding and weak diameter when this lemma is applied to the literal full-column frontier.

lemma raise_or_descending_endpoint {S : Set X} {s F H : X → ℝ}
    (hS : IsCompact S) (hs : ContinuousOn s S) (w : X) (cap ζ E ε : ℝ)
    (happrox : envelope S s cap (1-ζ) w-5*E ≤ F w)
    (hshield : s w+2*E < H w) (hcap : s w+7*E < cap)
    (hrad : ∀ z ∈ S, (0.00001:ℝ) ≤ dist w z ∧ dist w z ≤ 0.02)
    (hzeta : 0 ≤ ζ) (herr : ζ*0.02+7*E ≤ ε) :
    s w+2*E < clip s F H w ∨
      ∃ z ∈ S, (0.00001:ℝ) ≤ dist w z ∧ dist w z ≤ 0.02 ∧
        s z ≤ s w-dist w z+ε := by
…

Mentions: OAI.PlanarL1.Clipping.envelope, OAI.PlanarL1.Clipping.clip

def OAI.PlanarL1.Clipping.heightShield line 151
Source documentation
Literal trapezoidal height branch, constant outside the closed band.
```
noncomputable def heightShield (lo a s α H : ℝ) : ℝ :=
…
```
lemma OAI.PlanarL1.Clipping.heightShield_left line 154
lemma OAI.PlanarL1.Clipping.heightShield_right line 159
lemma OAI.PlanarL1.Clipping.heightShield_plateau line 164
lemma OAI.PlanarL1.Clipping.heightShield_bounds line 175
lemma OAI.PlanarL1.Clipping.heightShield_lipschitz line 184
def OAI.PlanarL1.Clipping.orderedBranch line 240
lemma OAI.PlanarL1.Clipping.orderedBranch_boundary line 243
lemma OAI.PlanarL1.Clipping.orderedBranch_seed line 249
lemma OAI.PlanarL1.Clipping.ordinary_boundary_margin line 258