diff --git a/Graphon.lean b/Graphon.lean index bee8d9e..36b00af 100644 --- a/Graphon.lean +++ b/Graphon.lean @@ -21,6 +21,8 @@ import Graphon.RelEqualityPattern import Graphon.RelKernelEvaluator import Graphon.RelKernelSampler import Graphon.KernelRandomization +import Graphon.ForMathlib.RelativeFactorCoupling +import Graphon.UniformFactorCoupling import Graphon.RelFixingAlgebra import Graphon.RelRankAlgebra import Graphon.RelLowerFactor @@ -199,6 +201,8 @@ in Lean 4 using Mathlib. * `Graphon.RelKernelEvaluator` — R4 evaluator layer (#107): `RelKernelFamily` (the label-free measurable representing kernels `f_{r,π}` on the finite pattern-local latent product), `RelCoord.localLatents` (the coordinate's window into the global latent source), the measurable `evalStructure`, and the **equivariance theorem** `evalStructure_relabel` (relabeling the evaluated structure = precomposing the source with the latent-index action) with the pattern↔image transport square `patternLatentIndexEquivCoord_map` — latent source measure, sampler pushforward, and representation theorem deliberately held for the next layers * `Graphon.RelKernelSampler` — R4 sampler layer (#107): the evaluator over an arbitrary carrier (`RelKernelFamily.eval`, definitionally `evalStructure` on `Vinfinite`) with the pullback transport `eval_comap`; the i.i.d. uniform `latentSource` over global subset-latent indices with relabeling invariance (via `LatentIndex.relabelEquiv`); and the **evaluated exchangeable law** `RelKernelFamily.evalLaw` with its **dissociation** `evalLaw_isDissociated` (disjoint vertex windows read disjoint nonempty subset-latent collections, so the i.i.d. source factorizes) — the forward half of the dissociated functional AHK representation; the converse representation theorem is the remaining content of #107 * `Graphon.KernelRandomization` — R4 converse piece 1 (#107): the small adapter from Mathlib's kernel representation theorem (`Kernel.exists_measurable_map_eq_unitInterval`, Kallenberg Lemma 4.22) to the project's uniform source — `Kernel.exists_measurable_map_eq_uniform01` (a Markov kernel into a standard Borel space is the pushforward of `uniform01` by a jointly measurable map, the `[0,1]`-subtype input adapted through `Set.projIcc`) and the single-measure corollary `Measure.exists_measurable_map_eq_uniform01` — the randomization ("noise outsourcing") input for the converse representation theorem +* `Graphon.ForMathlib.RelativeFactorCoupling` — **upstream candidate** (signature-free, Mathlib-only imports): the **relatively independent joining over a common factor**, `relativeFactorCoupling μ ν q r = (condDistrib id q μ ×ₖ condDistrib id r ν) ∘ₘ μ.map q`, for measurable `q : Ω → Z`, `r : Ξ → Z` with `ν.map r = μ.map q`. Both sides are disintegrated over `Z` and the fibres multiplied independently; the independent product `μ.prod ν` would not identify the factors, and an arbitrary coupling that did could still let each side see more of the other. The engine is `map_condDistrib_id`, **fibre concentration**: pushing `condDistrib id q μ` through `q` is the deterministic identity kernel, i.e. conditioning on `q` pins down `q`. From it: both marginals, the common-factor identity `q ∘ Prod.fst =ᵐ r ∘ Prod.snd` (proved from the two fibre-concentration statements, one per side — equality of the factor *marginals* says nothing about the joint), and `condIndepFun_fst_snd_relativeFactorCoupling`, conditional independence of the two coordinates given `comap (q ∘ Prod.fst)`. The conditioning is deliberately on that variable, defined on the coupling space, rather than on the disintegration variable `∘ₘ` integrates out: only the former is visible to consumers, who see the coupling and not its construction. No σ-algebra equality `σ(q ∘ fst) = σ(snd)` is claimed — the latent may carry strictly more than the factor, as `U` carries more than `1_{U < p}`; what conditional independence excludes is that the surplus says anything further about the first coordinate +* `Graphon.UniformFactorCoupling` — R4 converse piece 3 (#107): the uniform specialization of the joining above, `exists_relativeFactorCoupling_uniform01`. The only uniform-specific input is `Measure.exists_measurable_map_eq_uniform01` (#140), which supplies the coding map `f : ℝ → Z` matching the two factor laws; everything after is generic. It runs in the direction `Graphon.KernelRandomization` does not — that module manufactures a variable with a prescribed law *out of* a uniform, whereas here a uniform is manufactured *alongside* an already-given variable — and it is reusable at every rank, so it replaces a port of an external de Finetti package with the narrow transfer step the recursion actually needs * `Graphon.RelFixingAlgebra` — R4 converse piece 2a (#107): the **law-independent** factor-algebra layer — `SortwiseFixing` (the `A`-fixing stabilizer of finitely supported sortwise permutations, closed under `1`/`*`/`⁻¹`/conjugation), the raw `RelStructure.fixingAlgebra` (events invariant under the `A`-fixing group; deliberately *not* "generated by relations inside `A`", which loses hidden vertex information), monotonicity, `fixingAlgebra_empty = invariantAlgebra` (near-definitional), and the **transport equality** `fixingAlgebra_comap_relabel : comap (relabel σ) (fixingAlgebra A) = fixingAlgebra (image σ A)` via stabilizer conjugation — no completions, no law; the conditional-independence theorem is its own later PR * `Graphon.RelPollingInfrastructure` — R4 (#107): the reusable polling engine, extracted from `RelFixingCondIndep` once the rankwise relative-independence argument became its second consumer. Three public declarations: the tail engine `condExp_ae_eq_condExp_of_comap_eq` (a measure-preserving `T` fixing `f` a.e. and pulling `m₁` back to `m₂ ≤ m₁` forces `μ[f|m₁] =ᵐ μ[f|m₂]`), `InfiniteRelExchangeableLaw.measurePreserving_relabel`, and `InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra`. The `L²` squeeze and the conditional-expectation transport along `comap` stay private — they are the proof of the tail engine, not its interface * `Graphon.RelFixingCondIndep` — R4 converse piece 2b (#107): the headline `InfiniteRelExchangeableLaw.condIndep_fixingAlgebra` — for **every** exchangeable law, with no dissociation hypothesis, `CondIndep (fixingAlgebra (A ∩ B)) (fixingAlgebra A) (fixingAlgebra B) (fixingAlgebra_le _) M.law` (Austin arXiv:0801.1698 Lemma 3.11 / Proposition 3.12; Kallenberg Lemma 7.6 as the closest precursor — Lemmas 7.18–7.19 there belong to the later realization recursion). The private machinery: the `L²`-energy squeeze, measure-preserving-map transport of conditional expectation, and the tail-property engine (a.e.-fixing + comap-pullback ⟹ equal conditional expectations); the upgrade of `fixingAlgebra A`-invariance from finitely supported to *arbitrary* sortwise permutations fixing `A`, modulo the law; the poll geometry (deep copies of `B \ A` laid out along a two-sided `ℤ`-orbit — a unilateral block shift is not a bijection — moved by a single residue-wise permutation fixing `A`); the tail **joins** `⨆_{m ≥ n} fixingAlgebra ((A ∩ B) ∪ Q m)`, whose intersection is `fixingAlgebra (A ∩ B)` as a *raw* σ-algebra equality; and the reduction `E[f | fixingAlgebra B] =ᵐ E[f | fixingAlgebra (A ∩ B)]` that the theorem factorizes through. Everything but the headline is `private` diff --git a/Graphon/ForMathlib/RelativeFactorCoupling.lean b/Graphon/ForMathlib/RelativeFactorCoupling.lean new file mode 100644 index 0000000..699145a --- /dev/null +++ b/Graphon/ForMathlib/RelativeFactorCoupling.lean @@ -0,0 +1,211 @@ +/- +Copyright (c) 2026 Cameron Freer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Cameron Freer +-/ +import Mathlib.Probability.Independence.Conditional + +/-! +# Relatively independent joinings over a common factor + +Given two probability spaces carrying a *common factor* — measurable maps `q : Ω → Z` and +`r : Ξ → Z` with the same pushforward — this file builds the canonical coupling of `μ` and `ν` +that identifies the two factors and adds nothing else: + +`relativeFactorCoupling μ ν q r = (condDistrib id q μ ×ₖ condDistrib id r ν) ∘ₘ μ.map q` + +Both sides are disintegrated over `Z` and the fibres are then multiplied independently. Nothing +else would do: the independent product `μ.prod ν` does not satisfy `q X = r Ξ`, and an arbitrary +coupling with that identity could still let each side see more of the other than the common +factor does. + +## Main results + +* `map_condDistrib_id` — **fibre concentration**: the conditional law of a point given its factor + value, pushed forward through the factor, is the deterministic identity kernel. This is the + whole content of "conditioning on `q` pins down `q`", and everything below rests on it. +* `map_fst_relativeFactorCoupling`, `map_snd_relativeFactorCoupling` — the two marginals are `μ` + and `ν` (the second under the standing hypothesis `ν.map r = μ.map q`). +* `comp_fst_ae_eq_comp_snd_relativeFactorCoupling` — the **common-factor identity** + `q ∘ Prod.fst =ᵐ r ∘ Prod.snd`. +* `condIndepFun_fst_snd_relativeFactorCoupling` — the two coordinates are conditionally + independent **given the common factor read off the first coordinate**. + +## Why condition on `q ∘ Prod.fst` + +The conditioning σ-algebra is `MeasurableSpace.comap (q ∘ Prod.fst) inferInstance`, generated by a +genuine random variable on the coupling space, not by an auxiliary `Z`-valued variable that the +composition `∘ₘ` has integrated out. Only the former is available to downstream consumers, who see +the coupling and not its construction. The common-factor identity above transfers the statement to +`r ∘ Prod.snd` whenever that is the more convenient side. + +Note that the coupling gives only `σ(q ∘ fst) ⊆ σ(snd)` modulo the law: the second coordinate may +carry strictly more information than the shared factor, exactly as a uniform `U` carries more than +`1_{U < p}`. What the conditional independence excludes is that the surplus says anything about +the first coordinate beyond what the factor already determines. +-/ + +open MeasureTheory ProbabilityTheory + +namespace ProbabilityTheory + +variable {Ω Ξ Z : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] + [MeasurableSpace Ξ] [StandardBorelSpace Ξ] [Nonempty Ξ] + [MeasurableSpace Z] [StandardBorelSpace Z] [Nonempty Z] + +/-! ### Fibre concentration -/ + +/-- **Fibre concentration.** The conditional law of a point given the value of a factor map is +carried by the fibre over that value: pushing `condDistrib id q μ` forward through `q` returns +the deterministic identity kernel, almost everywhere for the law of the factor. -/ +theorem map_condDistrib_id (μ : Measure Ω) [IsFiniteMeasure μ] {q : Ω → Z} (hq : Measurable q) : + (condDistrib id q μ).map q =ᵐ[μ.map q] Kernel.id := by + have h₁ : condDistrib (q ∘ (id : Ω → Ω)) q μ =ᵐ[μ.map q] (condDistrib id q μ).map q := + condDistrib_comp q aemeasurable_id hq + have h₂ : condDistrib q q μ =ᵐ[μ.map q] Kernel.id := condDistrib_self q + have h₃ : condDistrib q q μ =ᵐ[μ.map q] (condDistrib id q μ).map q := by simpa using h₁ + exact h₃.symm.trans h₂ + +/-- The fibre over `z` carries all of the conditional law given `z`. -/ +theorem condDistrib_id_apply_fibre (μ : Measure Ω) [IsFiniteMeasure μ] {q : Ω → Z} + (hq : Measurable q) : + ∀ᵐ z ∂(μ.map q), (condDistrib id q μ) z (q ⁻¹' {z}) = 1 := by + filter_upwards [map_condDistrib_id μ hq] with z hz + rw [← Measure.map_apply hq (measurableSet_singleton z), ← Kernel.map_apply _ hq, hz, + Kernel.id_apply] + simp + +/-- Pointwise form of fibre concentration: conditionally on the factor value `z`, the factor is +almost surely equal to `z`. -/ +theorem ae_ae_eq_condDistrib_id (μ : Measure Ω) [IsFiniteMeasure μ] {q : Ω → Z} + (hq : Measurable q) : + ∀ᵐ z ∂(μ.map q), ∀ᵐ x ∂(condDistrib id q μ) z, q x = z := by + filter_upwards [condDistrib_id_apply_fibre μ hq] with z hz + rw [ae_iff, show {x | ¬ q x = z} = (q ⁻¹' {z})ᶜ from by ext x; simp] + exact (prob_compl_eq_zero_iff (hq (measurableSet_singleton z))).mpr hz + +/-! ### The coupling -/ + +/-- **The relatively independent joining of `μ` and `ν` over their common `Z`-factor.** Both sides +are disintegrated over `Z` — `μ` along `q`, `ν` along `r` — and the fibres are then multiplied +independently. -/ +noncomputable def relativeFactorCoupling (μ : Measure Ω) (ν : Measure Ξ) [IsFiniteMeasure μ] + [IsFiniteMeasure ν] (q : Ω → Z) (r : Ξ → Z) : Measure (Ω × Ξ) := + ((condDistrib id q μ) ×ₖ (condDistrib id r ν)) ∘ₘ (μ.map q) + +instance instIsFiniteMeasureRelativeFactorCoupling (μ : Measure Ω) (ν : Measure Ξ) + [IsFiniteMeasure μ] [IsFiniteMeasure ν] (q : Ω → Z) (r : Ξ → Z) : + IsFiniteMeasure (relativeFactorCoupling μ ν q r) := by + haveI : IsFiniteMeasure (μ.map q) := Measure.isFiniteMeasure_map μ q + rw [relativeFactorCoupling] + infer_instance + +variable {μ : Measure Ω} {ν : Measure Ξ} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] + {q : Ω → Z} {r : Ξ → Z} + +omit [StandardBorelSpace Z] [Nonempty Z] in +/-- The coupling is a probability measure. Measurability of `q` is genuinely needed: without it +`μ.map q` is the zero measure. -/ +theorem isProbabilityMeasure_relativeFactorCoupling (hq : Measurable q) : + IsProbabilityMeasure (relativeFactorCoupling μ ν q r) := by + haveI : IsProbabilityMeasure (μ.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable + rw [relativeFactorCoupling] + infer_instance + +omit [StandardBorelSpace Z] [Nonempty Z] in +/-- The first marginal is `μ`. -/ +theorem map_fst_relativeFactorCoupling (hq : Measurable q) : + (relativeFactorCoupling μ ν q r).map Prod.fst = μ := by + rw [relativeFactorCoupling, Measure.map_comp _ _ measurable_fst, ← Kernel.fst_eq, Kernel.fst_prod] + simpa using condDistrib_comp_map (X := q) hq.aemeasurable (aemeasurable_id (μ := μ)) + +omit [StandardBorelSpace Z] [Nonempty Z] in +/-- The second marginal is `ν`, under the standing hypothesis that the two factors have the same +law. -/ +theorem map_snd_relativeFactorCoupling (hr : Measurable r) (hqr : ν.map r = μ.map q) : + (relativeFactorCoupling μ ν q r).map Prod.snd = ν := by + rw [relativeFactorCoupling, Measure.map_comp _ _ measurable_snd, ← Kernel.snd_eq, + Kernel.snd_prod, ← hqr] + simpa using condDistrib_comp_map (μ := ν) (X := r) hr.aemeasurable (aemeasurable_id (μ := ν)) + +/-- **The common-factor identity**: the two coordinates agree on the shared factor. Proved from +the two fibre-concentration statements, one on each side of the joining — equality of the two +factor *marginals* would not suffice, since it says nothing about the joint law. -/ +theorem comp_fst_ae_eq_comp_snd_relativeFactorCoupling (hq : Measurable q) (hr : Measurable r) + (hqr : ν.map r = μ.map q) : + q ∘ Prod.fst =ᵐ[relativeFactorCoupling μ ν q r] r ∘ Prod.snd := by + haveI : IsProbabilityMeasure (μ.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable + have hmeas : MeasurableSet {p : Ω × Ξ | (q ∘ Prod.fst) p = (r ∘ Prod.snd) p} := + measurableSet_eq_fun (hq.comp measurable_fst) (hr.comp measurable_snd) + have hν : ∀ᵐ z ∂(μ.map q), ∀ᵐ y ∂(condDistrib id r ν) z, r y = z := by + rw [← hqr]; exact ae_ae_eq_condDistrib_id ν hr + rw [Filter.EventuallyEq, relativeFactorCoupling, Measure.ae_comp_iff hmeas] + filter_upwards [ae_ae_eq_condDistrib_id μ hq, hν] with z hz hz' + rw [Kernel.prod_apply] + have h1 : ∀ᵐ p ∂(((condDistrib id q μ) z).prod ((condDistrib id r ν) z)), q p.1 = z := + Measure.quasiMeasurePreserving_fst.ae hz + have h2 : ∀ᵐ p ∂(((condDistrib id q μ) z).prod ((condDistrib id r ν) z)), r p.2 = z := + Measure.quasiMeasurePreserving_snd.ae hz' + filter_upwards [h1, h2] with p hp1 hp2 + simp only [Function.comp_apply, hp1, hp2] + +/-- The joint law of the common factor and the two coordinates: the factor is a.s. the +disintegration variable, so reading it off the first coordinate reconstitutes the outer +integration. This is the structural identity behind the conditional independence below. -/ +theorem map_factorProd_relativeFactorCoupling (hq : Measurable q) : + (relativeFactorCoupling μ ν q r).map (fun p => (q p.1, p.1, p.2)) + = (Kernel.id ×ₖ ((condDistrib id q μ) ×ₖ (condDistrib id r ν))) ∘ₘ (μ.map q) := by + haveI : IsProbabilityMeasure (μ.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable + have hw : Measurable (fun p : Ω × Ξ => (q p.1, p.1, p.2)) := + (hq.comp measurable_fst).prodMk measurable_id + rw [relativeFactorCoupling, Measure.map_comp _ _ hw] + refine Measure.comp_congr ?_ + filter_upwards [ae_ae_eq_condDistrib_id μ hq] with z hz + rw [Kernel.map_apply _ hw, Kernel.prod_apply, Kernel.prod_apply, Kernel.id_apply, + Measure.dirac_prod, Kernel.prod_apply] + refine Measure.map_congr ?_ + have h1 : ∀ᵐ p ∂(((condDistrib id q μ) z).prod ((condDistrib id r ν) z)), q p.1 = z := + Measure.quasiMeasurePreserving_fst.ae hz + filter_upwards [h1] with p hp + simp [hp] + +/-- **The two coordinates are conditionally independent given the common factor.** The +conditioning σ-algebra is the one generated by `q ∘ Prod.fst`, a random variable on the coupling +space itself rather than the integrated-out disintegration variable. -/ +theorem condIndepFun_fst_snd_relativeFactorCoupling (hq : Measurable q) (hr : Measurable r) + (hqr : ν.map r = μ.map q) : + CondIndepFun (MeasurableSpace.comap (q ∘ Prod.fst) inferInstance) + (hq.comp measurable_fst).comap_le Prod.fst Prod.snd (relativeFactorCoupling μ ν q r) := by + haveI : IsProbabilityMeasure (μ.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable + set P := relativeFactorCoupling μ ν q r with hP + -- the law of the common factor on the coupling space + have hmapk : P.map (q ∘ Prod.fst) = μ.map q := by + rw [hP, ← Measure.map_map hq measurable_fst, map_fst_relativeFactorCoupling hq] + -- the two conditional distributions are the two disintegration kernels + have hcd1 : condDistrib Prod.fst (q ∘ Prod.fst) P =ᵐ[μ.map q] condDistrib id q μ := by + rw [← hmapk, condDistrib_ae_eq_iff_measure_eq_compProd _ measurable_fst.aemeasurable, hmapk, + compProd_map_condDistrib (aemeasurable_id (μ := μ))] + rw [show (fun p : Ω × Ξ => ((q ∘ Prod.fst) p, p.1)) = (fun x : Ω => (q x, id x)) ∘ Prod.fst from + rfl, ← Measure.map_map (by fun_prop) measurable_fst, hP, + map_fst_relativeFactorCoupling hq] + have hcd2 : condDistrib Prod.snd (q ∘ Prod.fst) P =ᵐ[μ.map q] condDistrib id r ν := by + rw [← hmapk, condDistrib_ae_eq_iff_measure_eq_compProd _ measurable_snd.aemeasurable, hmapk, + ← hqr, compProd_map_condDistrib (aemeasurable_id (μ := ν))] + have hswap : P.map (fun p : Ω × Ξ => ((q ∘ Prod.fst) p, p.2)) + = P.map (fun p : Ω × Ξ => (r p.2, id p.2)) := by + refine Measure.map_congr ?_ + filter_upwards [comp_fst_ae_eq_comp_snd_relativeFactorCoupling hq hr hqr] with p hp + rw [show ((q ∘ Prod.fst) p, p.2) = ((r ∘ Prod.snd) p, p.2) from by rw [hp]] + rfl + rw [hswap, show (fun p : Ω × Ξ => (r p.2, id p.2)) = (fun y : Ξ => (r y, id y)) ∘ Prod.snd from + rfl, ← Measure.map_map (by fun_prop) measurable_snd, hP, + map_snd_relativeFactorCoupling hr hqr] + rw [condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib measurable_fst measurable_snd + (hq.comp measurable_fst), hmapk] + simp only [Function.comp_apply] + rw [map_factorProd_relativeFactorCoupling hq] + refine (Measure.comp_congr ?_).symm + filter_upwards [hcd1, hcd2] with z h1 h2 + rw [Kernel.prod_apply, Kernel.prod_apply, Kernel.prod_apply, Kernel.prod_apply, h1, h2] + +end ProbabilityTheory diff --git a/Graphon/UniformFactorCoupling.lean b/Graphon/UniformFactorCoupling.lean new file mode 100644 index 0000000..271ca9c --- /dev/null +++ b/Graphon/UniformFactorCoupling.lean @@ -0,0 +1,66 @@ +/- +Copyright (c) 2026 Cameron Freer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Cameron Freer +-/ +import Graphon.ForMathlib.RelativeFactorCoupling +import Graphon.KernelRandomization + +/-! +# Coupling a factor to a uniform latent (R4 converse piece 3, #107) + +The specialization of `ProbabilityTheory.relativeFactorCoupling` in which the second space is the +project's uniform source: given a factor map `q : Ω → Z` of a probability measure `μ`, there is a +coupling of `μ` with `uniform01` on `Ω × ℝ` whose second coordinate is uniform, whose first has +law `μ`, in which the latent *resolves* the factor, and in which the latent tells nothing further +about `Ω`. + +This is the narrow randomization step the rankwise recursion needs, and it runs in the direction +that `Graphon.KernelRandomization` does not: that module manufactures a variable with a prescribed +law *out of* a uniform, whereas here a uniform must be manufactured *alongside* an already-given +variable. The only uniform-specific input is `Measure.exists_measurable_map_eq_uniform01` (#140), +which supplies the coding map `f : ℝ → Z` matching the two factor laws; everything after that is +the generic relative joining. + +## Contents + +* `ProbabilityTheory.exists_relativeFactorCoupling_uniform01` — the wrapper: a measurable coding + map together with all five properties of the resulting coupling. +-/ + +open MeasureTheory ProbabilityTheory + +namespace ProbabilityTheory + +variable {Ω Z : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] + [MeasurableSpace Z] [StandardBorelSpace Z] [Nonempty Z] + +/-- **Every factor of a probability measure can be coupled to a uniform latent.** The coding map +`f` comes from the randomization adapter; the coupling is the relatively independent joining of +`μ` and `uniform01` over the common `Z`-factor, and it satisfies, in order: it is a probability +measure; its first marginal is `μ`; its second marginal is `uniform01`; the latent resolves the +factor, `q X = f ξ` a.s.; and the two coordinates are conditionally independent given the factor +read off the first coordinate. + +The conditioning σ-algebra is generated by `q ∘ Prod.fst`, a variable on the coupling space +itself, rather than by the disintegration variable the construction integrates out. Conditional +independence of the latent from any coarser function of the first coordinate follows by +measurable composition. -/ +theorem exists_relativeFactorCoupling_uniform01 (μ : Measure Ω) [IsProbabilityMeasure μ] + {q : Ω → Z} (hq : Measurable q) : + ∃ f : ℝ → Z, Measurable f ∧ + IsProbabilityMeasure (relativeFactorCoupling μ uniform01 q f) ∧ + (relativeFactorCoupling μ uniform01 q f).map Prod.fst = μ ∧ + (relativeFactorCoupling μ uniform01 q f).map Prod.snd = uniform01 ∧ + q ∘ Prod.fst =ᵐ[relativeFactorCoupling μ uniform01 q f] f ∘ Prod.snd ∧ + CondIndepFun (MeasurableSpace.comap (q ∘ Prod.fst) inferInstance) + (hq.comp measurable_fst).comap_le Prod.fst Prod.snd + (relativeFactorCoupling μ uniform01 q f) := by + haveI : IsProbabilityMeasure (μ.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable + obtain ⟨f, hf, hfq⟩ := (μ.map q).exists_measurable_map_eq_uniform01 + exact ⟨f, hf, isProbabilityMeasure_relativeFactorCoupling hq, + map_fst_relativeFactorCoupling hq, map_snd_relativeFactorCoupling hf hfq, + comp_fst_ae_eq_comp_snd_relativeFactorCoupling hq hf hfq, + condIndepFun_fst_snd_relativeFactorCoupling hq hf hfq⟩ + +end ProbabilityTheory diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean index 0f56ad0..2709d82 100644 --- a/scripts/axiom_audit.lean +++ b/scripts/axiom_audit.lean @@ -232,3 +232,17 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py` #print axioms RelSignature.CoherentBasis.lowerFactorProjection_lowerFactorSpaceEquiv #print axioms RelSignature.CoherentBasis.measurable_exactMap_fixingAlgebra #print axioms RelSignature.CoherentBasis.iCondIndepFun_exactMap_singleton + +-- R4 converse piece 3 (#107): relatively independent joinings over a common factor +-- (`Graphon/ForMathlib/RelativeFactorCoupling.lean`, upstream candidate) and the uniform +-- specialization (`Graphon/UniformFactorCoupling.lean`). +#print axioms ProbabilityTheory.map_condDistrib_id +#print axioms ProbabilityTheory.condDistrib_id_apply_fibre +#print axioms ProbabilityTheory.ae_ae_eq_condDistrib_id +#print axioms ProbabilityTheory.isProbabilityMeasure_relativeFactorCoupling +#print axioms ProbabilityTheory.map_fst_relativeFactorCoupling +#print axioms ProbabilityTheory.map_snd_relativeFactorCoupling +#print axioms ProbabilityTheory.comp_fst_ae_eq_comp_snd_relativeFactorCoupling +#print axioms ProbabilityTheory.map_factorProd_relativeFactorCoupling +#print axioms ProbabilityTheory.condIndepFun_fst_snd_relativeFactorCoupling +#print axioms ProbabilityTheory.exists_relativeFactorCoupling_uniform01 diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py index efeaccb..a89a840 100644 --- a/scripts/check_census_and_axioms.py +++ b/scripts/check_census_and_axioms.py @@ -215,6 +215,16 @@ "RelSignature.CoherentBasis.lowerFactorProjection_lowerFactorSpaceEquiv", "RelSignature.CoherentBasis.measurable_exactMap_fixingAlgebra", "RelSignature.CoherentBasis.iCondIndepFun_exactMap_singleton", + "ProbabilityTheory.map_condDistrib_id", + "ProbabilityTheory.condDistrib_id_apply_fibre", + "ProbabilityTheory.ae_ae_eq_condDistrib_id", + "ProbabilityTheory.isProbabilityMeasure_relativeFactorCoupling", + "ProbabilityTheory.map_fst_relativeFactorCoupling", + "ProbabilityTheory.map_snd_relativeFactorCoupling", + "ProbabilityTheory.comp_fst_ae_eq_comp_snd_relativeFactorCoupling", + "ProbabilityTheory.map_factorProd_relativeFactorCoupling", + "ProbabilityTheory.condIndepFun_fst_snd_relativeFactorCoupling", + "ProbabilityTheory.exists_relativeFactorCoupling_uniform01", "RelSignature.condExp_ae_eq_condExp_of_comap_eq", "RelSignature.InfiniteRelExchangeableLaw.measurePreserving_relabel", "RelSignature.InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra",