TriangularRecursion.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

Finite-prefix density normalization for the canonical triangular sampler. These are conditional identities, not existence of geometric section data.

abbrev OAI.Problem358.TriangularRecursion.ConditionalFamily line 11
Source documentation
Conditional scalar sampling functions indexed by the length of the existing prefix.
```
abbrev ConditionalFamily := (n : ℕ) → (Fin n → ℝ) → ℝ → ℝ
```

def OAI.Problem358.TriangularRecursion.sample line 14

Source documentation

Successive conditional sampling, using the last input coordinate at each step.

def sample (Q : ConditionalFamily) : (n : ℕ) → (Fin n → ℝ) → (Fin n → ℝ)
  | 0 => fun s => s
  | n + 1 => fun s =>
      Fin.snoc (sample Q n (Fin.init s))
        (Q n (sample Q n (Fin.init s)) (s (Fin.last n)))

Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily

theorem OAI.Problem358.TriangularRecursion.sample_init line 20
theorem OAI.Problem358.TriangularRecursion.sample_last line 24
theorem OAI.Problem358.TriangularRecursion.sample_snoc line 28
theorem OAI.Problem358.TriangularRecursion.measurable_sample line 33
Source documentation
Joint measurability of all conditional samplers gives a measurable full sampler.
```
theorem measurable_sample (Q : ConditionalFamily)
    (hQ : ∀ n, Measurable (fun p : (Fin n → ℝ) × ℝ => Q n p.1 p.2)) :
    ∀ n, Measurable (sample Q n) := by
…
```
Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.sample
theorem OAI.Problem358.TriangularRecursion.hasDerivAt_sample_last line 53
Source documentation
The earlier sampled coordinates remain fixed while the last parameter varies.
```
theorem hasDerivAt_sample_last (Q : ConditionalFamily) (n : ℕ)
    (s : Fin n → ℝ) {t v : ℝ} (hQ : HasDerivAt (Q n (sample Q n s)) v t) :
    HasDerivAt (fun u => sample Q (n+1) (Fin.snoc s u) (Fin.last n)) v t := by
…
```
Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.sample

theorem OAI.Problem358.TriangularRecursion.sample_mem_domains line 59

Source documentation

Conditional prefix-domain invariance propagates to the complete recursive sampler.

theorem sample_mem_domains (Q : ConditionalFamily)
    (D : (n : ℕ) → Set (Fin n → ℝ))
    (hzero : ∀ x, x ∈ D 0)
    (hstep : ∀ n x, x ∈ D n → ∀ t ∈ Set.Ioo (0 : ℝ) 1,
      Fin.snoc x (Q n x t) ∈ D (n+1)) :
    ∀ n s, (∀ i, s i ∈ Set.Ioo (0 : ℝ) 1) → sample Q n s ∈ D n := by
…

Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.sample

def OAI.Problem358.TriangularRecursion.take line 74
Source documentation
Restrict a coordinate tuple to an initial prefix.
```
def take {m n : ℕ} (h : m ≤ n) (s : Fin n → ℝ) : Fin m → ℝ :=
…
```
theorem OAI.Problem358.TriangularRecursion.sample_take line 78
Source documentation
Later random parameters do not affect an earlier sampled prefix.
```
theorem sample_take (Q : ConditionalFamily) {m n : ℕ} (h : m ≤ n) (s : Fin n → ℝ) :
    take h (sample Q n s) = sample Q m (take h s) := by
…
```
Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.take, OAI.Problem358.TriangularRecursion.sample
theorem OAI.Problem358.TriangularRecursion.sample_coordinate line 96
Source documentation
Every sampled coordinate is the corresponding conditional scalar sampler.
```
theorem sample_coordinate (Q : ConditionalFamily) (n : ℕ) (s : Fin n → ℝ) (i : Fin n) :
    sample Q n s i =
      Q i.val (sample Q i.val (take (Nat.le_of_lt i.isLt) s)) (s i) := by
…
```
Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.sample, OAI.Problem358.TriangularRecursion.take
theorem OAI.Problem358.TriangularRecursion.take_update line 113
Source documentation
Updating a coordinate leaves its earlier prefix unchanged.
```
theorem take_update {n : ℕ} (s : Fin n → ℝ) (i : Fin n) (t : ℝ) :
    take (Nat.le_of_lt i.isLt) (Function.update s i t) =
      take (Nat.le_of_lt i.isLt) s := by
…
```
Mentions: OAI.Problem358.TriangularRecursion.take
theorem OAI.Problem358.TriangularRecursion.sample_update_coordinate line 125
Source documentation
The diagonal section of the recursive map is exactly its conditional quantile.
```
theorem sample_update_coordinate (Q : ConditionalFamily) (n : ℕ)
    (s : Fin n → ℝ) (i : Fin n) (t : ℝ) :
    sample Q n (Function.update s i t) i =
      Q i.val (sample Q i.val (take (Nat.le_of_lt i.isLt) s)) t := by
…
```
Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.sample, OAI.Problem358.TriangularRecursion.take
theorem OAI.Problem358.TriangularRecursion.hasDerivAt_sample_coordinate line 132
Source documentation
Every diagonal derivative transfers directly from the corresponding conditional quantile.
```
theorem hasDerivAt_sample_coordinate (Q : ConditionalFamily) (n : ℕ)
    (s : Fin n → ℝ) (i : Fin n) {t v : ℝ}
    (hQ : HasDerivAt (Q i.val (sample Q i.val (take (Nat.le_of_lt i.isLt) s))) v t) :
    HasDerivAt (fun u => sample Q n (Function.update s i u) i) v t := by
…
```
Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.sample, OAI.Problem358.TriangularRecursion.take
def OAI.Problem358.TriangularRecursion.midpoint line 139
Source documentation
The coupled midpoint of two samplers driven by the same parameter tuple.
```
def midpoint (Q R : ConditionalFamily) (n : ℕ) (s : Fin n → ℝ) : Fin n → ℝ :=
…
```
Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily
def OAI.Problem358.TriangularRecursion.midpointFiber line 143
Source documentation
The last-coordinate midpoint fibre, with the original input prefix as parameter.
```
def midpointFiber (Q R : ConditionalFamily) (n : ℕ) (s : Fin n → ℝ) (t : ℝ) : ℝ :=
…
```
Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily
theorem OAI.Problem358.TriangularRecursion.midpoint_snoc line 147
Source documentation
This is the exact triangular decomposition required by iterated substitution.
```
theorem midpoint_snoc (Q R : ConditionalFamily) (n : ℕ) (s : Fin n → ℝ) (t : ℝ) :
    midpoint Q R (n+1) (Fin.snoc s t) =
      Fin.snoc (midpoint Q R n s) (midpointFiber Q R n s t) := by
…
```
Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.midpoint, OAI.Problem358.TriangularRecursion.midpointFiber
theorem OAI.Problem358.TriangularRecursion.measurable_midpoint line 156
Source documentation
Jointly measurable conditional families have jointly measurable sampled midpoints.
```
theorem measurable_midpoint (Q R : ConditionalFamily)
    (hQ : ∀ n, Measurable (fun p : (Fin n → ℝ) × ℝ => Q n p.1 p.2))
    (hR : ∀ n, Measurable (fun p : (Fin n → ℝ) × ℝ => R n p.1 p.2)) (n : ℕ) :
    Measurable (midpoint Q R n) := by
…
```
Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.midpoint
theorem OAI.Problem358.TriangularRecursion.hasDerivAt_midpointFiber line 166
Source documentation
Midpoint fibres have the arithmetic mean of the conditional derivatives.
```
theorem hasDerivAt_midpointFiber (Q R : ConditionalFamily) (n : ℕ)
    (s : Fin n → ℝ) {t a b : ℝ}
    (hQ : HasDerivAt (Q n (sample Q n s)) a t)
    (hR : HasDerivAt (R n (sample R n s)) b t) :
    HasDerivAt (midpointFiber Q R n s) ((a+b)/2) t :=
…
```
Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.sample, OAI.Problem358.TriangularRecursion.midpointFiber

