MeasuredCoding.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FKCRT.timeCell line 13
Source documentation
Equal-Lebesgue-mass time cells. The endpoint one is assigned to the last cell; this retains a total, surjective coding without changing any mass.
```
def timeCell (N : ℕ) (hN : 0<N) (t : unitInterval) : Fin N :=
…
```
lemma OAI.FKCRT.timeCell_measurable line 16
lemma OAI.FKCRT.timeCell_of_lt_one line 27
lemma OAI.FKCRT.timeCell_eq_iff line 36
lemma OAI.FKCRT.cell_volume line 43
lemma OAI.FKCRT.timeCell_mass line 65
lemma OAI.FKCRT.timeCell_map line 78
lemma OAI.FKCRT.timeCell_surjective line 86
lemma OAI.FKCRT.timeCell_mono line 94
lemma OAI.FKCRT.timeCell_bounds line 99
def OAI.FKCRT.cellPoint line 117
Source documentation
The positive preorder point lies inside its equal-mass time cell.
```
def cellPoint (N : ℕ) (hN : 0<N) (i : Fin N) : unitInterval :=
…
```
lemma OAI.FKCRT.cellPoint_bounds line 120
lemma OAI.FKCRT.cellPoint_close line 132
lemma OAI.FKCRT.cellPoint_mono line 141
def OAI.FKCRT.Inventory.CoreTree.timeVertex line 159
Source documentation
The exact degree-mass coding, using every nonroot preorder pole.
```
def timeVertex (t : CoreTree) {n : ℕ} (M : FKCRT.RootedMap n)
    (e : t.Dart ≃ FKCRT.Dart n) (ht : 0<t.word.length) (s : unitInterval) : FKCRT.Vertex M :=
…
```
Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.RootedMap, OAI.FKCRT.Dart, OAI.FKCRT.Vertex
lemma OAI.FKCRT.Inventory.CoreTree.timeVertex_measurable line 163
lemma OAI.FKCRT.Inventory.CoreTree.timeVertex_surjective line 169

theorem OAI.FKCRT.Inventory.CoreTree.timeVertex_mass line 176

Source documentation

No asymptotic replacement of the degree measure is needed.

theorem timeVertex_mass (t : CoreTree) {n : ℕ} (M : FKCRT.RootedMap n)
    (e : t.Dart ≃ FKCRT.Dart n) (ht : 0<t.word.length)
    (hp : ∀ d,FKCRT.rotation M (e d)=e ((t.darts.formPerm*turns t.matching.first) d))
    (hlen : t.word.length=2*(n+1)) :
    @Measure.map _ _ inferInstance ⊤ (t.timeVertex M e ht) volume=FKCRT.degreeMass M := by
…

Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.RootedMap, OAI.FKCRT.Dart, OAI.FKCRT.rotation, OAI.FKCRT.degreeMass

lemma OAI.FKCRT.Inventory.CoreTree.realized_distance_of line 194

theorem OAI.FKCRT.Inventory.CoreTree.ghp_from_time_distortion line 217

Source documentation

Direct measured common-coding comparison of the actual finite map with any continuous excursion metric, with no unmeasured-GH substitution.

theorem ghp_from_time_distortion (t : CoreTree) {n : ℕ} (M : FKCRT.RootedMap n)
    (e : t.Dart ≃ FKCRT.Dart n) (ht : 0<t.word.length)
    (hp : ∀ d,FKCRT.rotation M (e d)=e ((t.darts.formPerm*turns t.matching.first) d))
    (hlen : t.word.length=2*(n+1)) (f : C(unitInterval,ℝ))
    {scale ε : ℝ} (hs : 0<scale) (hε : 0<ε)
    (hd : ∀ s u,|scale*((FKCRT.graph M Set.univ).dist (t.timeVertex M e ht s)
        (t.timeVertex M e ht u):ℝ)-FKCRT.excursionDist f s u|≤2*ε) :
    FKCRT.ghpEDist (FKCRT.mapSpace scale M) (FKCRT.treeSpace f)≤ENNReal.ofReal ε := by
…

Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.RootedMap, OAI.FKCRT.Dart, OAI.FKCRT.rotation, OAI.FKCRT.graph, OAI.FKCRT.excursionDist, OAI.FKCRT.ghpEDist, OAI.FKCRT.mapSpace, OAI.FKCRT.treeSpace

lemma OAI.FKCRT.cellPoint_interval_near line 246
lemma OAI.FKCRT.sampled_minimum_error line 275

theorem OAI.FKCRT.sampled_excursion_error line 297

Source documentation

Discrete positive preorder samples and their exact equal-mass coding approximate the continuous interval-minimum metric with its own modulus.

