Theorems · Theorem · probability
ProbabilityTheory.gaussianReal_add_gaussianReal_of_indepFun
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {m₁ m₂ : ℝ} {v₁ v₂ : NNReal} {X Y : Ω → ℝ},
ProbabilityTheory.IndepFun X Y P →
MeasureTheory.Measure.map X P = ProbabilityTheory.gaussianReal m₁ v₁ →
MeasureTheory.Measure.map Y P = ProbabilityTheory.gaussianReal m₂ v₂ →
MeasureTheory.Measure.map (X + Y) P = ProbabilityTheory.gaussianReal (m₁ + m₂) (v₁ + v₂)- Cited by
- 0 results in Mathlib
- Foundations
- Depth 296 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- NNRealstatement and proof · cited by 4,310
- MeasureTheory.Measure.mapstatement and proof · cited by 858
- AEMeasurableproof · cited by 840
- MeasureTheory.SigmaFiniteproof · cited by 526
- ProbabilityTheory.IndepFunstatement and proof · cited by 192
- ProbabilityTheory.gaussianRealstatement and proof · cited by 77
- MeasureTheory.Measure.convproof · cited by 41
- ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀'proof · cited by 6
- AEMeasurable.of_map_ne_zeroproof · cited by 5
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.