theorem OAI.Problem358.TriangularRecursion.hasDerivAt_midpoint_coordinate line 174

Source documentation

Every diagonal derivative of the coupled midpoint is the corresponding average.

theorem hasDerivAt_midpoint_coordinate (Q R : ConditionalFamily) (n : ℕ)
    (s : Fin n → ℝ) (i : Fin n) {t a b : ℝ}
    (hQ : HasDerivAt (Q i.val (sample Q i.val (take (Nat.le_of_lt i.isLt) s))) a t)
    (hR : HasDerivAt (R i.val (sample R i.val (take (Nat.le_of_lt i.isLt) s))) b t) :
    HasDerivAt (fun u => midpoint Q R n (Function.update s i u) i) ((a+b)/2) t :=
…

Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.sample, OAI.Problem358.TriangularRecursion.take, OAI.Problem358.TriangularRecursion.midpoint

theorem OAI.Problem358.TriangularRecursion.measurable_midpointFiber line 183

Source documentation

A midpoint fibre is jointly measurable in its original prefix and last parameter.

theorem measurable_midpointFiber (Q R : ConditionalFamily)
    (hQ : ∀ n, Measurable (fun p : (Fin n → ℝ) × ℝ => Q n p.1 p.2))
    (hR : ∀ n, Measurable (fun p : (Fin n → ℝ) × ℝ => R n p.1 p.2)) (n : ℕ) :
    Measurable (fun p : (Fin n → ℝ) × ℝ => midpointFiber Q R n p.1 p.2) := by
…

Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.midpointFiber

theorem OAI.Problem358.TriangularRecursion.strictMonoOn_midpointFiber line 193
Source documentation
Strict monotonicity of the conditional quantiles makes the midpoint fibre strictly monotone.
```
theorem strictMonoOn_midpointFiber (Q R : ConditionalFamily) (n : ℕ)
    (s : Fin n → ℝ) {I : Set ℝ}
    (hQ : StrictMonoOn (Q n (sample Q n s)) I)
    (hR : StrictMonoOn (R n (sample R n s)) I) :
    StrictMonoOn (midpointFiber Q R n s) I := by
…
```
Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.sample, OAI.Problem358.TriangularRecursion.midpointFiber
abbrev OAI.Problem358.TriangularDensity.Coordinates line 218
def OAI.Problem358.TriangularDensity.InUnitCube line 220
lemma OAI.Problem358.TriangularDensity.InUnitCube.init line 222
lemma OAI.Problem358.TriangularDensity.InUnitCube.last line 225

def OAI.Problem358.TriangularDensity.diagonalProduct line 229

Source documentation

Recursive product of the canonical sampler's longitudinal derivatives.

def diagonalProduct (q dq : ConditionalFamily) : (n : ℕ) → Coordinates n → ℝ
  | 0, _ => 1
  | n + 1, u => diagonalProduct q dq n (Fin.init u) *
      dq n (sample q n (Fin.init u)) (u (Fin.last n))

Mentions: OAI.Problem358.TriangularDensity.Coordinates

theorem OAI.Problem358.TriangularDensity.diagonalProduct_snoc line 234
theorem OAI.Problem358.TriangularDensity.measurable_diagonalProduct_of_le line 242
Source documentation
The Jacobian product is measurable using only data up to the actual dimension. Sample measurability can be supplied by the bounded-depth sampler-law API.
```
theorem measurable_diagonalProduct_of_le (q dq : ConditionalFamily) (N : ℕ)
    (hQ : ∀ n, n ≤ N → Measurable (sample q n))
    (hD : ∀ n, n < N → Measurable (fun p : Coordinates n × ℝ => dq n p.1 p.2)) :
    ∀ n, n ≤ N → Measurable (diagonalProduct q dq n) := by
…
```
Mentions: OAI.Problem358.TriangularDensity.Coordinates, OAI.Problem358.TriangularDensity.diagonalProduct

theorem OAI.Problem358.TriangularDensity.measurable_geometric_diagonalProduct_of_le line 261

Source documentation

Measurability of the geometric Jacobian weight for two sampled families.

theorem measurable_geometric_diagonalProduct_of_le
    (q r dq dr : ConditionalFamily) (N : ℕ)
    (hQ : ∀ n, n ≤ N → Measurable (sample q n))
    (hR : ∀ n, n ≤ N → Measurable (sample r n))
    (hD : ∀ n, n < N → Measurable (fun p : Coordinates n × ℝ => dq n p.1 p.2))
    (hE : ∀ n, n < N → Measurable (fun p : Coordinates n × ℝ => dr n p.1 p.2))
    (n : ℕ) (hn : n ≤ N) :
    Measurable (fun u => ENNReal.ofReal (Real.sqrt
      (diagonalProduct q dq n u * diagonalProduct r dr n u))) :=
…

Mentions: OAI.Problem358.TriangularDensity.Coordinates, OAI.Problem358.TriangularDensity.diagonalProduct

theorem OAI.Problem358.TriangularDensity.sample_mem_domains_of_le line 274

Source documentation

Finite-cutoff domain induction: no quantile hypotheses above dimension N.

theorem sample_mem_domains_of_le (q : ConditionalFamily) (D : (n : ℕ) → Set (Coordinates n))
    (N : ℕ) (hzero : (fun i => Fin.elim0 i) ∈ D 0)
    (hstep : ∀ n, n < N → ∀ x, x ∈ D n → ∀ t ∈ Ioo (0 : ℝ) 1,
      Fin.snoc x (q n x t) ∈ D (n + 1)) :
    ∀ n, n ≤ N → ∀ u, InUnitCube u → sample q n u ∈ D n := by
…

Mentions: OAI.Problem358.TriangularDensity.Coordinates, OAI.Problem358.TriangularDensity.InUnitCube

theorem OAI.Problem358.TriangularDensity.diagonalProduct_eq_density_ratio_of_le line 291

Source documentation

Finite-cutoff telescoping for a genuinely finite collection of sections.

theorem diagonalProduct_eq_density_ratio_of_le
    (q dq : ConditionalFamily) (D : (n : ℕ) → Set (Coordinates n))
    (p : (n : ℕ) → Coordinates n → ℝ) (N : ℕ)
    (hzero : (fun i => Fin.elim0 i) ∈ D 0)
    (hstep : ∀ n, n < N → ∀ x, x ∈ D n → ∀ t ∈ Ioo (0 : ℝ) 1,
      Fin.snoc x (q n x t) ∈ D (n + 1))
    (hnonzero : ∀ n, n ≤ N → ∀ x, x ∈ D n → p n x ≠ 0)
    (hratio : ∀ n, n < N → ∀ x, x ∈ D n → ∀ t ∈ Ioo (0 : ℝ) 1,
      dq n x t = p n x / p (n + 1) (Fin.snoc x (q n x t))) :
    ∀ n, n ≤ N → ∀ u, InUnitCube u →
      diagonalProduct q dq n u = p 0 (fun i => Fin.elim0 i) / p n (sample q n u) := by
…

Mentions: OAI.Problem358.TriangularDensity.Coordinates, OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.TriangularDensity.diagonalProduct

def OAI.Problem358.TriangularDensity.diagonal line 320
Source documentation
The individual longitudinal derivative in each full-coordinate direction.
```
def diagonal (q dq : ConditionalFamily) (n : ℕ) (u : Coordinates n) (i : Fin n) : ℝ :=
…
```
Mentions: OAI.Problem358.TriangularDensity.Coordinates
theorem OAI.Problem358.TriangularDensity.diagonalProduct_eq_prod line 325
Source documentation
The recursively accumulated Jacobian is the product used by the finite arithmetic/geometric-mean bound.
```
theorem diagonalProduct_eq_prod (q dq : ConditionalFamily) :
    ∀ n u, diagonalProduct q dq n u = ∏ i : Fin n, diagonal q dq n u i := by
…
```
Mentions: OAI.Problem358.TriangularDensity.diagonalProduct, OAI.Problem358.TriangularDensity.diagonal

