Examples and distinctions
Constructed examples of this model; each answer includes the Lean statement.
Exact root statement
∀ {Space : Type} [inst : MeasurableSpace Space] (ell : ℕ) (measure : MeasureTheory.Measure Space)
[MeasureTheory.IsProbabilityMeasure measure] (modes : Fin (fullSkyModeCount ell) → Space → ℝ) (signal noise : NNReal),
(∀ (mode : Fin (fullSkyModeCount ell)), Measurable (modes mode)) →
GaussianModeLaw measure modes signal noise →
(GaussianModeLaw measure modes signal noise → GaussianSquaredModeMoments measure modes ↑(signal + noise)) →
∫ (realization : Space), powerEstimator modes noise realization ∂measure = ↑signal ∧
ProbabilityTheory.variance (powerEstimator modes noise) measure =
2 * (↑signal + ↑noise) ^ 2 / ↑(fullSkyModeCount ell) ∧
MeasureTheory.Measure.map (powerEstimator modes noise) measure =
gaussianEstimatorLaw (fullSkyModeCount ell) signal noise
Compare two arguments
Compare their definitions and hypotheses. Shared declarations may be instantiated differently; differences do not establish equivalence or implication.
No comparison argument selected.
Compare an earlier extraction
Compare the displayed specifications with an earlier JSON export. This compares text, not mathematical equivalence. Files stay in this browser.
No earlier extraction selected.
Notes and questions
Import merges local entries without overwriting them.
All declarations in the selected argument
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- structure
- structure
Definitions and domain choices
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
Checked statements: parameters, hypotheses, and interpretation
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Constructors, projections, and other meaning dependencies
- constructor
- constructor
External mathematical declarations
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary