OAI/Analysis/Brenier/TriangularSampling.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.measurePreserving_finSnoc line 12

   Source documentation

   Appending the last coordinate identifies a finite product law with a product of its prefix law and its last-coordinate law.

   theorem measurePreserving_finSnoc {X : Type*} [MeasurableSpace X]
       (n : ℕ) (η : Measure X) [SigmaFinite η] :
       MeasurePreserving (fun p : (Fin n → X) × X => Fin.snoc p.1 p.2)
         ((Measure.pi fun _ : Fin n => η).prod η)
         (Measure.pi fun _ : Fin (n + 1) => η) := by
   …

2. theorem OAI.Problem358.measurePreserving_finInitLast line 26

   Source documentation

   Splitting the prefix and last coordinate preserves a finite product law.

   theorem measurePreserving_finInitLast {X : Type*} [MeasurableSpace X]
       (n : ℕ) (η : Measure X) [SigmaFinite η] :
       MeasurePreserving (fun x : Fin (n + 1) → X => (Fin.init x, x (Fin.last n)))
         (Measure.pi fun _ : Fin (n + 1) => η)
         ((Measure.pi fun _ : Fin n => η).prod η) := by
   …

3. theorem OAI.Problem358.TriangularSampling.map_prod_eq_compProd line 56

   Source documentation

   A measurable triangular sampler has the prescribed dependent-product law when its prefix has the prescribed law and its last coordinate has the prescribed conditional law almost everywhere.

   theorem map_prod_eq_compProd
       (μ : Measure A) (η : Measure B) (ρ : Measure X) (κ : Kernel X Y)
       [SFinite μ] [SFinite η] [SFinite ρ] [IsSFiniteKernel κ]
       (F : A → X) (G : A × B → Y)
       (hF : Measurable F) (hG : Measurable G)
       (hbase : Measure.map F μ = ρ)
       (hfiber : ∀ᵐ a ∂μ, Measure.map (fun b => G (a, b)) η = κ (F a)) :
       Measure.map (fun p : A × B => (F p.1, G p)) (μ.prod η) = ρ ⊗ₘ κ := by
   …

4. theorem OAI.Problem358.TriangularSampling.map_init_last_pi line 82

   Source documentation

   Splitting a finite product at its last coordinate preserves its product law.

   theorem map_init_last_pi {Z : Type*} [MeasurableSpace Z]
       (η : Measure Z) [SigmaFinite η] (n : ℕ) :
       Measure.map (fun s : Fin (n + 1) → Z => (Fin.init s, s (Fin.last n)))
         (Measure.pi (fun _ : Fin (n + 1) => η)) =
         (Measure.pi (fun _ : Fin n => η)).prod η := by
   …

5. theorem OAI.Problem358.TriangularSampling.map_snoc_pi_eq line 93

   Source documentation

   The last-coordinate induction step for the law of a finite triangular sampler.

   theorem map_snoc_pi_eq
       (n : ℕ) (η : Measure B) [SigmaFinite η]
       (ρ : Measure (Fin n → Y)) (κ : Kernel (Fin n → Y) Y)
       [SFinite ρ] [IsSFiniteKernel κ]
       (F : (Fin n → B) → (Fin n → Y)) (G : (Fin n → B) × B → Y)
       (hF : Measurable F) (hG : Measurable G)
       (hbase : Measure.map F (Measure.pi (fun _ : Fin n => η)) = ρ)
       (hfiber : ∀ᵐ a ∂Measure.pi (fun _ : Fin n => η),
         Measure.map (fun b => G (a, b)) η = κ (F a)) :
       Measure.map (fun s : Fin (n + 1) → B =>
         Fin.snoc (F (Fin.init s)) (G (Fin.init s, s (Fin.last n))))
         (Measure.pi (fun _ : Fin (n + 1) => η)) =
   …

