Theorems · Theorem · probability

ProbabilityTheory.covarianceBilin.congr_simp

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] (μ μ_1 : MeasureTheory.Measure E),
  μ = μ_1 → ProbabilityTheory.covarianceBilin μ = ProbabilityTheory.covarianceBilin μ_1

Defined in: Mathlib.Probability.Moments.CovarianceBilin
Cited by: 1 results in Mathlib
Foundations: Depth 271 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup InnerProductSpace MeasurableSpace BorelSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

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
RingHom.idstatement · cited by 18,349
NormedAddCommGroupstatement and proof · cited by 15,752
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ContinuousLinearMapstatement · cited by 5,352
InnerProductSpacestatement and proof · cited by 3,523
BorelSpacestatement and proof · cited by 1,602
ProbabilityTheory.covarianceBilinstatement and proof · cited by 25

Cited by1

Results whose statement or proof uses this declaration.

ProbabilityTheory.IsGaussian.ext_iffproof · cited by 0