Statistical Inference

This file records the first Lean interface for the decision-theoretic setup used in the tutorial chapter.

structure InferenceModelofMeasure (ι : Type u_1) (Ω S X Y : ι → Type) [(i : ι) → MeasurableSpace (Ω i)] [(i : ι) → MeasurableSpace (S i)] [(i : ι) → MeasurableSpace (X i)] [(i : ι) → MeasurableSpace (Y i)] : Type u_1

• domain (i : ι) : Set (MeasureTheory.Measure (Ω i))
• functional (i : ι) : ↑(self.domain i) → S i
• measurable_functional (i : ι) : Measurable (self.functional i)
• data (i : ι) : Ω i → X i
• measurable_data (i : ι) : Measurable (self.data i)
• decision_rule (i : ι) : ProbabilityTheory.Kernel (X i) (Y i)
• loss_function (i : ι) : Y i → S i → ENNReal
• measurable_loss_function (i : ι) : Measurable (Function.uncurry (self.loss_function i))

noncomputable def InferenceModelofMeasure.conditionalRisk {ι : Type u_1} {Ω S X Y : ι → Type} [(i : ι) → MeasurableSpace (Ω i)] [(i : ι) → MeasurableSpace (S i)] [(i : ι) → MeasurableSpace (X i)] [(i : ι) → MeasurableSpace (Y i)] (I : InferenceModelofMeasure ι Ω S X Y) {i : ι} {μ : MeasureTheory.Measure (Ω i)} (hμ : μ ∈ I.domain i) : ENNReal

Equations

• I.conditionalRisk hμ = ∫⁻ (ω : Ω i), ∫⁻ (y : Y i), I.loss_function i y (I.functional i ⟨μ, hμ⟩) ∂(I.decision_rule i) (I.data i ω) ∂μ

def InferenceModelofMeasure.IsConsistent {ι : Type u_1} {Ω S X Y : ι → Type} [(i : ι) → MeasurableSpace (Ω i)] [(i : ι) → MeasurableSpace (S i)] [(i : ι) → MeasurableSpace (X i)] [(i : ι) → MeasurableSpace (Y i)] (l : Filter ι) (I : InferenceModelofMeasure ι Ω S X Y) : Prop

Equations

• InferenceModelofMeasure.IsConsistent l I = ∀ (μ : (i : ι) → MeasureTheory.Measure (Ω i)) (hμ : ∀ (i : ι), μ i ∈ I.domain i), Filter.Tendsto (fun (i : ι) => I.conditionalRisk ⋯) l (nhds 0)

def InferenceModelofMeasure.IsUniformlyConsistent {ι : Type u_1} {Ω S X Y : ι → Type} [(i : ι) → MeasurableSpace (Ω i)] [(i : ι) → MeasurableSpace (S i)] [(i : ι) → MeasurableSpace (X i)] [(i : ι) → MeasurableSpace (Y i)] (l : Filter ι) (I : InferenceModelofMeasure ι Ω S X Y) : Prop

Equations

• One or more equations did not get rendered due to their size.

def InferenceModelofMeasure.HasRateOfConvergence {ι : Type u_1} {Ω S X Y : ι → Type} [(i : ι) → MeasurableSpace (Ω i)] [(i : ι) → MeasurableSpace (S i)] [(i : ι) → MeasurableSpace (X i)] [(i : ι) → MeasurableSpace (Y i)] (l : Filter ι) (I : InferenceModelofMeasure ι Ω S X Y) (r : ι → ENNReal) : Prop

Equations

• One or more equations did not get rendered due to their size.

def ProbabilityTheory.Kernel.of_measure (θ : Type u_1) {Ω : Type u_2} [MeasurableSpace θ] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) : Kernel θ Ω

Each measure induces a constant kernel.

Equations

