PrefixSections.lean`

75 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Problem358.FinitePrefix.Coordinates line 11
def OAI.Problem358.FinitePrefix.append line 14
Source documentation
Append two finite coordinate blocks, with their usual sup norms.
```
def append (n m : ℕ) :
    (Coordinates n × Coordinates m) ≃L[ℝ] Coordinates (n + m) where
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates
theorem OAI.Problem358.FinitePrefix.append_apply line 24
def OAI.Problem358.FinitePrefix.join line 28
Source documentation
Reassemble a bounded prefix and its complementary coordinate block.
```
def join {n d : ℕ} (h : n ≤ d) :
    (Coordinates n × Coordinates (d - n)) ≃L[ℝ] Coordinates d :=
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates
def OAI.Problem358.FinitePrefix.leftIndex line 35
Source documentation
Index of a coordinate in the prefix.
```
def leftIndex {n d : ℕ} (h : n ≤ d) (i : Fin n) : Fin d := i.castLE h
```
def OAI.Problem358.FinitePrefix.rightIndex line 38
Source documentation
Index of a coordinate in the complementary block.
```
def rightIndex {n d : ℕ} (h : n ≤ d) (i : Fin (d - n)) : Fin d :=
…
```
theorem OAI.Problem358.FinitePrefix.join_left line 41
theorem OAI.Problem358.FinitePrefix.join_right line 49
def OAI.Problem358.FinitePrefix.headBlock line 57
Source documentation
The actual bounded prefix.
```
def headBlock {n d : ℕ} (h : n ≤ d) (x : Coordinates d) : Coordinates n :=
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates
def OAI.Problem358.FinitePrefix.tailBlock line 61
Source documentation
The remaining coordinates after a bounded prefix.
```
def tailBlock {n d : ℕ} (h : n ≤ d) (x : Coordinates d) : Coordinates (d - n) :=
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates
theorem OAI.Problem358.FinitePrefix.prefix_join line 64
theorem OAI.Problem358.FinitePrefix.suffix_join line 69
theorem OAI.Problem358.FinitePrefix.join_symm_apply line 74
theorem OAI.Problem358.FinitePrefix.join_prefix_suffix line 79
theorem OAI.Problem358.FinitePrefix.measurePreserving_append line 85
Source documentation
Appending coordinate blocks preserves the product Lebesgue measure.
```
theorem measurePreserving_append (n m : ℕ) :
    MeasurePreserving (append n m) (volume.prod volume) volume := by
…
```
Mentions: OAI.Problem358.FinitePrefix.append
theorem OAI.Problem358.FinitePrefix.measurePreserving_join line 102
Source documentation
The bounded-prefix coordinate split has unit Jacobian.
```
theorem measurePreserving_join {n d : ℕ} (h : n ≤ d) :
    MeasurePreserving (join h) (volume.prod volume) volume := by
…
```
Mentions: OAI.Problem358.FinitePrefix.join
theorem OAI.Problem358.FinitePrefix.measurePreserving_split line 108
Source documentation
The inverse split also preserves Lebesgue measure.
```
theorem measurePreserving_split {n d : ℕ} (h : n ≤ d) :
    MeasurePreserving (join h).symm volume (volume.prod volume) := by
