SourceCellMarking.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's marking rule uses the infimum of the parent mass and the supremum of its absolute drop over the entire line cell. The possible unmarked large drop is the last active index, hence is unique.

def OAI.LipschitzHilbert.sourceMarkedCell line 14
Source documentation
The exact two inequalities in the source's cell marking rule.
```
def sourceMarkedCell (I : Set ℝ) (n h : ℝ → ℝ) (M : ℝ) : Prop :=
…
```
theorem OAI.LipschitzHilbert.sourceMarkedCell_active line 17
theorem OAI.LipschitzHilbert.sourceMarkedCell_inactive line 22
theorem OAI.LipschitzHilbert.sourceMarkedCell_drop line 30
Source documentation
Relative motion on the entire cell turns the supremum condition into a uniform positive absolute drop, also for a half-open cell.
```
theorem sourceMarkedCell_drop {I : Set ℝ} {n h : ℝ → ℝ} {M E x : ℝ}
    (hE : 0 < E) (hm : sourceMarkedCell I n h M) (hx : x ∈ I)
    (hmove : ∀ y ∈ I, h y ≤ E*h x) : (1/2:ℝ)/E ≤ h x := by
…
```
Mentions: OAI.LipschitzHilbert.sourceMarkedCell

theorem OAI.LipschitzHilbert.source_unmarked_large_drop line 40

Source documentation

If an unmarked cell contains a drop of at least one, its mass infimum is at most M. Relative motion bounds every mass by E*M.

theorem source_unmarked_large_drop {I : Set ℝ} {n h : ℝ → ℝ} {M E x : ℝ}
    (hE : 0 < E) (hx : x ∈ I) (hm : ¬ sourceMarkedCell I n h M)
    (hlarge : 1 ≤ h x) (hbounded : BddAbove (h '' I))
    (hmove : ∀ y ∈ I, n x ≤ E*n y) : n x ≤ E*M := by
…

Mentions: OAI.LipschitzHilbert.sourceMarkedCell

theorem OAI.LipschitzHilbert.source_unmarked_crosses_cutoff line 59

Source documentation

A unit absolute drop from a mass below M+1 crosses the stopping threshold. This is the exceptional index in the source decomposition.

theorem source_unmarked_crosses_cutoff {I : Set ℝ} {n next : ℝ → ℝ} {M E x : ℝ}
    (hE : 0 < E) (hx : x ∈ I)
    (hm : ¬ sourceMarkedCell I n (fun y => n y-next y) M)
    (hlarge : 1 ≤ n x-next x)
    (hbounded : BddAbove ((fun y => n y-next y) '' I))
    (hmove : ∀ y ∈ I, n x ≤ E*n y) (hsmall : E*M < M+1) : next x < M := by
…

Mentions: OAI.LipschitzHilbert.sourceMarkedCell

theorem OAI.LipschitzHilbert.source_cell_marking_cases line 70

Source documentation

The marked/unmarked dichotomy under the quantitative relative motion used for the actual source weights.

theorem source_cell_marking_cases (I : Set ℝ) (n next : ℝ → ℝ) (M q : ℝ)
    (hn : ∀ y ∈ I, 0 ≤ n y) (hq0 : 0 ≤ q) (hq1 : q ≤ 1)
    (hsmall : (1+q)*M < M+1)
    (hmove : ∀ x ∈ I, ∀ y ∈ I,
      n x ≤ (1+q)*n y ∧ n x-next x ≤ (1+q)*(n y-next y))
    (x : ℝ) (hx : x ∈ I) :
    (sourceMarkedCell I n (fun y => n y-next y) M →
      M < n x ∧ (1/4:ℝ) ≤ n x-next x) ∧
    (¬ sourceMarkedCell I n (fun y => n y-next y) M →
      1 ≤ n x-next x → n x < M+1 ∧ next x < M) := by
…

Mentions: OAI.LipschitzHilbert.sourceMarkedCell

theorem OAI.LipschitzHilbert.source_exceptional_index_unique line 99

Source documentation

Every exceptional unmarked large drop is the last active index. There can be only one, independently of the number of angular levels.

theorem source_exceptional_index_unique (n : ℕ → ℝ) (M : ℝ)
    (hanti : Antitone n) (exceptional : ℕ → Prop)
    (hactive : ∀ j, exceptional j → M < n j)
    (hstop : ∀ j, exceptional j → n (j+1) ≤ M) :
    Set.Subsingleton {j | exceptional j} := by
…