OAI/Combinatorics/PlanarL1/ScaleHistory.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PlanarL1.Columns.Model.BState.Histories line 19

   Source documentation

   The auxiliary fields are the actual finite recorded histories, with a lower bound on every previously used scale. Empty fresh histories obey any bound.

   structure Histories (S : BState M κ lam Ω μ) (t : ℝ) where
   …

   Mentions: OAI.PlanarL1.Columns.Model.BState

2. def OAI.PlanarL1.Columns.Model.BState.Histories.weaken line 27
3. def OAI.PlanarL1.Columns.Model.BState.Histories.lift line 32
4. def OAI.PlanarL1.Columns.Model.BState.Histories.ofOrdinary line 37
5. def OAI.PlanarL1.Columns.Model.BState.Histories.append line 43
6. def OAI.PlanarL1.Columns.Model.BState.Histories.increment line 74
7. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.newData_recorded line 99
8. def OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.histories line 113
9. lemma OAI.PlanarL1.infDist_homothety line 132

   Source documentation

   The distance to a literal image scales under a surjective homothety, including the empty set convention for infDist.

   lemma infDist_homothety {X Y : Type*} [PseudoMetricSpace X] [PseudoMetricSpace Y]
       (f : X → Y) {q : ℝ} (hq : 0<q) (hd : ∀ x y, dist (f x) (f y)=q*dist x y)
       (x : X) (S : Set X) : Metric.infDist (f x) (f '' S)=q*Metric.infDist x S := by
   …

10. lemma OAI.PlanarL1.Increment.clamp_scale line 154
11. lemma OAI.PlanarL1.Increment.quadratic_scale line 158
12. lemma OAI.PlanarL1.Increment.low_scale line 165
13. lemma OAI.PlanarL1.Increment.high_scale line 170
14. lemma OAI.PlanarL1.Increment.positivePart_scale line 178
15. lemma OAI.PlanarL1.Increment.scalar_scale line 185
16. lemma OAI.PlanarL1.Increment.taper_scale line 193
17. lemma OAI.PlanarL1.Columns.Model.scale_univ line 209
18. lemma OAI.PlanarL1.Columns.Model.Point.dist_band_eq line 214
19. def OAI.PlanarL1.Columns.Model.Ambient.dilate line 223
20. def OAI.PlanarL1.Columns.Model.Ambient.scaleEquiv line 229
21. lemma OAI.PlanarL1.Columns.Model.Ambient.scaleEquiv_dist line 235
22. lemma OAI.PlanarL1.Columns.Model.Ambient.scaleEquiv_point line 241
23. def OAI.PlanarL1.Columns.Model.Ambient.History.dilate line 246
24. def OAI.PlanarL1.Columns.Model.Field.coordinateScale line 264
25. lemma OAI.PlanarL1.Columns.Model.Field.coordinateScale_dist line 267
26. lemma OAI.PlanarL1.Columns.Model.Field.dilate_wall line 272
27. lemma OAI.PlanarL1.Columns.Model.Field.dilate_transverseValue line 296
28. lemma OAI.PlanarL1.Columns.Model.Ambient.History.dilate_field line 313
29. lemma OAI.PlanarL1.Columns.Model.BData.dilate_recorded line 346
30. def OAI.PlanarL1.Columns.Model.BState.Histories.dilate line 361
31. lemma OAI.PlanarL1.Columns.Model.Field.ext_value line 379
32. def OAI.PlanarL1.Columns.Model.Point.reRoot line 387

    Source documentation

    Changing the bookkeeping root does not change a geometric point.

    def reRoot (h : (M.activeGraph I).Reachable s r) (x : M.Point I r) : M.Point I s :=
    …

33. lemma OAI.PlanarL1.Columns.Model.Point.reRoot_column line 389
34. lemma OAI.PlanarL1.Columns.Model.Point.reRoot_height line 391
35. lemma OAI.PlanarL1.Columns.Model.Point.reRoot_inverse line 393
36. lemma OAI.PlanarL1.Columns.Model.Point.dist_reRoot line 395
37. lemma OAI.PlanarL1.Columns.Model.Point.radialValue_reRoot line 398
38. lemma OAI.PlanarL1.Columns.Model.Point.radialField_reRoot line 406
39. lemma OAI.PlanarL1.Columns.Model.Field.eval_reRoot line 415
40. def OAI.PlanarL1.Columns.Model.Field.BandDescent.reRoot line 418
41. lemma OAI.PlanarL1.Columns.Model.Field.NoLowCircular.reRoot line 429
42. lemma OAI.PlanarL1.Columns.Model.Field.constant_no_descent line 439
43. lemma OAI.PlanarL1.Columns.Model.OrdinaryData.source_of_descent line 449

    Source documentation

    Constant ordinary charts cannot survive the genuine descending-path test. A surviving source is relocated to the bookkeeping root of the current band.

    lemma source_of_descent (D : OrdinaryData M) {root : Fin n}
        (x : M.Point D.band root) (hx : D.Contains x.column x.height)
        {ε : ℝ} (hε : ε < (1:ℝ)/100000)
        (hd : Nonempty (D.comparison.BandDescent J x ε)) :
        ∃ o : M.Point D.band root, D.comparison=o.radialField := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.OrdinaryData