…
```
Mentions: OAI.Problem358.FinitePrefix.join

theorem OAI.Problem358.FinitePrefix.measurePreserving_join_restrict line 114

Source documentation

Restriction to a body commutes with coordinate reassembly.

theorem measurePreserving_join_restrict {n d : ℕ} (h : n ≤ d)
    {K : Set (Coordinates d)} (hK : MeasurableSet K) :
    MeasurePreserving (join h)
      ((volume.prod volume).restrict (join h ⁻¹' K)) (volume.restrict K) :=
…

Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.join

theorem OAI.Problem358.FinitePrefix.continuous_headBlock line 120
theorem OAI.Problem358.FinitePrefix.continuous_tailBlock line 123
theorem OAI.Problem358.FinitePrefix.init_headBlock line 126
theorem OAI.Problem358.FinitePrefix.last_headBlock line 131
def OAI.Problem358.FinitePrefix.scalarBlock line 134
theorem OAI.Problem358.FinitePrefix.measurePreserving_scalarBlock line 137
def OAI.Problem358.FinitePrefix.tripleSplit line 143
Source documentation
Regroup a prefix, its next scalar coordinate, and the final remainder.
```
def tripleSplit {n d : ℕ} (h : n < d) :
    (Coordinates n × (ℝ × Coordinates (d - (n + 1)))) ≃L[ℝ] Coordinates d :=
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates
theorem OAI.Problem358.FinitePrefix.measurePreserving_tripleSplit line 152
theorem OAI.Problem358.FinitePrefix.tripleSplit_left line 161
theorem OAI.Problem358.FinitePrefix.tripleSplit_next line 170
theorem OAI.Problem358.FinitePrefix.headBlock_tripleSplit line 180
Source documentation
Taking the next prefix after installing a scalar is exactly Fin.snoc.
```
@[simp] theorem headBlock_tripleSplit {n d : ℕ} (h : n < d)
    (x : Coordinates n) (t : ℝ) (z : Coordinates (d - (n+1))) :
    headBlock (Nat.succ_le_of_lt h) (tripleSplit h (x,t,z)) = Fin.snoc x t := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.headBlock, OAI.Problem358.FinitePrefix.tripleSplit
theorem OAI.Problem358.FinitePrefix.snoc_mem_prefix_image line 192
Source documentation
Membership of the reconstructed point gives the precise next-prefix invariant.
```
theorem snoc_mem_prefix_image {n d : ℕ} (h : n < d)
    {K : Set (Coordinates d)} {x : Coordinates n} {t : ℝ}
    {z : Coordinates (d - (n+1))}
    (hy : tripleSplit h (x,t,z) ∈ interior K) :
    Fin.snoc x t ∈ headBlock (Nat.succ_le_of_lt h) '' interior K := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.tripleSplit, OAI.Problem358.FinitePrefix.headBlock
def OAI.Problem358.FinitePrefix.prefixDomain line 210
Source documentation
The valid coordinate prefixes are the projections of the body's interior.
```
def prefixDomain {d n : ℕ} (K : Set (Coordinates d)) (h : n ≤ d) : Set (Coordinates n) :=
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates
def OAI.Problem358.FinitePrefix.prefixSection line 214
Source documentation
The remaining section after a fixed coordinate prefix.
```
def prefixSection {d n : ℕ} (K : Set (Coordinates d)) (h : n ≤ d)
    (a : Coordinates n) : Set (Coordinates (d - n)) :=
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates
lemma OAI.Problem358.FinitePrefix.prefixDomain_iff line 218
lemma OAI.Problem358.FinitePrefix.isCompact_prefixSection line 227
lemma OAI.Problem358.FinitePrefix.prefixSection_interior_nonempty line 233
lemma OAI.Problem358.FinitePrefix.prefixSection_volume_pos line 240
lemma OAI.Problem358.FinitePrefix.prefixSection_volumeReal_pos line 245
lemma OAI.Problem358.FinitePrefix.measurable_prefixSection_volume line 252
lemma OAI.Problem358.FinitePrefix.join_zero line 257
lemma OAI.Problem358.FinitePrefix.prefixDomain_zero line 265
lemma OAI.Problem358.FinitePrefix.join_full line 271
lemma OAI.Problem358.FinitePrefix.prefixDomain_full line 276
lemma OAI.Problem358.FinitePrefix.prefixSection_full line 281
theorem OAI.Problem358.FinitePrefix.map_headBlock_restrict line 300
Source documentation
The density of an actual bounded coordinate prefix is the volume of its remaining-coordinate section. No convexity or positive-volume assumption is needed.
```
theorem map_headBlock_restrict {n d : ℕ} (h : n ≤ d)
    {K : Set (Coordinates d)} (hK : MeasurableSet K) :
    Measure.map (headBlock h) (volume.restrict K) =
      volume.withDensity (fun a : Coordinates n =>
        volume {b : Coordinates (d-n) | join h (a,b) ∈ K}) := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.headBlock, OAI.Problem358.FinitePrefix.join

theorem OAI.Problem358.FinitePrefix.map_headBlock_normalized_restrict line 316

Source documentation

Actual normalized prefix laws have the common normalization by full body volume, not by the individual section mass.

theorem map_headBlock_normalized_restrict {n d : ℕ} (h : n ≤ d)
    {K : Set (Coordinates d)} (hK : MeasurableSet K) :
    Measure.map (headBlock h) ((volume K)⁻¹ • volume.restrict K) =
      (volume K)⁻¹ • volume.withDensity (fun a : Coordinates n =>
        volume {b : Coordinates (d-n) | join h (a,b) ∈ K}) := by
…

Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.headBlock, OAI.Problem358.FinitePrefix.join

theorem OAI.Problem358.FinitePrefix.isOpenMap_headBlock line 337
Source documentation
Taking a bounded coordinate prefix is an open map, including the empty and the full prefix.
```
theorem isOpenMap_headBlock {n d : ℕ} (h : n ≤ d) :
    IsOpenMap (headBlock h) := by
…
```
Mentions: OAI.Problem358.FinitePrefix.headBlock
theorem OAI.Problem358.FinitePrefix.isOpen_prefixDomain line 344
Source documentation
The valid prefixes of a body form an open set.
```
theorem isOpen_prefixDomain {n d : ℕ} (K : Set (Coordinates d)) (h : n ≤ d) :
    IsOpen (prefixDomain K h) :=
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixDomain
theorem OAI.Problem358.FinitePrefix.ae_mem_prefixDomain_map line 350
Source documentation
Any law carried by the body's interior has its prefix law carried by the valid prefix domain. No choice of conditional law on bad prefixes is relevant.
```
theorem ae_mem_prefixDomain_map {n d : ℕ} {K : Set (Coordinates d)}
    (h : n ≤ d) {μ : Measure (Coordinates d)}
    (hμ : ∀ᵐ x ∂μ, x ∈ interior K) :
    ∀ᵐ a ∂Measure.map (headBlock h) μ, a ∈ prefixDomain K h := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.headBlock, OAI.Problem358.FinitePrefix.prefixDomain
theorem OAI.Problem358.FinitePrefix.ae_mem_interior_normalized_restrict line 361
Source documentation
Convex boundaries are null, so normalization of restricted volume does not place any mass on the boundary. Degenerate volume is allowed.
```
theorem ae_mem_interior_normalized_restrict {d : ℕ} {K : Set (Coordinates d)}
    (hK : Convex ℝ K) :
    ∀ᵐ x ∂((volume K)⁻¹ • volume.restrict K), x ∈ interior K := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates
theorem OAI.Problem358.FinitePrefix.ae_mem_prefixDomain_map_normalized_restrict line 373
Source documentation
The actual normalized prefix marginal is almost surely a valid interior prefix. This is the support input for geometric conditional quantiles.
```
theorem ae_mem_prefixDomain_map_normalized_restrict {n d : ℕ}
    {K : Set (Coordinates d)} (hK : Convex ℝ K) (h : n ≤ d) :
    ∀ᵐ a ∂Measure.map (headBlock h) ((volume K)⁻¹ • volume.restrict K),
      a ∈ prefixDomain K h :=
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.headBlock, OAI.Problem358.FinitePrefix.prefixDomain
theorem OAI.Problem358.FinitePrefix.map_normalized_restrict_compl_prefixDomain line 380
Source documentation
The same support statement as literal vanishing of the bad-prefix mass.
```
theorem map_normalized_restrict_compl_prefixDomain {n d : ℕ}
    {K : Set (Coordinates d)} (hK : Convex ℝ K) (h : n ≤ d) :
    (Measure.map (headBlock h) ((volume K)⁻¹ • volume.restrict K))
      (prefixDomain K h)ᶜ = 0 := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.headBlock, OAI.Problem358.FinitePrefix.prefixDomain