6. theorem OAI.Problem358.TriangularSampling.map_sample_pi_eq line 150

   Source documentation

   Successive conditional quantiles sample a consistent family of prefix laws. The conditional law is needed only almost everywhere under the prescribed prefix law, so values of a quantile outside its valid prefix domain are irrelevant.

   theorem map_sample_pi_eq
       (Q : TriangularRecursion.ConditionalFamily)
       (hQ : ∀ n, Measurable (fun p : (Fin n → ℝ) × ℝ => Q n p.1 p.2))
       (η : Measure ℝ) [SigmaFinite η]
       (ρ : (n : ℕ) → Measure (Fin n → ℝ))
       (κ : (n : ℕ) → Kernel (Fin n → ℝ) ℝ)
       [∀ n, SFinite (ρ n)] [∀ n, IsSFiniteKernel (κ n)]
       (hzero : ρ 0 = Measure.pi (fun _ : Fin 0 => η))
       (hstep : ∀ n, ρ (n + 1) =
         Measure.map (fun p : (Fin n → ℝ) × ℝ =>
           (Fin.snoc p.1 p.2 : Fin (n + 1) → ℝ)) (ρ n ⊗ₘ κ n))
       (hfiber : ∀ n, ∀ᵐ x ∂ρ n, Measure.map (Q n x) η = κ n x) :
   …

   Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily

7. theorem OAI.Problem358.TriangularSampling.map_sample_pi_eq_of_steps line 188

   Source documentation

   A finite-dimensional version: only the first N disintegration identities and conditional laws are required. No consistency beyond the desired dimension is assumed.

   theorem map_sample_pi_eq_of_steps
       (N : ℕ) (Q : TriangularRecursion.ConditionalFamily)
       (hQ : ∀ n, Measurable (fun p : (Fin n → ℝ) × ℝ => Q n p.1 p.2))
       (η : Measure ℝ) [SigmaFinite η]
       (ρ : (n : ℕ) → Measure (Fin n → ℝ))
       (κ : (n : ℕ) → Kernel (Fin n → ℝ) ℝ)
       (hρ : ∀ n ≤ N, SFinite (ρ n))
       (hκ : ∀ n < N, IsSFiniteKernel (κ n))
       (hzero : ρ 0 = Measure.pi (fun _ : Fin 0 => η))
       (hstep : ∀ n < N, ρ (n + 1) =
         Measure.map (fun p : (Fin n → ℝ) × ℝ =>
           (Fin.snoc p.1 p.2 : Fin (n + 1) → ℝ)) (ρ n ⊗ₘ κ n))
   …

   Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily

8. theorem OAI.Problem358.map_triangular_recursion line 243

   Source documentation

   Law induction for triangular samplers with explicit conditional laws.

   theorem map_triangular_recursion
       {X : Type*} [MeasurableSpace X] (η : Measure X) [SigmaFinite η]
       (ν : (n : ℕ) → Measure (Fin n → X))
       (κ : (n : ℕ) → Kernel (Fin n → X) X)
       [∀ n, SFinite (ν n)] [∀ n, IsSFiniteKernel (κ n)]
       (F : (n : ℕ) → (Fin n → X) → (Fin n → X))
       (G : (n : ℕ) → ((Fin n → X) × X) → X)
       (hF : ∀ n, Measurable (F n)) (hG : ∀ n, Measurable (G n))
       (hzero : Measure.map (F 0) (Measure.pi fun _ : Fin 0 => η) = ν 0)
       (hrecursion : ∀ n s t,
         F (n + 1) (Fin.snoc s t) = Fin.snoc (F n s) (G n (s, t)))
       (htarget : ∀ n, ν (n + 1) =
   …

9. theorem OAI.Problem358.TriangularRecursion.map_sample_of_conditional_laws line 289

   Source documentation

   The law of the recursive sampler follows from conditional laws valid almost everywhere under the desired prefix law. No pointwise law on null prefixes is needed.

   theorem map_sample_of_conditional_laws
       (η : Measure ℝ) [SigmaFinite η]
       (Q : ConditionalFamily)
       (ν : (n : ℕ) → Measure (Fin n → ℝ))
       (κ : (n : ℕ) → Kernel (Fin n → ℝ) ℝ)
       [∀ n, SFinite (ν n)] [∀ n, IsSFiniteKernel (κ n)]
       (hQ : ∀ n, Measurable (fun p : (Fin n → ℝ) × ℝ => Q n p.1 p.2))
       (hzero : (Measure.pi fun _ : Fin 0 => η) = ν 0)
       (htarget : ∀ n, ν (n + 1) =
         Measure.map (fun p : (Fin n → ℝ) × ℝ => Fin.snoc p.1 p.2) (ν n ⊗ₘ κ n))
       (hfiber : ∀ n, ∀ᵐ x ∂ν n, Measure.map (Q n x) η = κ n x) :
       ∀ n, Measure.map (sample Q n) (Measure.pi fun _ : Fin n => η) = ν n := by
   …

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

10. theorem OAI.Problem358.TriangularRecursion.empty_prefix_law line 339

    Source documentation

    The empty-prefix base law is automatic for probability laws.

    theorem empty_prefix_law (η : Measure ℝ) [IsProbabilityMeasure η]
        (ν : Measure (Fin 0 → ℝ)) [IsProbabilityMeasure ν] :
        (Measure.pi fun _ : Fin 0 => η) = ν := by
    …

11. theorem OAI.Problem358.TriangularRecursion.map_sample_probability line 353

    Source documentation

    Probability-prefix form of the triangular sampling law.

    theorem map_sample_probability
        (η : Measure ℝ) [IsProbabilityMeasure η]
        (Q : ConditionalFamily)
        (ν : (n : ℕ) → Measure (Fin n → ℝ))
        (κ : (n : ℕ) → Kernel (Fin n → ℝ) ℝ)
        [∀ n, IsProbabilityMeasure (ν n)] [∀ n, IsSFiniteKernel (κ n)]
        (hQ : ∀ n, Measurable (fun p : (Fin n → ℝ) × ℝ => Q n p.1 p.2))
        (htarget : ∀ n, ν (n + 1) =
          Measure.map (fun p : (Fin n → ℝ) × ℝ => Fin.snoc p.1 p.2) (ν n ⊗ₘ κ n))
        (hfiber : ∀ n, ∀ᵐ x ∂ν n, Measure.map (Q n x) η = κ n x) :
        ∀ n, Measure.map (sample Q n) (Measure.pi fun _ : Fin n => η) = ν n :=
    …

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

12. def OAI.Problem358.TriangularRecursion.jointPlan line 376

    Source documentation

    Couple two triangular samplers by using the same independent scalar inputs.

    def jointPlan (η : Measure ℝ) (Q R : ConditionalFamily) (n : ℕ) :
        Measure ((Fin n → ℝ) × (Fin n → ℝ)) :=
    …

    Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily

13. theorem OAI.Problem358.TriangularRecursion.measurable_jointSample line 382

    Source documentation

    The joint sampler is measurable whenever both conditional families are measurable.

    theorem measurable_jointSample (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 s => (sample Q n s, sample R n s)) :=
    …

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

14. theorem OAI.Problem358.TriangularRecursion.isProbabilityMeasure_jointPlan line 389

    Source documentation

    The common-parameter joint law is a probability measure.

    theorem isProbabilityMeasure_jointPlan (η : Measure ℝ) [IsProbabilityMeasure η]
        (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 : ℕ) :
        IsProbabilityMeasure (jointPlan η Q R n) :=
    …

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

15. theorem OAI.Problem358.TriangularRecursion.map_fst_jointPlan line 398

    Source documentation

    Its first marginal is exactly the first sampler law.

    theorem map_fst_jointPlan (η : Measure ℝ) (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 : ℕ) :
        Measure.map Prod.fst (jointPlan η Q R n) =
          Measure.map (sample Q n) (Measure.pi fun _ : Fin n => η) := by
    …

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

16. theorem OAI.Problem358.TriangularRecursion.map_snd_jointPlan line 407

    Source documentation

    Its second marginal is exactly the second sampler law.

    theorem map_snd_jointPlan (η : Measure ℝ) (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 : ℕ) :
        Measure.map Prod.snd (jointPlan η Q R n) =
          Measure.map (sample R n) (Measure.pi fun _ : Fin n => η) := by
    …

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

17. theorem OAI.Problem358.TriangularRecursion.map_midpoint_jointPlan line 416

    Source documentation

    Taking the midpoint of the coupling is exactly the recursively decomposed midpoint law.

    theorem map_midpoint_jointPlan (η : Measure ℝ) (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 : ℕ) :
        Measure.map (fun p : (Fin n → ℝ) × (Fin n → ℝ) =>
          (1 / 2 : ℝ) • p.1 + (1 / 2 : ℝ) • p.2) (jointPlan η Q R n) =
          Measure.map (midpoint Q R n) (Measure.pi fun _ : Fin n => η) := by
    …

    Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.jointPlan, OAI.Problem358.TriangularRecursion.midpoint

18. theorem OAI.Problem358.TriangularRecursion.jointPlan_spec_of_laws line 430

    Source documentation

    A fixed-depth coupling certificate needs only the two measurable full samplers and their laws, so it also applies to finite-depth conditional families.

    theorem jointPlan_spec_of_laws (η : Measure ℝ) [IsProbabilityMeasure η]
        (Q R : ConditionalFamily) (n : ℕ)
        {ν μ : Measure (Fin n → ℝ)}
        (hQ : Measurable (sample Q n)) (hR : Measurable (sample R n))
        (hν : Measure.map (sample Q n) (Measure.pi fun _ : Fin n => η) = ν)
        (hμ : Measure.map (sample R n) (Measure.pi fun _ : Fin n => η) = μ) :
        IsProbabilityMeasure (jointPlan η Q R n) ∧
          Measure.map Prod.fst (jointPlan η Q R n) = ν ∧
          Measure.map Prod.snd (jointPlan η Q R n) = μ ∧
          Measure.map (fun p : (Fin n → ℝ) × (Fin n → ℝ) =>
            (1 / 2 : ℝ) • p.1 + (1 / 2 : ℝ) • p.2) (jointPlan η Q R n) =
            Measure.map (midpoint Q R n) (Measure.pi fun _ : Fin n => η) := by
    …

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

19. theorem OAI.Problem358.TriangularRecursion.measurable_sample_upto line 465

    Source documentation

    Measurability only requires the conditional samplers used before the given depth.

    theorem measurable_sample_upto (Q : ConditionalFamily) (d : ℕ)
        (hQ : ∀ k, k < d → Measurable (fun p : (Fin k → ℝ) × ℝ => Q k p.1 p.2)) :
        ∀ n, n ≤ d → Measurable (sample Q n) := by
    …

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

20. theorem OAI.Problem358.TriangularRecursion.map_sample_of_conditional_laws_upto line 488

    Source documentation

    Finite-depth sampling law: no regularity or law hypotheses are imposed beyond d.

    theorem map_sample_of_conditional_laws_upto
        (η : Measure ℝ) [SigmaFinite η] (Q : ConditionalFamily) (d : ℕ)
        (ν : (n : ℕ) → Measure (Fin n → ℝ))
        (κ : (n : ℕ) → Kernel (Fin n → ℝ) ℝ)
        (hν : ∀ n, n ≤ d → SFinite (ν n))
        (hκ : ∀ n, n < d → IsSFiniteKernel (κ n))
        (hQ : ∀ n, n < d → Measurable (fun p : (Fin n → ℝ) × ℝ => Q n p.1 p.2))
        (hzero : (Measure.pi fun _ : Fin 0 => η) = ν 0)
        (htarget : ∀ n, n < d → ν (n + 1) =
          Measure.map (fun p : (Fin n → ℝ) × ℝ => Fin.snoc p.1 p.2) (ν n ⊗ₘ κ n))
        (hfiber : ∀ n, n < d → ∀ᵐ x ∂ν n, Measure.map (Q n x) η = κ n x) :
        ∀ n, n ≤ d → Measure.map (sample Q n) (Measure.pi fun _ : Fin n => η) = ν n := by
    …

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

21. theorem OAI.Problem358.TriangularRecursion.map_sample_probability_upto line 544

    Source documentation

    Probability-law form with the empty-prefix base case discharged automatically.

    theorem map_sample_probability_upto
        (η : Measure ℝ) [IsProbabilityMeasure η] (Q : ConditionalFamily) (d : ℕ)
        (ν : (n : ℕ) → Measure (Fin n → ℝ))
        (κ : (n : ℕ) → Kernel (Fin n → ℝ) ℝ)
        (hν : ∀ n, n ≤ d → IsProbabilityMeasure (ν n))
        (hκ : ∀ n, n < d → IsSFiniteKernel (κ n))
        (hQ : ∀ n, n < d → Measurable (fun p : (Fin n → ℝ) × ℝ => Q n p.1 p.2))
        (htarget : ∀ n, n < d → ν (n + 1) =
          Measure.map (fun p : (Fin n → ℝ) × ℝ => Fin.snoc p.1 p.2) (ν n ⊗ₘ κ n))
        (hfiber : ∀ n, n < d → ∀ᵐ x ∂ν n, Measure.map (Q n x) η = κ n x) :
        ∀ n, n ≤ d → Measure.map (sample Q n) (Measure.pi fun _ : Fin n => η) = ν n := by
    …

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

22. theorem OAI.Problem358.TriangularRecursion.sample_mem_domains_upto line 564

    Source documentation

    Pointwise valid-prefix preservation also needs conditional data only below d.

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

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