Theorems · Theorem · probability

ProbabilityTheory.uncenteredCovarianceBilinDual.congr_simp

∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} [inst_1 : NormedSpace ℝ E]
  [inst_2 : OpensMeasurableSpace E] (μ μ_1 : MeasureTheory.Measure E),
  μ = μ_1 → ProbabilityTheory.uncenteredCovarianceBilinDual μ = ProbabilityTheory.uncenteredCovarianceBilinDual μ_1

Defined in: Mathlib.Probability.Moments.CovarianceBilinDual
Cited by: 0 results in Mathlib
Foundations: Depth 269 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup NormedSpace OpensMeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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
NormedSpacestatement and proof · cited by 12,499
MeasureTheory.Measurestatement and proof · cited by 10,939
ContinuousLinearMapstatement · cited by 5,352
OpensMeasurableSpacestatement and proof · cited by 636
StrongDualstatement · cited by 459
ProbabilityTheory.uncenteredCovarianceBilinDualstatement and proof · cited by 10

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.