theorem OAI.Problem358.FinitePrefix.ae_sample_mem_prefixDomain line 388

Source documentation

A sampler with the actual prefix marginal almost surely reaches the valid prefix domain, independently of its values on parameter-null sets.

theorem ae_sample_mem_prefixDomain {A : Type*} [MeasurableSpace A]
    {n d : ℕ} {K : Set (Coordinates d)} (hK : Convex ℝ K) (h : n ≤ d)
    {η : Measure A} {F : A → Coordinates n} (hF : AEMeasurable F η)
    (hlaw : Measure.map F η =
      Measure.map (headBlock h) ((volume K)⁻¹ • volume.restrict K)) :
    ∀ᵐ a ∂η, F a ∈ prefixDomain K h := by
…

Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.headBlock, OAI.Problem358.FinitePrefix.prefixDomain

theorem OAI.Problem358.FinitePrefix.prefixSection_zero line 403
Source documentation
Before any coordinates are chosen, the remaining section is the full body.
```
@[simp] theorem prefixSection_zero {d : ℕ} (K : Set (Coordinates d))
    (a : Coordinates 0) :
    prefixSection K (Nat.zero_le d) a = K := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixSection
theorem OAI.Problem358.FinitePrefix.volume_prefixSection_zero line 410
Source documentation
The initial density is the volume of the full body.
```
@[simp] theorem volume_prefixSection_zero {d : ℕ} (K : Set (Coordinates d))
    (a : Coordinates 0) :
    volume (prefixSection K (Nat.zero_le d) a) = volume K := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixSection
theorem OAI.Problem358.FinitePrefix.volume_prefixSection_full line 416
Source documentation
A zero-dimensional terminal section has volume one on the body.
```
theorem volume_prefixSection_full {d : ℕ} {K : Set (Coordinates d)}
    {a : Coordinates d} (ha : a ∈ K) :
    volume (prefixSection K (le_refl d) a) = 1 := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixSection
theorem OAI.Problem358.FinitePrefix.volume_prefixSection_full_of_mem_domain line 423
Source documentation
In particular the terminal density is one at every valid full prefix.
```
theorem volume_prefixSection_full_of_mem_domain {d : ℕ} {K : Set (Coordinates d)}
    {a : Coordinates d} (ha : a ∈ prefixDomain K (le_refl d)) :
    volume (prefixSection K (le_refl d) a) = 1 := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixDomain, OAI.Problem358.FinitePrefix.prefixSection
theorem OAI.Problem358.FinitePrefix.volumeReal_prefixSection_zero line 429
theorem OAI.Problem358.FinitePrefix.volumeReal_prefixSection_full line 435
Source documentation
The terminal real density used by the telescoping derivative product.
```
theorem volumeReal_prefixSection_full {d : ℕ} {K : Set (Coordinates d)}
    {a : Coordinates d} (ha : a ∈ prefixDomain K (le_refl d)) :
    (volume (prefixSection K (le_refl d) a)).toReal = 1 := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixDomain, OAI.Problem358.FinitePrefix.prefixSection
theorem OAI.Problem358.FinitePrefix.prefixSection_full_of_not_mem line 441
Source documentation
A terminal section outside the body is empty.
```
theorem prefixSection_full_of_not_mem {d : ℕ} {K : Set (Coordinates d)}
    {a : Coordinates d} (ha : a ∉ K) :
    prefixSection K (le_refl d) a = ∅ := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixSection
theorem OAI.Problem358.FinitePrefix.volume_prefixSection_full_eq_indicator line 448
Source documentation
The full-prefix density is exactly the indicator of the body.
```
theorem volume_prefixSection_full_eq_indicator {d : ℕ} (K : Set (Coordinates d))
    (a : Coordinates d) :
    volume (prefixSection K (le_refl d) a) =
      K.indicator (fun _ => (1 : ℝ≥0∞)) a := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixSection

theorem OAI.Problem358.FinitePrefix.normalized_initial_prefix_law line 458

Source documentation

The normalized zero-prefix law is the unit-volume law on the empty product.

theorem normalized_initial_prefix_law {d : ℕ} {K : Set (Coordinates d)}
    (hK0 : volume K ≠ 0) (hKtop : volume K ≠ ⊤) :
    (volume K)⁻¹ • volume.withDensity
      (fun a : Coordinates 0 => volume (prefixSection K (Nat.zero_le d) a)) =
        (volume : Measure (Coordinates 0)) := by
…

Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixSection

theorem OAI.Problem358.FinitePrefix.terminal_prefix_law line 467
Source documentation
The terminal unnormalized prefix law is precisely restricted volume.
```
theorem terminal_prefix_law {d : ℕ} {K : Set (Coordinates d)}
    (hK : MeasurableSet K) :
    volume.withDensity
      (fun a : Coordinates d => volume (prefixSection K (le_refl d) a)) =
        volume.restrict K := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixSection

theorem OAI.Problem358.FinitePrefix.normalized_terminal_prefix_law line 476

Source documentation

Therefore the terminal normalized prefix law is the desired uniform law.

theorem normalized_terminal_prefix_law {d : ℕ} {K : Set (Coordinates d)}
    (hK : MeasurableSet K) :
    (volume K)⁻¹ • volume.withDensity
      (fun a : Coordinates d => volume (prefixSection K (le_refl d) a)) =
        (volume K)⁻¹ • volume.restrict K := by
…

Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.prefixSection

theorem OAI.Problem358.FinitePrefix.tripleSplit_right line 493
Source documentation
The final coordinates of the three-block split are its final input block.
```
@[simp] theorem tripleSplit_right {n d : ℕ} (h : n < d)
    (x : Coordinates n) (t : ℝ) (z : Coordinates (d - (n + 1)))
    (i : Fin (d - (n + 1))) :
    tripleSplit h (x, t, z) (rightIndex (Nat.succ_le_of_lt h) i) = z i := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.tripleSplit, OAI.Problem358.FinitePrefix.rightIndex
theorem OAI.Problem358.FinitePrefix.tailBlock_tripleSplit line 508
theorem OAI.Problem358.FinitePrefix.tripleSplit_eq_join_snoc line 515
Source documentation
A three-block split is the next prefix split after installing its scalar coordinate.
```
theorem tripleSplit_eq_join_snoc {n d : ℕ} (h : n < d)
    (x : Coordinates n) (t : ℝ) (z : Coordinates (d - (n + 1))) :
    tripleSplit h (x, t, z) = join (Nat.succ_le_of_lt h) (Fin.snoc x t, z) := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.tripleSplit, OAI.Problem358.FinitePrefix.join
def OAI.Problem358.FinitePrefix.tailJoin line 522
Source documentation
Regroup the next scalar coordinate with the remaining tail.
```
def tailJoin {n d : ℕ} (h : n < d) :
    (ℝ × Coordinates (d - (n + 1))) ≃L[ℝ] Coordinates (d - n) :=
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates
theorem OAI.Problem358.FinitePrefix.measurePreserving_tailJoin line 530
Source documentation
Regrouping a scalar and a tail has unit Jacobian.
```
theorem measurePreserving_tailJoin {n d : ℕ} (h : n < d) :
    MeasurePreserving (tailJoin h) (volume.prod volume) volume := by
…
```
Mentions: OAI.Problem358.FinitePrefix.tailJoin
theorem OAI.Problem358.FinitePrefix.tripleSplit_eq_join_tailJoin line 543
Source documentation
The same three-block split regrouped at the old prefix.
```
theorem tripleSplit_eq_join_tailJoin {n d : ℕ} (h : n < d)
    (x : Coordinates n) (t : ℝ) (z : Coordinates (d - (n + 1))) :
    tripleSplit h (x, t, z) = join h.le (x, tailJoin h (t, z)) := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.FinitePrefix.tripleSplit, OAI.Problem358.FinitePrefix.join, OAI.Problem358.FinitePrefix.tailJoin