• ProbabilityTheory.Kernel.of_measure θ μ = { toFun := fun (x : θ) => μ, measurable' := ⋯ }

@[implicit_reducible]

instance instMeasurableSpaceKernel_statlib (θ : Type u_1) (Ω : Type u_2) [MeasurableSpace θ] [MeasurableSpace Ω] : MeasurableSpace (ProbabilityTheory.Kernel θ Ω)

Equations

• instMeasurableSpaceKernel_statlib θ Ω = ⨆ (t : θ), MeasurableSpace.comap (fun (κ : ProbabilityTheory.Kernel θ Ω) => κ t) MeasureTheory.Measure.instMeasurableSpace

structure InferenceModelofKernel (ι : Type u_1) (θ Ω S X Y : ι → Type) [(i : ι) → MeasurableSpace (θ i)] [(i : ι) → MeasurableSpace (Ω i)] [(i : ι) → MeasurableSpace (S i)] [(i : ι) → MeasurableSpace (X i)] [(i : ι) → MeasurableSpace (Y i)] : Type u_1

• domain (i : ι) : Set (ProbabilityTheory.Kernel (θ i) (Ω i))
• functional (i : ι) : ↑(self.domain i) → S i
• measurable_functional (i : ι) : Measurable (self.functional i)
• data (i : ι) : Ω i → X i
• measurable_data (i : ι) : Measurable (self.data i)
• decision_rule (i : ι) : ProbabilityTheory.Kernel (X i) (Y i)
• loss_function (i : ι) : Y i → S i → ENNReal
• measurable_loss_function (i : ι) : Measurable (Function.uncurry (self.loss_function i))

def InferenceModelofKernel.of_InferenceModelofMeasure {ι : Type u_1} {θ Ω S X Y : ι → Type} [(i : ι) → MeasurableSpace (θ i)] [(i : ι) → MeasurableSpace (Ω i)] [(i : ι) → MeasurableSpace (S i)] [(i : ι) → MeasurableSpace (X i)] [(i : ι) → MeasurableSpace (Y i)] (I : InferenceModelofMeasure ι Ω S X Y) : InferenceModelofKernel ι θ Ω S X Y

Equations

• One or more equations did not get rendered due to their size.

noncomputable def InferenceModelofKernel.conditionalRisk {ι : Type u_1} {θ Ω S X Y : ι → Type} [(i : ι) → MeasurableSpace (θ i)] [(i : ι) → MeasurableSpace (Ω i)] [(i : ι) → MeasurableSpace (S i)] [(i : ι) → MeasurableSpace (X i)] [(i : ι) → MeasurableSpace (Y i)] (I : InferenceModelofKernel ι θ Ω S X Y) {i : ι} (t : θ i) {κ : ProbabilityTheory.Kernel (θ i) (Ω i)} (hκ : κ ∈ I.domain i) : ENNReal

Equations

• I.conditionalRisk t hκ = ∫⁻ (ω : Ω i), ∫⁻ (y : Y i), I.loss_function i y (I.functional i ⟨κ, hκ⟩) ∂(I.decision_rule i) (I.data i ω) ∂κ t

def InferenceModelofKernel.IsConsistent {ι : Type u_1} {θ Ω S X Y : ι → Type} [(i : ι) → MeasurableSpace (θ i)] [(i : ι) → MeasurableSpace (Ω i)] [(i : ι) → MeasurableSpace (S i)] [(i : ι) → MeasurableSpace (X i)] [(i : ι) → MeasurableSpace (Y i)] (l : Filter ι) (I : InferenceModelofKernel ι θ Ω S X Y) : Prop

Equations

• One or more equations did not get rendered due to their size.

def InferenceModelofKernel.IsUniformlyConsistent {ι : Type u_1} {θ Ω S X Y : ι → Type} [(i : ι) → MeasurableSpace (θ i)] [(i : ι) → MeasurableSpace (Ω i)] [(i : ι) → MeasurableSpace (S i)] [(i : ι) → MeasurableSpace (X i)] [(i : ι) → MeasurableSpace (Y i)] (l : Filter ι) (I : InferenceModelofKernel ι θ Ω S X Y) : Prop

Equations

• One or more equations did not get rendered due to their size.