OrderedSweep.lean`

55 declarations, 0 contain sorry, 0 declared as axioms

def OAI.BoundedTreewidthL1.OrderedSweepFlow.fiber line 12
def OAI.BoundedTreewidthL1.OrderedSweepFlow.mass line 16
def OAI.BoundedTreewidthL1.OrderedSweepFlow.bath line 19
def OAI.BoundedTreewidthL1.OrderedSweepFlow.total line 22
def OAI.BoundedTreewidthL1.OrderedSweepFlow.risk line 24
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.mem_fiber line 32
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.fiber_eq line 39
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.mass_pos line 44
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.bath_const_fiber line 49
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.bath_le line 54
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.le_bath line 62
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.fiber_lt line 70
theorem OAI.BoundedTreewidthL1.OrderedSweepFlow.bath_monotone line 79
theorem OAI.BoundedTreewidthL1.OrderedSweepFlow.bath_antitone line 91
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.bath_bounds line 103
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.bath_expand line 109
theorem OAI.BoundedTreewidthL1.OrderedSweepFlow.bath_total line 117
def OAI.BoundedTreewidthL1.OrderedSweepFlow.defect line 144
def OAI.BoundedTreewidthL1.OrderedSweepFlow.optimal line 147
def OAI.BoundedTreewidthL1.OrderedSweepFlow.labelReal line 150
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.defect_eq line 158
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.bath_mul line 169
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.defect_bath line 184
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.optimal_fiber line 196
theorem OAI.BoundedTreewidthL1.OrderedSweepFlow.optimal_monotone line 200
theorem OAI.BoundedTreewidthL1.OrderedSweepFlow.optimal_defect_le line 211
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.labelReal_bounds line 233
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.defect_mean_bound line 240
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.pair_mean_bound line 258

theorem OAI.BoundedTreewidthL1.OrderedSweepFlow.monotone_classifier line 274

Source documentation

On a chain of nested cuts, a monotone classifier determined by its trace on a bag is either constant or evaluation at one of that bag's vertices.

theorem monotone_classifier {P : Type*} (labels : α → P → Bool)
    (hl : ∀ p, Monotone (fun x => labels x p)) (c : α → Bool) (hc : Monotone c)
    (htrace : ∀ x y, (∀ p, labels x p = labels y p) → c x = c y) :
    c = (fun _ => false) ∨ c = (fun _ => true) ∨ ∃ p, c = (fun x => labels x p) := by
…

theorem OAI.BoundedTreewidthL1.OrderedSweepFlow.height_transport line 331

Source documentation

The height-gap transport estimate for a retained ordered sweep. f is the backward endpoint response; interval heat baths keep it monotone and preserve its mean. The comparison predictor may be arbitrarily randomized by the past.

theorem height_transport {P : Type*} (μ : α → ℝ) (hμ : ∀ x, 0 < μ x)
    (b : α → β) (hb : Monotone b) (labels : α → P → Bool)
    (hl : ∀ p, Monotone (fun x => labels x p))
    (htrace : ∀ x y, (∀ p, labels x p = labels y p) → b x = b y)
    (f p : α → ℝ) (hf : Monotone f) (hfb : ∀ x, 0 ≤ f x ∧ f x ≤ 1)
    (hp : ∀ x, 0 ≤ p x ∧ p x ≤ 1)
    (hpb : ∀ x y, b x = b y → p x = p y)
    (t : ℝ) (h0 : t ≤ total μ f) (h1 : t ≤ total μ (fun _ => 1) - total μ f)
    (hgap : ∀ v, t ≤ |total μ f - total μ (labelReal (fun x => labels x v))|) :
    t ≤ defect μ f p := by
…

Mentions: OAI.BoundedTreewidthL1.OrderedSweepFlow.total, OAI.BoundedTreewidthL1.OrderedSweepFlow.labelReal, OAI.BoundedTreewidthL1.OrderedSweepFlow.defect

def OAI.BoundedTreewidthL1.OrderedSweepFlow.execute line 370
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.execute_monotone line 373
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.execute_total line 382
lemma OAI.BoundedTreewidthL1.OrderedSweepFlow.execute_bounds line 390
def OAI.BoundedTreewidthL1.OrderedReservation.trueSet line 404
def OAI.BoundedTreewidthL1.OrderedReservation.Carrier line 408
instance OAI.BoundedTreewidthL1.OrderedReservation.(instance at line 410) line 410
def OAI.BoundedTreewidthL1.OrderedReservation.weight line 414
lemma OAI.BoundedTreewidthL1.OrderedReservation.weight_pos line 417
lemma OAI.BoundedTreewidthL1.OrderedReservation.exists_threshold line 421
lemma OAI.BoundedTreewidthL1.OrderedReservation.thresholds_nested line 434
lemma OAI.BoundedTreewidthL1.OrderedReservation.carrier_nested line 442
lemma OAI.BoundedTreewidthL1.OrderedReservation.trueSet_injective line 451
lemma OAI.BoundedTreewidthL1.OrderedReservation.rank_injective line 459
instance OAI.BoundedTreewidthL1.OrderedReservation.carrierOrder line 468
lemma OAI.BoundedTreewidthL1.OrderedReservation.labels_monotone line 471
def OAI.BoundedTreewidthL1.OrderedReservation.traceRank line 483
lemma OAI.BoundedTreewidthL1.OrderedReservation.traceRank_monotone line 486
lemma OAI.BoundedTreewidthL1.OrderedReservation.traceRank_fiber line 495
lemma OAI.BoundedTreewidthL1.OrderedReservation.sum_carrier line 524
lemma OAI.BoundedTreewidthL1.OrderedReservation.sum_event line 541
lemma OAI.BoundedTreewidthL1.OrderedReservation.label_mean line 549
lemma OAI.BoundedTreewidthL1.OrderedReservation.total_weight line 583

theorem OAI.BoundedTreewidthL1.OrderedReservation.sweep_height_transport line 598

Source documentation

Explicit descending-reservation transport on the original sweep measure. The chain may have any length, and testing and intermediate bags may repeat. There is no width assumption or Markov-flow hypothesis.

theorem sweep_height_transport (M : ℝ) (hM : 0 ≤ M) (F : V → ℝ)
    (hF : ∀ v, -M ≤ F v ∧ F v ≤ M) (z : V) (P : Finset V)
    (bags : List (Finset V)) (p : Carrier M F → ℝ)
    (hp : ∀ a, 0 ≤ p a ∧ p a ≤ 1)
    (hptrace : ∀ a b, (∀ v : P, a.val v = b.val v) → p a = p b)
    (t : ℝ) (hlo : t ≤ F z + M) (hhi : t ≤ M - F z)
    (hgap : ∀ v ∈ P, t ≤ |F z - F v|) :
    t ≤ defect (weight M F)
      (execute (weight M F) (bags.map (traceRank M F))
        (labelReal (fun a => a.val z))) p := by
…

Mentions: OAI.BoundedTreewidthL1.OrderedReservation.Carrier, OAI.BoundedTreewidthL1.OrderedReservation.weight, OAI.BoundedTreewidthL1.OrderedReservation.traceRank