theorem sampled_excursion_error (N : ℕ) (hN : 0<N) (f : C(unitInterval,ℝ))
    {η : ℝ} (hmod : ∀ s t,dist s t ≤ 1/(N:ℝ) → |f s-f t| ≤ η)
    (s t : unitInterval) (hst : s ≤ t) (m : Fin N)
    (hsm : timeCell N hN s ≤  m) (hmt : m ≤  timeCell N hN t)
    (hm : ∀ i,timeCell N hN s ≤  i → i ≤  timeCell N hN t →
      f (cellPoint N hN m) ≤ f (cellPoint N hN i)) :
    |(f (cellPoint N hN (timeCell N hN s))+f (cellPoint N hN (timeCell N hN t))-
      2*f (cellPoint N hN m))-excursionDist f s t| ≤ 4*η := by
…

Mentions: OAI.FKCRT.timeCell, OAI.FKCRT.cellPoint, OAI.FKCRT.excursionDist

lemma OAI.FKCRT.Inventory.CoreTree.wordNodeEquiv_val line 323
lemma OAI.FKCRT.Inventory.CoreTree.nodeIndex_wordNodeEquiv_symm line 324
def OAI.FKCRT.Inventory.CoreTree.nodePoint line 329
Source documentation
Same-code positive mesh, with the omitted root still present at time zero.
```
def nodePoint (t : CoreTree) (v : t.Node) : unitInterval :=
…
```
Mentions: OAI.FKCRT.Inventory.CoreTree
lemma OAI.FKCRT.Inventory.CoreTree.nodePoint_nonroot line 336
lemma OAI.FKCRT.Inventory.CoreTree.normalized_pole_comparison line 341
lemma OAI.FKCRT.Inventory.CoreTree.exists_positive_index line 376
lemma OAI.FKCRT.Inventory.CoreTree.time_distortion_ordered line 386

theorem OAI.FKCRT.Inventory.CoreTree.time_distortion line 441

Source documentation

Uniform measured-space distortion from actual marked ancestral error, actual largest core, and the modulus of the chosen continuous path.

theorem time_distortion (t : CoreTree) {n : ℕ} (M : FKCRT.RootedMap n)
    (e : t.Dart ≃ FKCRT.Dart n) (ht : 0<t.word.length)
    (he : ∀ d,FKCRT.reversal M (e d)=e (t.matching.mate d))
    (hp : ∀ d,FKCRT.rotation M (e d)=e ((t.darts.formPerm*turns t.matching.first) d))
    (f : C(unitInterval,ℝ)) {scale ε η : ℝ} (hs : 0<scale)
    (herr : ∀ v,|scale*(t.routeLength v:ℝ)-f (t.nodePoint v)| ≤ ε)
    (hmod : ∀ s u,dist s u ≤ 1/(t.word.length:ℝ) → |f s-f u| ≤ η)
    (s u : unitInterval) :
    |scale*((FKCRT.graph M Set.univ).dist (t.timeVertex M e ht s)
      (t.timeVertex M e ht u):ℝ)-FKCRT.excursionDist f s u| ≤
        4*scale*(t.maxDegree:ℝ)+4*ε+4*η := by
…

Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.RootedMap, OAI.FKCRT.Dart, OAI.FKCRT.reversal, OAI.FKCRT.rotation, OAI.FKCRT.graph, OAI.FKCRT.excursionDist

theorem OAI.FKCRT.Inventory.CoreTree.ghp_tree_map_bound line 459

Source documentation

The measured comparison is oriented from the fixed continuous-tree space, precisely as required in the continuity tests.

theorem ghp_tree_map_bound (t : CoreTree) {n : ℕ} (M : FKCRT.RootedMap n)
    (e : t.Dart ≃ FKCRT.Dart n) (ht : 0<t.word.length)
    (he : ∀ d,FKCRT.reversal M (e d)=e (t.matching.mate d))
    (hp : ∀ d,FKCRT.rotation M (e d)=e ((t.darts.formPerm*turns t.matching.first) d))
    (hlen : t.word.length=2*(n+1)) (f : C(unitInterval,ℝ))
    {scale ε η δ : ℝ} (hs : 0<scale) (hδ : 0<δ)
    (herr : ∀ v,|scale*(t.routeLength v:ℝ)-f (t.nodePoint v)| ≤ ε)
    (hmod : ∀ s u,dist s u ≤ 1/(t.word.length:ℝ) → |f s-f u| ≤ η)
    (hsmall : 4*scale*(t.maxDegree:ℝ)+4*ε+4*η ≤ 2*δ) :
    FKCRT.ghpEDist (FKCRT.treeSpace f) (FKCRT.mapSpace scale M) ≤ ENNReal.ofReal δ := by
…

Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.RootedMap, OAI.FKCRT.Dart, OAI.FKCRT.reversal, OAI.FKCRT.rotation, OAI.FKCRT.ghpEDist, OAI.FKCRT.treeSpace, OAI.FKCRT.mapSpace