theorem OAI.Problem358.FinitePrefix.tripleSplit_parentSection line 583
Source documentation
Fixing the old prefix gives exactly the old tail section, in regrouped coordinates.
```
theorem tripleSplit_parentSection {n d : ℕ} (h : n < d)
    (K : Set (Coordinates d)) (a : Coordinates n) :
    AffineSlice.fiber (tripleSplit h ⁻¹' K) a =
      tailJoin h ⁻¹' prefixSection K h.le a := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.AffineSlice.fiber, OAI.Problem358.FinitePrefix.tripleSplit, OAI.Problem358.FinitePrefix.tailJoin, OAI.Problem358.FinitePrefix.prefixSection
theorem OAI.Problem358.FinitePrefix.tripleSplit_parentSection_volume line 592
Source documentation
Parent section volume is unchanged by splitting off its next scalar coordinate.
```
theorem tripleSplit_parentSection_volume {n d : ℕ} (h : n < d)
    (K : Set (Coordinates d)) (a : Coordinates n) :
    (volume.prod volume) (AffineSlice.fiber (tripleSplit h ⁻¹' K) a) =
      volume (prefixSection K h.le a) := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.AffineSlice.fiber, OAI.Problem358.FinitePrefix.tripleSplit, OAI.Problem358.FinitePrefix.prefixSection
theorem OAI.Problem358.FinitePrefix.tripleSplit_parentSection_volumeReal line 601
Source documentation
Real-valued parent section volume, matching the conditional density denominator.
```
theorem tripleSplit_parentSection_volumeReal {n d : ℕ} (h : n < d)
    (K : Set (Coordinates d)) (a : Coordinates n) :
    (volume.prod volume).real (AffineSlice.fiber (tripleSplit h ⁻¹' K) a) =
      volume.real (prefixSection K h.le a) := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.AffineSlice.fiber, OAI.Problem358.FinitePrefix.tripleSplit, OAI.Problem358.FinitePrefix.prefixSection
theorem OAI.Problem358.FinitePrefix.tripleSplit_childSection line 608
Source documentation
The scalar child section is precisely the section at the extended prefix.
```
theorem tripleSplit_childSection {n d : ℕ} (h : n < d)
    (K : Set (Coordinates d)) (a : Coordinates n) (t : ℝ) :
    AffineSlice.fiber (AffineSlice.fiber (tripleSplit h ⁻¹' K) a) t =
      prefixSection K (Nat.succ_le_of_lt h) (Fin.snoc a t) := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.AffineSlice.fiber, OAI.Problem358.FinitePrefix.tripleSplit, OAI.Problem358.FinitePrefix.prefixSection
theorem OAI.Problem358.FinitePrefix.tripleSplit_childSection_volume line 617
Source documentation
Child section volume, matching the conditional density numerator.
```
theorem tripleSplit_childSection_volume {n d : ℕ} (h : n < d)
    (K : Set (Coordinates d)) (a : Coordinates n) (t : ℝ) :
    volume (AffineSlice.fiber (AffineSlice.fiber (tripleSplit h ⁻¹' K) a) t) =
      volume (prefixSection K (Nat.succ_le_of_lt h) (Fin.snoc a t)) := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.AffineSlice.fiber, OAI.Problem358.FinitePrefix.tripleSplit, OAI.Problem358.FinitePrefix.prefixSection
theorem OAI.Problem358.FinitePrefix.tripleSplit_childSection_volumeReal line 624
Source documentation
The real-valued child section identity used by inverse-CDF derivatives.
```
theorem tripleSplit_childSection_volumeReal {n d : ℕ} (h : n < d)
    (K : Set (Coordinates d)) (a : Coordinates n) (t : ℝ) :
    volume.real (AffineSlice.fiber (AffineSlice.fiber (tripleSplit h ⁻¹' K) a) t) =
      volume.real (prefixSection K (Nat.succ_le_of_lt h) (Fin.snoc a t)) := by
…
```
Mentions: OAI.Problem358.FinitePrefix.Coordinates, OAI.Problem358.AffineSlice.fiber, OAI.Problem358.FinitePrefix.tripleSplit, OAI.Problem358.FinitePrefix.prefixSection