Theorems · Theorem · probability
ProbabilityTheory.IdentDistrib.aemeasurable_fst
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
[inst_2 : MeasurableSpace γ] {f : α → γ} {g : β → γ}
{μ : autoParam (MeasureTheory.Measure α) ProbabilityTheory.IdentDistrib._auto_1}
{ν : autoParam (MeasureTheory.Measure β) ProbabilityTheory.IdentDistrib._auto_3},
ProbabilityTheory.IdentDistrib f g μ ν → AEMeasurable f μ- Defined in
- Mathlib.Probability.IdentDistrib
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- AEMeasurablestatement · cited by 840
- ProbabilityTheory.IdentDistribstatement and proof · cited by 74
Cited by18
Results whose statement or proof uses this declaration.
- ProbabilityTheory.IdentDistrib.symmproof · cited by 8
- ProbabilityTheory.IdentDistrib.ae_sndproof · cited by 4
- ProbabilityTheory.IdentDistrib.integral_eqproof · cited by 4
- ProbabilityTheory.IdentDistrib.measure_mem_eqproof · cited by 3
- ProbabilityTheory.IdentDistrib.transproof · cited by 2
- ProbabilityTheory.IdentDistrib.lintegral_eqproof · cited by 2
- ProbabilityTheory.charFun_inv_sqrt_mul_sumproof · cited by 1
- ProbabilityTheory.IdentDistrib.aestronglyMeasurable_fstproof · cited by 1
- ProbabilityTheory.IdentDistrib.comp_of_aemeasurableproof · cited by 1
- ProbabilityTheory.MemLp.uniformIntegrable_of_identDistrib_auxproof · cited by 1
- ProbabilityTheory.mgf_congr_identDistribproof · cited by 0
- ProbabilityTheory.indepFun_of_identDistrib_pairproof · cited by 0