DirectLimits.lean`

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Conservative direct limits, profiles, and the exact real margin

def OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.of line 19
Source documentation
Canonical maps into the directed union, represented as a direct limit. No ambient monoid or model-existence hypothesis is needed.
```
def of (i : ι) : M i →* DirectLimit M f where
…
```
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.of_apply line 24
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.of_map line 27
instance OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.(instance at line 32) line 32
Source documentation
Left cancellation passes to a directed limit even without injective transition maps: each equation can be tested at a common later stage.
```
instance : LeftCancelMonoid (DirectLimit M f) where
…
```
instance OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.(instance at line 44) line 44
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.of_injective line 62
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.of_factors line 65
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.of_dvd_iff line 79
Source documentation
Divisibility in the union between two elements of one stage is exactly divisibility at that stage, with no new right factor.
```
theorem of_dvd_iff (i : ι) (x y : M i) : of f i x ∣ of f i y ↔ x ∣ y := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.of
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.of_conservative line 86
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.conditionalJoins line 111
Source documentation
Conditional joins in a conservative tower remain conditional joins in the union; pairs that never had a common right multiple acquire none.
```
theorem conditionalJoins (hM : ∀ i, HasConditionalJoins (LeftDivOrder (M i))) :
    HasConditionalJoins (LeftDivOrder (DirectLimit M f)) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins, OAI.PartitionConsistency.DiagramOrder.LeftDivOrder
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.probeProfile line 130
Source documentation
The successor persistence theorem passes to the full union. The path remains the original path; its downward closure is taken in the final monoid.
```
theorem probeProfile (i : ι) (a b e m : M i) (n : ℕ → M i)
    (hP : ∀ j (hij : i ≤ j),
      ProbeProfile (f i j hij a) (f i j hij b) (f i j hij e)
        (f i j hij m) (fun k => f i j hij (n k))) :
    ProbeProfile (of f i a) (of f i b) (of f i e) (of f i m)
      (fun k => of f i (n k)) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.ProbeProfile, OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.of
def OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.height line 181
def OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.cost line 184
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.height_of line 187
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.cost_of line 190
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.height_pos line 194
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.height_lt_one line 199
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.cost_pos line 204
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.cost_le_one line 209
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.cost_le_old_sup line 222
Source documentation
Costs of all later divisors, including those not present at the old stage, are uniformly bounded by the old missed-cost supremum.
```
theorem cost_le_old_sup (i : ι) (x y : LeftDivOrder (M i))
    (d : LeftDivOrder (DirectLimit M f))
    (hdy : d ≤ of f i y) (hdx : ¬ d ≤ of f i x) :
    cost f H hε d ≤ sSup ((H i).cost '' {a : LeftDivOrder (M i) | a ≤ y ∧ ¬ a ≤ x}) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.LeftDivOrder, OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.of, OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.cost
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.old_cost_supremum line 251
Source documentation
No supremum inflation occurs at limit stages. Merely preserving pointwise strict inequalities would not imply this statement.
```
theorem old_cost_supremum (i : ι) (x y : LeftDivOrder (M i)) :
    sSup (cost f H hε '' {d : LeftDivOrder (DirectLimit M f) |
      d ≤ of f i y ∧ ¬ d ≤ of f i x}) =
        sSup ((H i).cost '' {d : LeftDivOrder (M i) | d ≤ y ∧ ¬ d ≤ x}) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.LeftDivOrder, OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.cost, OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.of
def OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.heightCost line 295
Source documentation
Limit-stage extension of the exact real height/cost margin, using unchanged old suprema at every transition of the tower.
```
def heightCost : HeightCost (LeftDivOrder (DirectLimit M f)) where
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.HeightCost, OAI.PartitionConsistency.DiagramOrder.LeftDivOrder
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.heightCost_height_of line 316
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.heightCost_cost_of line 319
theorem OAI.PartitionConsistency.DiagramOrder.ConservativeLimit.cardinal_le line 335
Source documentation
The cardinal bound used at the limit stages of the schedule. This does not require injectivity, conservativity, or an algebraic structure.
```
theorem cardinal_le {μ : Cardinal.{u}} (hμ : Cardinal.aleph0 ≤ μ)
    (hι : Cardinal.mk ι ≤ μ) (hM : ∀ i, Cardinal.mk (M i) ≤ μ) :
    Cardinal.mk (DirectLimit M f) ≤ μ := by
…
```