theorem OAI.Problem358.TriangularDensity.diagonalProduct_eq_initial_density line 337

Source documentation

At a terminal section whose density is one, the diagonal derivative product is the original body's volume, independent of all sampling parameters.

theorem diagonalProduct_eq_initial_density
    (q dq : ConditionalFamily) (D : (n : ℕ) → Set (Coordinates n))
    (p : (n : ℕ) → Coordinates n → ℝ) (N : ℕ)
    (hzero : (fun i => Fin.elim0 i) ∈ D 0)
    (hstep : ∀ n, n < N → ∀ x, x ∈ D n → ∀ t ∈ Ioo (0 : ℝ) 1,
      Fin.snoc x (q n x t) ∈ D (n + 1))
    (hnonzero : ∀ n, n ≤ N → ∀ x, x ∈ D n → p n x ≠ 0)
    (hratio : ∀ n, n < N → ∀ x, x ∈ D n → ∀ t ∈ Ioo (0 : ℝ) 1,
      dq n x t = p n x / p (n + 1) (Fin.snoc x (q n x t)))
    (hterminal : ∀ x ∈ D N, p N x = 1)
    (u : Coordinates N) (hu : InUnitCube u) :
    diagonalProduct q dq N u = p 0 (fun i => Fin.elim0 i) := by
…

Mentions: OAI.Problem358.TriangularDensity.Coordinates, OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.TriangularDensity.diagonalProduct

theorem OAI.Problem358.TriangularDensity.ae_inUnitCube line 367
Source documentation
The finite product of interval-restricted Lebesgue measures is concentrated on the open unit cube, including the zero-dimensional case.
```
theorem ae_inUnitCube (n : ℕ) :
    ∀ᵐ u ∂(Measure.pi fun _ : Fin n =>
      (volume : Measure ℝ).restrict (Ioo (0 : ℝ) 1)), InUnitCube u := by
…
```
Mentions: OAI.Problem358.TriangularDensity.InUnitCube
theorem OAI.Problem358.TriangularDensity.diagonalProduct_pos_of_le line 376
Source documentation
Positive longitudinal derivatives along valid sampled prefixes give a positive diagonal product. No assumptions above the finite cutoff are needed.
```
theorem diagonalProduct_pos_of_le (q dq : ConditionalFamily) (N : ℕ)
    (hpos : ∀ n, n < N → ∀ u, InUnitCube u → ∀ t ∈ Ioo (0 : ℝ) 1,
      0 < dq n (sample q n u) t) :
    ∀ n, n ≤ N → ∀ u, InUnitCube u → 0 < diagonalProduct q dq n u := by
…
```
Mentions: OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.TriangularDensity.diagonalProduct

theorem OAI.Problem358.TriangularDensity.diagonalProduct_pos_of_domains line 392

Source documentation

The domain-invariance form discharges sampled-prefix positivity directly from the conditional density data used to construct a sampler.

theorem diagonalProduct_pos_of_domains
    (q dq : ConditionalFamily) (D : (n : ℕ) → Set (Coordinates n)) (N : ℕ)
    (hzero : (fun i => Fin.elim0 i) ∈ D 0)
    (hstep : ∀ n, n < N → ∀ x, x ∈ D n → ∀ t ∈ Ioo (0 : ℝ) 1,
      Fin.snoc x (q n x t) ∈ D (n + 1))
    (hpos : ∀ n, n < N → ∀ x, x ∈ D n → ∀ t ∈ Ioo (0 : ℝ) 1,
      0 < dq n x t) :
    ∀ n, n ≤ N → ∀ u, InUnitCube u → 0 < diagonalProduct q dq n u := by
…

Mentions: OAI.Problem358.TriangularDensity.Coordinates, OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.TriangularDensity.diagonalProduct