Estimation.Efficiency.AsymptoticLanConvolution
Local asymptotic normality and scalar convolution theory for semiparametric efficiency: local experiments, i.i.d. quadratic-mean differentiability, regular estimator limits, and the canonical-gradient variance lower bound.
Basic 8 core · 0 supporting 4 to review This module gives a paper-independent interface for triangular local experiments. ★ canonicalGradientPairing_of_mem_range
Local experiments and local asymptotic normality
This module gives a paper-independent interface for triangular local experiments. A local experiment consists of a base law and one local-alternative law for each finite-dimensional direction. Its log likelihood ratio is the logarithm of the Radon--Nikodym derivative of the absolutely continuous part of the local law with respect to the base law.
Weak convergence is formulated by bounded continuous test functions so that the sample space
may vary with the row. IsLAN records the Gaussian central-sequence limit and the quadratic
log-likelihood expansion. No survival-analysis or paper-run objects occur in this layer.
def WeaklyConverges unreviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
A row-indexed random element converges weakly to Q when its expectation against every bounded continuous real test function converges to the corresponding expectation under Q.
def TendstoInProbability unreviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
A real triangular array converges in probability to c when, for every positive tolerance, the probability of an absolute error at least that tolerance tends to zero.
Definition (Lean source)
parameters
def
TendstoInProbability P X c :
Prop
structure LocalExperiment unreviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
A sequence of local statistical experiments with finite-dimensional direction space H. For row n, baseLaw n is the law at the base point and localLaw n h is the law at the fixed local direction h (normally the original parameter is displaced by h / sqrt n).
Definition (Lean source)
parameters
Ω :
ℕ → Type*
∀ n, MeasurableSpace (Ω n)
H :
Type*
Zero H
fields
Probability law at the base point in each row.
baseLaw :
(n : ℕ) → Measure (Ω n)
Probability law at local direction `h` in each row.
localLaw :
(n : ℕ) → H → Measure (Ω n)
Every base law has total mass one.
base_probability :
∀ n, IsProbabilityMeasure (baseLaw n)
Every local-alternative law has total mass one.
local_probability :
∀ n h, IsProbabilityMeasure (localLaw n h)
Local direction zero is the base law in every row.
local_zero :
∀ n, localLaw n 0 = baseLaw n
def logLikelihoodRatio reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution.LocalExperiment
The generalized log likelihood ratio of local direction h against the base law is the logarithm of the real Radon--Nikodym derivative of the local law's absolutely continuous part. Where that derivative is zero, the extended-real value -∞ is represented by the diverging finite truncation -n; DQM makes this exceptional event asymptotically negligible.
Definition (Lean source)
parameters
def
logLikelihoodRatio E n h ω :
ℝ
structure IsLAN reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
A local experiment is locally asymptotically normal with central sequence centralSequence and information form information when the central sequence has the centered Gaussian characteristic function determined by information, and every fixed-direction log likelihood ratio equals the linear score term minus half the information quadratic form up to a remainder converging to zero in base-law probability.
Definition (Lean source)
parameters
Ω :
ℕ → Type u_1
H :
Type u_2
E :
LocalExperiment Ω H
centralSequence :
(n : ℕ) → Ω n → H
information :
BilinForm ℝ H
gaussianLimit :
Measure H
assumes
central_measurable :
∀ n, AEMeasurable (centralSequence n) (E.baseLaw n)
The central sequence is measurable in every row.
information_symmetric :
information.IsSymm
The information form is symmetric.
information_nonnegative :
∀ h, 0 ≤ information h h
The information quadratic form is nonnegative.
gaussian_charFun :
The Gaussian limit has characteristic function exp (-information(t,t)/2).
central_converges :
WeaklyConverges E.baseLaw centralSequence gaussianLimit
The central sequence converges weakly to the specified Gaussian law.
expansion :
∀ h : H,
TendstoInProbability E.baseLaw (fun n ω => E.logLikelihoodRatio n h ω - inner ℝ h (centralSequence n ω) + (1 / 2 : ℝ) * information h h) 0
The LAN quadratic expansion holds in base-law probability for every fixed direction.
structure IsRegularEstimator reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
A scalar estimator has regular limit limitLaw with derivative targetDerivative when, under every fixed local direction h, its base-centered statistic minus the deterministic local target shift converges weakly to the same law.
Definition (Lean source)
parameters
Ω :
ℕ → Type u_1
H :
Type u_2
E :
LocalExperiment Ω H
statistic :
(n : ℕ) → Ω n → ℝ
targetDerivative :
H →ₗ[ℝ] ℝ
limitLaw :
Measure ℝ
assumes
measurable :
∀ n h, AEMeasurable (statistic n) (E.localLaw n h)
The statistic is a.e. measurable under every local law.
regular :
∀ h : H,
WeaklyConverges (fun n => E.localLaw n h) (fun n ω => statistic n ω - targetDerivative h) limitLaw
Centering by the local derivative gives the same weak limit in every fixed direction.
structure CanonicalGradientPairing unreviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
A canonical-gradient pairing for a finite-dimensional LAN experiment. The map scoreMap embeds parameter directions into an ambient L²-type Hilbert space K; gradient belongs to the score range, the information is the score inner product, and target derivatives are inner products with the gradient. Consequently its efficient variance is ‖gradient‖².
Definition (Lean source)
parameters
assumes
gradient_mem_range :
gradient ∈ range scoreMap
The canonical gradient belongs to the finite-dimensional score range.
information_eq_inner :
∀ h g, information h g = inner ℝ (scoreMap h) (scoreMap g)
Fisher information is the inner product of embedded scores.
derivative_eq_inner :
∀ h, targetDerivative h = inner ℝ gradient (scoreMap h)
The pathwise derivative is pairing with the canonical gradient.
theorem canonicalGradientPairing_of_mem_range reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
Given an information form, a target derivative, a score embedding, and a candidate gradient, proof that the gradient is in the score range, that information is the score inner product, and that the derivative pairs with the gradient yield a canonical-gradient pairing.
Formal statement
hypotheses
H :
Type u_2
K :
information :
BilinForm ℝ H
targetDerivative :
H →ₗ[ℝ] ℝ
scoreMap :
H →ₗ[ℝ] K
gradient :
K
hgradient :
gradient ∈ range scoreMap
hinfo :
∀ h g, information h g = inner ℝ (scoreMap h) (scoreMap g)
hderiv :
∀ h, targetDerivative h = inner ℝ gradient (scoreMap h)
conclusion
CanonicalGradientPairing information targetDerivative scoreMap gradient
Proof (Lean source)
theorem canonicalGradientPairing_of_mem_range
{K : Type*} [NormedAddCommGroup K] [InnerProductSpace ℝ K]
(information : BilinForm ℝ H) (targetDerivative : H →ₗ[ℝ] ℝ)
(scoreMap : H →ₗ[ℝ] K) (gradient : K)
(hgradient : gradient ∈ range scoreMap)
(hinfo : ∀ h g, information h g = inner ℝ (scoreMap h) (scoreMap g))
(hderiv : ∀ h, targetDerivative h = inner ℝ gradient (scoreMap h)) :
CanonicalGradientPairing information targetDerivative scoreMap gradient :=
{ gradient_mem_range := hgradient
information_eq_inner := hinfo
derivative_eq_inner := hderiv }
ConvolutionCore 5 core · 5 supporting This module supplies the compactness, likelihood-normalization, and Gaussian-limit ingredients used in the scalar Hájek--Le Cam convolution argument. ★ lan_logLikelihoodRatio_weaklyConverges
Joint weak limits for LAN experiments
This module supplies the compactness, likelihood-normalization, and Gaussian-limit ingredients
used in the scalar Hájek--Le Cam convolution argument. The resulting exponential-tilt identity
and convolution factorization are completed in Convolution.
def efficientGaussianLaw reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
The efficient scalar Gaussian law associated with a canonical gradient is the centered normal distribution with variance equal to the squared norm of that gradient.
Definition (Lean source)
structure JointWeakSubsequence reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
A joint weak subsequential limit couples two row-indexed statistics whose marginal laws converge. The selected indices are strictly increasing, the joint laws converge against every bounded continuous test function, and the two marginals of the limit are the prescribed laws.
Definition (Lean source)
parameters
Ω :
ℕ → Type u_1
H :
Type u_2
subsequence :
ℕ → ℕ
P :
(n : ℕ) → Measure (Ω n)
statistic :
(n : ℕ) → Ω n → ℝ
centralSequence :
(n : ℕ) → Ω n → H
limitLaw :
Measure ℝ
scoreLimit :
Measure H
jointLaw :
Measure (ℝ × H)
assumes
converges :
∀ f : BoundedContinuousFunction (ℝ × H) ℝ,
The joint pushforward laws converge weakly along the selected indices.
fst_marginal :
Measure.map fst jointLaw = limitLaw
The first marginal is the prescribed scalar limit.
snd_marginal :
Measure.map snd jointLaw = scoreLimit
The second marginal is the prescribed score limit.
structure RegularLANJointLimit reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
A joint LAN limit couples the scalar estimator limit with the Gaussian central-sequence limit and satisfies the exponential-tilt identity forced by regularity under every fixed local direction. It is an intermediate conclusion of the LAN change-of-measure argument, not an assumption in the public convolution theorem.
Definition (Lean source)
parameters
H :
Type u_2
information :
BilinForm ℝ H
targetDerivative :
H →ₗ[ℝ] ℝ
limitLaw :
Measure ℝ
scoreLimit :
Measure H
jointLaw :
Measure (ℝ × H)
assumes
snd_marginal :
Measure.map snd jointLaw = scoreLimit
Its score marginal is the LAN Gaussian limit law.
tilt_identity :
∀ (t : ℝ) (h : H),
Exponential tilting by a local direction translates the estimator limit by the target derivative in that direction.
def lanLogLikelihoodLimit reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
The limiting log likelihood ratio in direction h is the affine projection inner h Z - information(h,h)/2 of the LAN Gaussian central-sequence limit.
theorem lan_logLikelihoodRatio_weaklyConverges reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
A locally asymptotically normal experiment and a fixed local direction make its guarded log likelihood ratio converge weakly to the affine Gaussian limit.
Formal statement
hypotheses
Ω :
ℕ → Type u_1
lan :
h :
H
conclusion
WeaklyConverges E.baseLaw (fun n ω => E.logLikelihoodRatio n h ω) (lanLogLikelihoodLimit information scoreLimit h)
Proof (Lean source)
theorem lan_logLikelihoodRatio_weaklyConverges
{E : LocalExperiment Ω H} {centralSequence : (n : ℕ) → Ω n → H}
{information : BilinForm ℝ H} {scoreLimit : Measure H}
(lan : IsLAN E centralSequence information scoreLimit) (h : H) :
WeaklyConverges E.baseLaw (fun n ω => E.logLikelihoodRatio n h ω)
(lanLogLikelihoodLimit information scoreLimit h) := by
let g : H → ℝ := fun z => inner ℝ h z - (1 / 2 : ℝ) * information h h
let R : (n : ℕ) → Ω n → ℝ := fun n ω =>
E.logLikelihoodRatio n h ω - inner ℝ h (centralSequence n ω) +
(1 / 2 : ℝ) * information h h
have hg : Continuous g := by fun_prop
have hX : WeaklyConverges E.baseLaw (fun n ω => g (centralSequence n ω))
(lanLogLikelihoodLimit information scoreLimit h) := by
refine ⟨fun n => hg.aemeasurable.comp_aemeasurable (lan.central_measurable n), ?_⟩
intro f
have hf := lan.central_converges.2
(f.compContinuous ⟨g, hg⟩)
simpa only [BoundedContinuousFunction.compContinuous_apply, ContinuousMap.coe_mk,
Function.comp_apply, g, lanLogLikelihoodLimit,
integral_map hg.aemeasurable f.continuous.aestronglyMeasurable] using hf
have hllr (n : ℕ) : AEMeasurable (E.logLikelihoodRatio n h) (E.baseLaw n) := by
let r : Ω n → ℝ := fun ω =>
((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal
have hr : Measurable r := (Measure.measurable_rnDeriv _ _).ennreal_toReal
unfold LocalExperiment.logLikelihoodRatio
exact (Measurable.ite (hr (measurableSet_singleton 0)) measurable_const hr.log).aemeasurable
have hRmeas (n : ℕ) : AEMeasurable (R n) (E.baseLaw n) := by
dsimp only [R]
have hi : Continuous (fun z : H => inner ℝ h z) := by fun_prop
exact ((hllr n).sub
(hi.aemeasurable.comp_aemeasurable (lan.central_measurable n))).add aemeasurable_const
have hlimitProb : IsProbabilityMeasure
(lanLogLikelihoodLimit information scoreLimit h) := by
letI : IsProbabilityMeasure scoreLimit := lan.gaussian_probability
exact Measure.isProbabilityMeasure_map hg.aemeasurable
have hsum := weaklyConverges_add_tendstoInProbability E.base_probability
hlimitProb hX (lan.expansion h) hRmeas
convert hsum using 1
funext n ω
dsimp only [g, R]
ring
5 supporting declarations (lemmas, instances)
-
efficientGaussianLaw_probabilityinstance — The efficient Gaussian law is a probability measure. -
exists_jointWeakSubsequencetheorem — Two measurable row-indexed statistics with weakly convergent probability marginals admit a joint weakly convergent subsequence, and every such joint limit has the prescribed marginals.hypothesesΩ :sharedℕ → Type u_1H :sharedType u_2P :(n : ℕ) → Measure (Ω n)statistic :(n : ℕ) → Ω n → ℝcentralSequence :(n : ℕ) → Ω n → HlimitLaw :Measure ℝscoreLimit :Measure HhP :∀ n, IsProbabilityMeasure (P n)hlimit :IsProbabilityMeasure limitLawhscore :IsProbabilityMeasure scoreLimithstatistic :WeaklyConverges P statistic limitLawhcentral :WeaklyConverges P centralSequence scoreLimitconclusion∃ (jointLaw : Measure (ℝ × H)) (subsequence : ℕ → ℕ),JointWeakSubsequence subsequence P statistic centralSequence limitLaw scoreLimit jointLawProof (Lean source)
theorem exists_jointWeakSubsequence {P : (n : ℕ) → Measure (Ω n)} {statistic : (n : ℕ) → Ω n → ℝ} {centralSequence : (n : ℕ) → Ω n → H} {limitLaw : Measure ℝ} {scoreLimit : Measure H} (hP : ∀ n, IsProbabilityMeasure (P n)) (hlimit : IsProbabilityMeasure limitLaw) (hscore : IsProbabilityMeasure scoreLimit) (hstatistic : WeaklyConverges P statistic limitLaw) (hcentral : WeaklyConverges P centralSequence scoreLimit) : ∃ (jointLaw : Measure (ℝ × H)) (subsequence : ℕ → ℕ), JointWeakSubsequence subsequence P statistic centralSequence limitLaw scoreLimit jointLaw := by let pair : (n : ℕ) → Ω n → ℝ × H := fun n ω => (statistic n ω, centralSequence n ω) have hpair (n : ℕ) : AEMeasurable (pair n) (P n) := (hstatistic.1 n).prodMk (hcentral.1 n) let jointPM : ℕ → ProbabilityMeasure (ℝ × H) := fun n => ⟨Measure.map (pair n) (P n), Measure.isProbabilityMeasure_map (hpair n)⟩ let statPM : ℕ → ProbabilityMeasure ℝ := fun n => ⟨Measure.map (statistic n) (P n), Measure.isProbabilityMeasure_map (hstatistic.1 n)⟩ let scorePM : ℕ → ProbabilityMeasure H := fun n => ⟨Measure.map (centralSequence n) (P n), Measure.isProbabilityMeasure_map (hcentral.1 n)⟩ let statLimitPM : ProbabilityMeasure ℝ := ⟨limitLaw, hlimit⟩ let scoreLimitPM : ProbabilityMeasure H := ⟨scoreLimit, hscore⟩ have hstatPM : Tendsto statPM atTop (𝓝 statLimitPM) := by rw [ProbabilityMeasure.tendsto_iff_forall_integral_tendsto] intro f simpa only [statPM, statLimitPM, ProbabilityMeasure.coe_mk, integral_map (hstatistic.1 _) f.continuous.aestronglyMeasurable] using hstatistic.2 f have hscorePM : Tendsto scorePM atTop (𝓝 scoreLimitPM) := by rw [ProbabilityMeasure.tendsto_iff_forall_integral_tendsto] intro f simpa only [scorePM, scoreLimitPM, ProbabilityMeasure.coe_mk, integral_map (hcentral.1 _) f.continuous.aestronglyMeasurable] using hcentral.2 f have hstatCompact : IsCompact (closure (range statPM)) := hstatPM.isCompact_insert_range.closure_of_subset (Set.range_subset_iff.mpr fun n => Set.mem_insert_iff.mpr (inr ⟨n, rfl⟩)) have hscoreCompact : IsCompact (closure (range scorePM)) := hscorePM.isCompact_insert_range.closure_of_subset (Set.range_subset_iff.mpr fun n => Set.mem_insert_iff.mpr (inr ⟨n, rfl⟩)) have hstatTight : IsTightMeasureSet (range fun n => (statPM n : Measure ℝ)) := by convert isTightMeasureSet_of_isCompact_closure hstatCompact using 1 ext μ simp have hscoreTight : IsTightMeasureSet (range fun n => (scorePM n : Measure H)) := by convert isTightMeasureSet_of_isCompact_closure hscoreCompact using 1 ext μ simp have hfst (n : ℕ) : Measure.fst (jointPM n : Measure (ℝ × H)) = statPM n := by dsimp [jointPM, statPM] change Measure.map fst (Measure.map (pair n) (P n)) = _ rw [(continuous_fst.aemeasurable).map_map_of_aemeasurable (hpair n)] rfl have hsnd (n : ℕ) : Measure.snd (jointPM n : Measure (ℝ × H)) = scorePM n := by dsimp [jointPM, scorePM] change Measure.map snd (Measure.map (pair n) (P n)) = _ rw [(continuous_snd.aemeasurable).map_map_of_aemeasurable (hpair n)] rfl have hjointTight : IsTightMeasureSet (range fun n => (jointPM n : Measure (ℝ × H))) := by apply IsTightMeasureSet.prodMk · convert hstatTight using 1 ext μ simp [hfst] · convert hscoreTight using 1 ext μ simp [hsnd] have hjointCompact : IsCompact (closure (range jointPM)) := by apply isCompact_closure_of_isTightMeasureSet convert hjointTight using 1 ext μ simp obtain ⟨jointLimitPM, -, subsequence, hsubseq, hjointLim⟩ := hjointCompact.isSeqCompact.subseq_of_frequently_in (Filter.Eventually.frequently (Filter.Eventually.of_forall fun n => subset_closure (Set.mem_range_self n))) refine ⟨jointLimitPM, subsequence, ?_⟩ have hfstLim : Tendsto (fun n => (jointPM (subsequence n)).map continuous_fst.aemeasurable) atTop (𝓝 (jointLimitPM.map continuous_fst.aemeasurable)) := ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous _ _ hjointLim continuous_fst have hsndLim : Tendsto (fun n => (jointPM (subsequence n)).map continuous_snd.aemeasurable) atTop (𝓝 (jointLimitPM.map continuous_snd.aemeasurable)) := ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous _ _ hjointLim continuous_snd have hstatSubseq : Tendsto (fun n => statPM (subsequence n)) atTop (𝓝 statLimitPM) := hstatPM.comp hsubseq.tendsto_atTop have hscoreSubseq : Tendsto (fun n => scorePM (subsequence n)) atTop (𝓝 scoreLimitPM) := hscorePM.comp hsubseq.tendsto_atTop have hfstPM (n : ℕ) : (jointPM n).map continuous_fst.aemeasurable = statPM n := Subtype.ext (hfst n) have hsndPM (n : ℕ) : (jointPM n).map continuous_snd.aemeasurable = scorePM n := Subtype.ext (hsnd n) have hfstEq : jointLimitPM.map continuous_fst.aemeasurable = statLimitPM := by apply tendsto_nhds_unique hfstLim simpa only [hfstPM] using hstatSubseq have hsndEq : jointLimitPM.map continuous_snd.aemeasurable = scoreLimitPM := by apply tendsto_nhds_unique hsndLim simpa only [hsndPM] using hscoreSubseq refine { subsequence_strictMono := hsubseq probability := jointLimitPM.property converges := ?_ fst_marginal := ?_ snd_marginal := ?_ } · intro f have hf := (ProbabilityMeasure.tendsto_iff_forall_integral_tendsto.mp hjointLim) f have hf' : Tendsto (fun n => ∫ z, f z ∂(jointPM (subsequence n) : Measure (ℝ × H))) atTop (𝓝 (∫ z, f z ∂(jointLimitPM : Measure (ℝ × H)))) := by simpa only [Function.comp_apply] using hf have heq : (fun n => ∫ ω, f (statistic (subsequence n) ω, centralSequence (subsequence n) ω) ∂P (subsequence n)) = (fun n => ∫ z, f z ∂(jointPM (subsequence n) : Measure (ℝ × H))) := by funext n rw [show (jointPM (subsequence n) : Measure (ℝ × H)) = Measure.map (pair (subsequence n)) (P (subsequence n)) from rfl] rw [integral_map (hpair _) f.continuous.aestronglyMeasurable] rw [heq] exact hf' · exact congr_arg ProbabilityMeasure.toMeasure hfstEq · exact congr_arg ProbabilityMeasure.toMeasure hsndEq -
integral_exp_logLikelihoodRatio_letheorem — The expectation of the exponential of the guarded log likelihood ratio is bounded by the local probability mass plus the artificial exp (-n) contribution on its zero-density set.hypothesesProof (Lean source)
theorem integral_exp_logLikelihoodRatio_le (E : LocalExperiment Ω H) (n : ℕ) (h : H) : ∫ ω, exp (E.logLikelihoodRatio n h ω) ∂E.baseLaw n ≤ 1 + exp (-(n : ℝ)) := by letI : IsProbabilityMeasure (E.baseLaw n) := E.base_probability n letI : IsProbabilityMeasure (E.localLaw n h) := E.local_probability n h let r : Ω n → ℝ := fun ω => ((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal have hr_meas : Measurable r := (Measure.measurable_rnDeriv _ _).ennreal_toReal have hllr_meas : Measurable (E.logLikelihoodRatio n h) := by unfold LocalExperiment.logLikelihoodRatio exact Measurable.ite (hr_meas (measurableSet_singleton 0)) measurable_const hr_meas.log have hpoint : ∀ ω, exp (E.logLikelihoodRatio n h ω) ≤ r ω + exp (-(n : ℝ)) := by intro ω unfold LocalExperiment.logLikelihoodRatio dsimp only by_cases hz : r ω = 0 · rw [if_pos hz, hz, zero_add] · rw [if_neg hz, Real.exp_log (lt_of_le_of_ne ENNReal.toReal_nonneg (Ne.symm hz))] exact le_add_of_nonneg_right (Real.exp_pos _).le have hr_int : Integrable r (E.baseLaw n) := by simpa only [integrableOn_univ] using (Measure.integrableOn_toReal_rnDeriv (μ := E.localLaw n h) (ν := E.baseLaw n) (s := univ) (measure_ne_top _ _)) have hexp_int : Integrable (fun ω => exp (E.logLikelihoodRatio n h ω)) (E.baseLaw n) := by apply (hr_int.add (integrable_const (exp (-(n : ℝ))))).mono' hllr_meas.exp.aestronglyMeasurable exact ae_of_all _ fun ω => by rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] exact hpoint ω calc (∫ ω, exp (E.logLikelihoodRatio n h ω) ∂E.baseLaw n) ≤ ∫ ω, (r ω + exp (-(n : ℝ))) ∂E.baseLaw n := integral_mono_ae hexp_int (hr_int.add (integrable_const (exp (-(n : ℝ))))) (ae_of_all _ hpoint) _ = (∫ ω, r ω ∂E.baseLaw n) + exp (-(n : ℝ)) := by rw [integral_add hr_int (integrable_const _), integral_const] simp _ ≤ 1 + exp (-(n : ℝ)) := by gcongr rw [← setIntegral_univ] exact (Measure.setIntegral_toReal_rnDeriv_le (μ := E.localLaw n h) (ν := E.baseLaw n) (s := univ) (measure_ne_top _ _)).trans measureReal_le_one -
integral_exp_lanLogLikelihoodLimittheorem — The exponential moment of the affine Gaussian LAN log-likelihood limit equals one.hypotheseshscoreProb :IsProbabilityMeasure scoreLimith :Hconclusion∫ y, exp y ∂lanLogLikelihoodLimit information scoreLimit h = 1Proof (Lean source)
theorem integral_exp_lanLogLikelihoodLimit {information : BilinForm ℝ H} {scoreLimit : Measure H} (hscoreProb : IsProbabilityMeasure scoreLimit) (hscoreChar : ∀ t : H, charFun scoreLimit t = exp (-((information t t : ℂ) / 2))) (h : H) : ∫ y, exp y ∂lanLogLikelihoodLimit information scoreLimit h = 1 := by letI : IsProbabilityMeasure scoreLimit := hscoreProb have hv : 0 ≤ information h h := by have hn := norm_charFun_le_one (μ := scoreLimit) h rw [hscoreChar h, Complex.norm_exp] at hn norm_num at hn linarith have hproj : Measure.map (fun z => inner ℝ h z) scoreLimit = gaussianReal 0 (information h h).toNNReal := by apply Measure.ext_of_charFun funext t rw [charFun_apply, integral_map (by fun_prop) (by fun_prop)] have heq : (∫ x, exp ((inner ℝ (inner ℝ h x) t : ℂ) * I) ∂scoreLimit) = charFun scoreLimit (t • h) := by rw [charFun_apply] congr with x congr 2 simp [inner_smul_right, real_inner_comm] rw [heq, hscoreChar (t • h), charFun_gaussianReal] simp [Real.coe_toNNReal _ hv, map_smul] congr 1 ring have hlaw : lanLogLikelihoodLimit information scoreLimit h = Measure.map (fun x : ℝ => x - (1 / 2 : ℝ) * information h h) (gaussianReal 0 (information h h).toNNReal) := by unfold lanLogLikelihoodLimit have hmap := AEMeasurable.map_map_of_aemeasurable (μ := scoreLimit) (g := fun x : ℝ => x - (1 / 2 : ℝ) * information h h) (f := fun z : H => inner ℝ h z) (by fun_prop) (by fun_prop) calc Measure.map (fun z : H => inner ℝ h z - (1 / 2 : ℝ) * information h h) scoreLimit = Measure.map ((fun x : ℝ => x - (1 / 2 : ℝ) * information h h) ∘ fun z : H => inner ℝ h z) scoreLimit := rfl _ = Measure.map (fun x : ℝ => x - (1 / 2 : ℝ) * information h h) (Measure.map (fun z : H => inner ℝ h z) scoreLimit) := hmap.symm _ = _ := congrArg _ hproj rw [hlaw, integral_map (by fun_prop) (by fun_prop)] have hexp (x : ℝ) : exp (x - (1 / 2 : ℝ) * information h h) = exp x * exp (-(1 / 2 : ℝ) * information h h) := by rw [sub_eq_add_neg, Real.exp_add] congr 2 ring simp_rw [hexp] rw [integral_mul_const] have hmgf := congr_fun (mgf_id_gaussianReal (μ := 0) (v := (information h h).toNNReal)) 1 simp [mgf, Real.coe_toNNReal _ hv] at hmgf ⊢ rw [hmgf, ← Real.exp_add] rw [← Real.exp_zero] congr 1 ring -
lan_likelihoodRatio_integral_tendsto_onetheorem — In a LAN experiment, the exponential of the guarded log likelihood ratio has expectation tending to one under the base law. Equivalently, the asymptotically negligible singular part of the local law cannot lose mass in the Gaussian likelihood-ratio limit.hypothesesΩ :sharedℕ → Type u_1lan :h :HProof (Lean source)
theorem lan_likelihoodRatio_integral_tendsto_one {E : LocalExperiment Ω H} {centralSequence : (n : ℕ) → Ω n → H} {information : BilinForm ℝ H} {scoreLimit : Measure H} (lan : IsLAN E centralSequence information scoreLimit) (h : H) : Tendsto (fun n => ∫ ω, exp (E.logLikelihoodRatio n h ω) ∂E.baseLaw n) atTop (𝓝 1) := by have hlimitProb : IsProbabilityMeasure (lanLogLikelihoodLimit information scoreLimit h) := by letI : IsProbabilityMeasure scoreLimit := lan.gaussian_probability exact Measure.isProbabilityMeasure_map (by fun_prop) have hrowIntegrable : ∀ n, Integrable (fun ω => exp (E.logLikelihoodRatio n h ω)) (E.baseLaw n) := by intro n letI : IsProbabilityMeasure (E.baseLaw n) := E.base_probability n letI : IsProbabilityMeasure (E.localLaw n h) := E.local_probability n h let r : Ω n → ℝ := fun ω => ((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal have hr_meas : Measurable r := (Measure.measurable_rnDeriv _ _).ennreal_toReal have hllr_meas : Measurable (E.logLikelihoodRatio n h) := by unfold LocalExperiment.logLikelihoodRatio exact Measurable.ite (hr_meas (measurableSet_singleton 0)) measurable_const hr_meas.log have hr_int : Integrable r (E.baseLaw n) := by simpa only [integrableOn_univ] using (Measure.integrableOn_toReal_rnDeriv (μ := E.localLaw n h) (ν := E.baseLaw n) (s := univ) (measure_ne_top _ _)) apply (hr_int.add (integrable_const (exp (-(n : ℝ))))).mono' hllr_meas.exp.aestronglyMeasurable exact ae_of_all _ fun ω => by rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] change exp (E.logLikelihoodRatio n h ω) ≤ r ω + exp (-(n : ℝ)) unfold LocalExperiment.logLikelihoodRatio dsimp only by_cases hz : r ω = 0 · rw [if_pos hz, hz, zero_add] · rw [if_neg hz, Real.exp_log (lt_of_le_of_ne ENNReal.toReal_nonneg (Ne.symm hz))] exact le_add_of_nonneg_right (Real.exp_pos _).le exact exp_integral_tendsto_one_of_weaklyConverges E.base_probability hlimitProb (lan_logLikelihoodRatio_weaklyConverges lan h) hrowIntegrable (integral_exp_lanLogLikelihoodLimit lan.gaussian_probability lan.gaussian_charFun h) (fun n => integral_exp_logLikelihoodRatio_le E n h)
IIDDQM 9 core · 6 supporting 1 to review This module defines dominated finite-dimensional i.i.d. ★ local_zeroBaseDensity_mass
Dominated i.i.d. quadratic-mean differentiability
This module defines dominated finite-dimensional i.i.d. models, quadratic-mean differentiability,
their score information, and the product-likelihood ingredients for local asymptotic normality.
The closing LAN theorem and remaining triangular-array argument are in IIDDQMLAN.
structure DominatedIIDModel unreviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
A dominated finite-dimensional i.i.d. model is a probability law law θ for every parameter θ, together with one common dominating measure. The base parameter is 0.
Definition (Lean source)
parameters
X H :
Type*
fields
Observation law at parameter `θ`.
law :
H → Measure X
Every observation law has total mass one.
probability :
∀ θ, IsProbabilityMeasure (law θ)
Common dominating measure used to state DQM.
dominating :
Measure X
The dominating measure is sigma-finite, so its Radon--Nikodym densities represent the
model laws.
dominating_sigmaFinite :
SigmaFinite dominating
Every model law is absolutely continuous with respect to the dominating measure.
absolutelyContinuous :
∀ θ, law θ ≪ dominating
def sqrtDensity reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution.DominatedIIDModel
The square root of the density of law θ with respect to the model's dominating measure.
Definition (Lean source)
parameters
def
sqrtDensity M θ x :
ℝ
def iidLaw reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution.DominatedIIDModel
The n-observation i.i.d. law is the finite product of the one-observation law.
Definition (Lean source)
parameters
given by
Measure.pi (fun _ : Fin n => M.law θ)
structure IIDQuadraticMeanDifferentiable reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
Quadratic-mean differentiability at the base parameter 0 with score score. The squared L² error in the first-order square-root-density expansion is little-o of ‖h‖², and the score is measurable and square-integrable under the base law.
Definition (Lean source)
parameters
fields
Vector score at the base parameter.
score :
X → H
Measurability of the score.
score_measurable :
Measurable score
Square integrability of the score under the base observation law.
score_squareIntegrable :
Integrable (fun x => ‖score x‖ ^ 2) (M.law 0)
The defining quadratic-mean expansion of the square-root densities.
expansion :
(fun h => ∫ x, (M.sqrtDensity h x - M.sqrtDensity 0 x - (1 / 2 : ℝ) * inner ℝ h (score x) * M.sqrtDensity 0 x) ^ 2 ∂M.dominating)
=o[𝓝 0] fun h : H => ‖h‖ ^ 2
def information reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution.IIDQuadraticMeanDifferentiable
Fisher information is the bilinear second moment of the DQM score.
Definition (Lean source)
parameters
X :
Type u_1
H :
Type u_2
M :
qmd :
def
given by
LinearMap.mk₂ ℝ (fun h g => inner ℝ (secondMomentLM qmd.score_measurable qmd.score_squareIntegrable h) g) (by intros; rw [map_add, inner_add_left]) (by intros; rw [map_smul, inner_smul_left]; simp) (by intros; rw [inner_add_right]) (by intros; simp only [inner_smul_right, smul_eq_mul])
def centralSequence reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution.IIDQuadraticMeanDifferentiable
The normalized score sum on the canonical n-fold product sample.
def localExperiment reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution.IIDQuadraticMeanDifferentiable
The canonical local experiment of an i.i.d. model uses the base product law at parameter zero and the local product law at parameter (sqrt n)⁻¹ • h.
Definition (Lean source)
parameters
def
given by
clause 1
baseLaw n := M.iidLaw 0 n
clause 2
localLaw n h := M.iidLaw ((sqrt (n : ℝ))⁻¹ • h) n
clause 3
base_probability n := iidLaw_probability M 0 n
clause 4
local_probability n h := iidLaw_probability M ((sqrt (n : ℝ))⁻¹ • h) n
clause 5
local_zero n := by simp
def sqrtLikelihoodIncrement reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution.IIDQuadraticMeanDifferentiable
Twice the relative square-root likelihood increment for one observation at local parameter h / sqrt n. It is set to zero on the zero set of the base square-root density; the local mass of that set is controlled separately.
Definition (Lean source)
parameters
X :
Type u_1
qmd :
n :
ℕ
h :
H
x :
X
def
sqrtLikelihoodIncrement qmd n h x :
ℝ
given by
if M.sqrtDensity 0 x
= 0 then 0 else 2 * (M.sqrtDensity ((sqrt (n : ℝ))⁻¹ • h) x / M.sqrtDensity 0 x - 1)
theorem local_zeroBaseDensity_mass reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution.IIDQuadraticMeanDifferentiable
For a dominated i.i.d. model that is quadratic-mean differentiable and a fixed local direction, the local probability mass outside the base-law support is little-o of one over the sample size.
Formal statement
hypotheses
X :
Type u_1
qmd :
h :
H
Proof (Lean source)
theorem local_zeroBaseDensity_mass (qmd : IIDQuadraticMeanDifferentiable M) (h : H) :
Tendsto (fun n : ℕ => (n : ℝ) * (M.law ((sqrt (n : ℝ))⁻¹ • h)
{x | M.sqrtDensity 0 x = 0}).toReal) atTop (𝓝 0) := by
-- On the zero set of the base density both the base term and score-linear term in the
-- DQM expansion vanish, so the squared remainder is exactly the local density.
letI : SigmaFinite M.dominating := M.dominating_sigmaFinite
have hsqrt_meas (u : H) : Measurable (M.sqrtDensity u) := by
unfold DominatedIIDModel.sqrtDensity
exact Real.continuous_sqrt.measurable.comp
(ENNReal.measurable_toReal.comp (Measure.measurable_rnDeriv _ _))
have hzero : MeasurableSet {x | M.sqrtDensity 0 x = 0} :=
(hsqrt_meas 0) (measurableSet_singleton 0)
have hupper (n : ℕ) :
(M.law ((sqrt (n : ℝ))⁻¹ • h)
{x | M.sqrtDensity 0 x = 0}).toReal ≤
∫ x, qmd.dqmRemainder ((sqrt (n : ℝ))⁻¹ • h) x ^ 2 ∂M.dominating := by
let _ : IsProbabilityMeasure (M.law ((sqrt (n : ℝ))⁻¹ • h)) :=
M.probability _
rw [← measureReal_def, ← Measure.setIntegral_toReal_rnDeriv
(M.absolutelyContinuous ((sqrt (n : ℝ))⁻¹ • h))]
calc
(∫ x in {x | M.sqrtDensity 0 x = 0},
((M.law ((sqrt (n : ℝ))⁻¹ • h)).rnDeriv M.dominating x).toReal
∂M.dominating) =
∫ x in {x | M.sqrtDensity 0 x = 0},
qmd.dqmRemainder ((sqrt (n : ℝ))⁻¹ • h) x ^ 2 ∂M.dominating := by
apply integral_congr_ae
filter_upwards [ae_restrict_mem hzero] with x hx
rw [← Real.sq_sqrt ENNReal.toReal_nonneg]
simp only [dqmRemainder, hx, mul_zero, sub_zero]
rfl
_ ≤ ∫ x, qmd.dqmRemainder
((sqrt (n : ℝ))⁻¹ • h) x ^ 2 ∂M.dominating :=
setIntegral_le_integral (qmd.dqmRemainder_sq_integrable _)
(ae_of_all _ fun x => sq_nonneg _)
apply squeeze_zero
· intro n
exact mul_nonneg (Nat.cast_nonneg _) ENNReal.toReal_nonneg
· intro n
exact mul_le_mul_of_nonneg_left (hupper n) (Nat.cast_nonneg _)
· exact qmd.scaledDqmRemainder_tendsto h
6 supporting declarations (lemmas, instances)
-
information_applytheorem — Evaluating the Fisher-information form gives the second moment of the two scalar score projections.hypothesesX :sharedType u_1qmd :h g :HProof (Lean source)
theorem information_apply (qmd : IIDQuadraticMeanDifferentiable M) (h g : H) : qmd.information M h g = ∫ x, inner ℝ h (qmd.score x) * inner ℝ g (qmd.score x) ∂M.law 0 := by rw [information] exact secondMomentLM_inner qmd.score_measurable qmd.score_squareIntegrable h g -
score_integral_eq_zerotheorem — DQM forces the score to have mean zero under the base law. This is the normalization identity obtained by differentiating the total mass of the model.hypothesesconclusion∫ x, qmd.score x ∂M.law 0 = 0Proof (Lean source)
theorem score_integral_eq_zero (qmd : IIDQuadraticMeanDifferentiable M) : ∫ x, qmd.score x ∂M.law 0 = 0 := by -- Proof plan: expand equality of the two density masses along `t • h`, divide the -- square-root-density identity by `t`, use the DQM `L²` remainder and Cauchy--Schwarz, -- then separate vectors by inner products. letI : SigmaFinite M.dominating := M.dominating_sigmaFinite have hsqrt_sq (θ : H) : ∫ x, M.sqrtDensity θ x ^ 2 ∂M.dominating = 1 := by let _ : IsProbabilityMeasure (M.law θ) := M.probability θ have hpoint : (fun x => M.sqrtDensity θ x ^ 2) =ᵐ[M.dominating] fun x => ((M.law θ).rnDeriv M.dominating x).toReal := by filter_upwards [] with x exact Real.sq_sqrt ENNReal.toReal_nonneg rw [integral_congr_ae hpoint, Measure.integral_toReal_rnDeriv (M.absolutelyContinuous θ)] simp have hp_mem (θ : H) : MemLp (M.sqrtDensity θ) 2 M.dominating := by have hpmeas : Measurable (M.sqrtDensity θ) := by unfold DominatedIIDModel.sqrtDensity exact Real.continuous_sqrt.measurable.comp (ENNReal.measurable_toReal.comp (Measure.measurable_rnDeriv _ _)) apply (memLp_two_iff_integrable_sq_norm hpmeas.aestronglyMeasurable).2 let _ : IsProbabilityMeasure (M.law θ) := M.probability θ refine (Measure.integrable_toReal_rnDeriv (μ := M.law θ) (ν := M.dominating)).congr ?_ filter_upwards [] with x simp only [DominatedIIDModel.sqrtDensity, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _), Real.sq_sqrt ENNReal.toReal_nonneg] have hproj_int (h : H) : Integrable (fun x => inner ℝ h (qmd.score x) ^ 2) (M.law 0) := by refine Integrable.mono' (qmd.score_squareIntegrable.const_mul (‖h‖ ^ 2)) ((qmd.score_measurable.const_inner (c := h)).pow_const 2).aestronglyMeasurable (ae_of_all _ fun x => ?_) simp only [norm_pow, Real.norm_eq_abs] calc |inner ℝ h (qmd.score x)| ^ 2 ≤ (‖h‖ * ‖qmd.score x‖) ^ 2 := (sq_le_sq₀ (abs_nonneg _) (mul_nonneg (norm_nonneg _) (norm_nonneg _))).2 (abs_real_inner_le_norm h (qmd.score x)) _ = ‖h‖ ^ 2 * ‖qmd.score x‖ ^ 2 := by ring let aRaw (h : H) (x : X) : ℝ := (1 / 2 : ℝ) * inner ℝ h (qmd.score x) * M.sqrtDensity 0 x have ha_mem (h : H) : MemLp (aRaw h) 2 M.dominating := by have hpmeas : Measurable (M.sqrtDensity 0) := by unfold DominatedIIDModel.sqrtDensity exact Real.continuous_sqrt.measurable.comp (ENNReal.measurable_toReal.comp (Measure.measurable_rnDeriv _ _)) have hameas : Measurable (aRaw h) := by unfold aRaw exact (qmd.score_measurable.const_inner (c := h)).const_mul (1 / 2) |>.mul hpmeas apply (memLp_two_iff_integrable_sq_norm hameas.aestronglyMeasurable).2 let _ : IsProbabilityMeasure (M.law 0) := M.probability 0 have hw := (integrable_toReal_rnDeriv_mul_iff (M.absolutelyContinuous 0)).2 (hproj_int h) refine (hw.const_mul ((1 / 2 : ℝ) ^ 2)).congr ?_ filter_upwards [] with x simp only [aRaw, DominatedIIDModel.sqrtDensity, Real.norm_eq_abs, abs_mul, abs_of_nonneg (Real.sqrt_nonneg _)] norm_num [mul_pow, sq_abs, Real.sq_sqrt ENNReal.toReal_nonneg] <;> ring let p (θ : H) : Lp ℝ 2 M.dominating := (hp_mem θ).toLp (M.sqrtDensity θ) let a (h : H) : Lp ℝ 2 M.dominating := (ha_mem h).toLp (aRaw h) have hnorm_sq_toLp (f : X → ℝ) (hf : MemLp f 2 M.dominating) : ‖hf.toLp f‖ ^ 2 = ∫ x, f x ^ 2 ∂M.dominating := by rw [← real_inner_self_eq_norm_sq, L2.inner_def] apply integral_congr_ae filter_upwards [hf.coeFn_toLp] with x hx simp only [hx, real_inner_self_eq_norm_sq, Real.norm_eq_abs, sq_abs] have hnormp (θ : H) : ‖p θ‖ ^ 2 = 1 := by change ‖(hp_mem θ).toLp (M.sqrtDensity θ)‖ ^ 2 = 1 rw [hnorm_sq_toLp] exact hsqrt_sq θ let _ : IsProbabilityMeasure (M.law 0) := M.probability 0 have hscore_int : Integrable qmd.score (M.law 0) := ((memLp_two_iff_integrable_sq_norm qmd.score_measurable.aestronglyMeasurable).2 qmd.score_squareIntegrable).integrable (by norm_num) have hinner (h : H) : inner ℝ (p 0) (a h) = (1 / 2 : ℝ) * inner ℝ h (∫ x, qmd.score x ∂M.law 0) := by change inner ℝ ((hp_mem 0).toLp (M.sqrtDensity 0)) ((ha_mem h).toLp (aRaw h)) = _ rw [L2.inner_def] have hae := (hp_mem 0).coeFn_toLp.and (ha_mem h).coeFn_toLp have hi : (∫ x, inner ℝ (((hp_mem 0).toLp (M.sqrtDensity 0)) x) (((ha_mem h).toLp (aRaw h)) x) ∂M.dominating) = ∫ x, M.sqrtDensity 0 x * aRaw h x ∂M.dominating := by apply integral_congr_ae filter_upwards [hae] with x hx simp only [hx.1, hx.2, Real.inner_apply] rw [hi] calc (∫ x, M.sqrtDensity 0 x * aRaw h x ∂M.dominating) = (1 / 2 : ℝ) * ∫ x, ((M.law 0).rnDeriv M.dominating x).toReal * inner ℝ h (qmd.score x) ∂M.dominating := by rw [← integral_const_mul] apply integral_congr_ae filter_upwards [] with x simp only [aRaw, DominatedIIDModel.sqrtDensity] ring_nf rw [Real.sq_sqrt ENNReal.toReal_nonneg] ring _ = (1 / 2 : ℝ) * ∫ x, inner ℝ h (qmd.score x) ∂M.law 0 := by congr 1 simpa only [smul_eq_mul] using (integral_rnDeriv_smul (f := fun x => inner ℝ h (qmd.score x)) (M.absolutelyContinuous 0)) _ = (1 / 2 : ℝ) * inner ℝ h (∫ x, qmd.score x ∂M.law 0) := by rw [integral_inner hscore_int h] have hderiv (h : H) : HasDerivAt (fun t : ℝ => p (t • h)) (a h) 0 := by let rRaw (t : ℝ) (x : X) : ℝ := M.sqrtDensity (t • h) x - M.sqrtDensity 0 x - t * aRaw h x have hr_mem (t : ℝ) : MemLp (rRaw t) 2 M.dominating := by have := ((hp_mem (t • h)).sub (hp_mem 0)).sub ((ha_mem h).const_smul t) change MemLp (M.sqrtDensity (t • h) - M.sqrtDensity 0 - t • aRaw h) 2 M.dominating exact this have hr_eq (t : ℝ) : p (t • h) - p 0 - t • a h = (hr_mem t).toLp (rRaw t) := by change (hp_mem (t • h)).toLp (M.sqrtDensity (t • h)) - (hp_mem 0).toLp (M.sqrtDensity 0) - t • (ha_mem h).toLp (aRaw h) = _ rw [← MemLp.toLp_sub, ← MemLp.toLp_const_smul, ← MemLp.toLp_sub] apply MemLp.toLp_congr exact ae_of_all _ fun x => rfl have hr_norm_sq (t : ℝ) : ‖p (t • h) - p 0 - t • a h‖ ^ 2 = ∫ x, rRaw t x ^ 2 ∂M.dominating := by rw [hr_eq, hnorm_sq_toLp] have he : (fun t : ℝ => ∫ x, rRaw t x ^ 2 ∂M.dominating) =o[𝓝 0] fun t : ℝ => ‖t • h‖ ^ 2 := by have ht : Tendsto (fun t : ℝ => t • h) (𝓝 0) (𝓝 0) := by rw [tendsto_zero_iff_norm_tendsto_zero] simpa only [norm_smul, zero_mul] using tendsto_norm_zero.mul_const ‖h‖ have hc := qmd.expansion.comp_tendsto ht refine hc.congr (fun t => ?_) (fun _ => rfl) simp only [Function.comp_apply] apply integral_congr_ae filter_upwards [] with x congr 1 simp only [rRaw, aRaw, inner_smul_left, starRingEnd_apply, star_trivial] ring have hs := he.sqrt (Filter.Eventually.of_forall fun t : ℝ => sq_nonneg ‖t • h‖) have hsnorm : (fun t : ℝ => ‖p (t • h) - p 0 - t • a h‖) =o[𝓝 0] fun t : ℝ => ‖t • h‖ := by refine hs.congr (fun t => ?_) (fun t => ?_) · rw [← hr_norm_sq, Real.sqrt_sq (norm_nonneg _)] · rw [Real.sqrt_sq (norm_nonneg _)] have hbig : (fun t : ℝ => ‖t • h‖) =O[𝓝 0] fun t : ℝ => t := by apply Asymptotics.IsBigO.of_bound ‖h‖ filter_upwards [] with t simp only [Real.norm_eq_abs, norm_smul] rw [abs_of_nonneg (mul_nonneg (abs_nonneg _) (norm_nonneg _))] exact le_of_eq (mul_comm _ _) rw [hasDerivAt_iff_isLittleO_nhds_zero] simp only [zero_add, zero_smul] exact (Asymptotics.isLittleO_norm_left.mp (hsnorm.trans_isBigO hbig)) have horth (h : H) : inner ℝ h (∫ x, qmd.score x ∂M.law 0) = 0 := by have hd := (hderiv h).norm_sq have hc : HasDerivAt (fun t : ℝ => ‖p (t • h)‖ ^ 2) 0 0 := (hasDerivAt_const (x := 0) (1 : ℝ)).congr_of_eventuallyEq (Filter.Eventually.of_forall fun t => hnormp (t • h)) have hu := hd.unique hc simp only [zero_smul] at hu rw [hinner] at hu linarith apply (inner_self_eq_zero (𝕜 := ℝ)).mp exact horth (∫ x, qmd.score x ∂M.law 0) -
information_isSymm_nonnegativetheorem — The score second-moment form is symmetric and nonnegative.hypothesesconclusionconclusion 1(qmd.information M).IsSymmconclusion 2h :0 ≤ qmd.information M h hProof (Lean source)
theorem information_isSymm_nonnegative (qmd : IIDQuadraticMeanDifferentiable M) : (qmd.information M).IsSymm ∧ ∀ h, 0 ≤ qmd.information M h h := by -- Rewrite with `information_apply`; symmetry is commutativity of multiplication and -- nonnegativity is the integral of a square. constructor · refine ⟨fun h g => ?_⟩ rw [information_apply, information_apply] exact integral_congr_ae (ae_of_all _ fun x => mul_comm _ _) · intro h rw [information_apply] exact integral_nonneg fun x => mul_self_nonneg _ -
iidLaw_probabilitytheorem — Every finite product law of a dominated i.i.d. probability model is a probability measure.hypothesesconclusionIsProbabilityMeasure (M.iidLaw θ n)Proof (Lean source)
theorem iidLaw_probability (M : DominatedIIDModel X H) (θ : H) (n : ℕ) : IsProbabilityMeasure (M.iidLaw θ n) := by -- Install `M.probability θ` for each `Fin n` coordinate and use the `Measure.pi` instance. let _ : ∀ _ : Fin n, IsProbabilityMeasure (M.law θ) := fun _ => M.probability θ change IsProbabilityMeasure (Measure.pi (fun _ : Fin n => M.law θ)) exact inferInstance -
iidLaw_rnDeriv_eq_prodtheorem — The Radon--Nikodym derivative of a finite i.i.d. product law is the product of the one-observation Radon--Nikodym derivatives (of their absolutely continuous parts). No one-observation absolute-continuity assumption is needed.hypothesesconclusion(M.iidLaw θ n).rnDeriv (M.iidLaw 0 n)=ᵐ[M.iidLaw 0 n] fun x => ∏ i, (M.law θ).rnDeriv (M.law 0) (x i)Proof (Lean source)
theorem iidLaw_rnDeriv_eq_prod (M : DominatedIIDModel X H) (θ : H) (n : ℕ) : (M.iidLaw θ n).rnDeriv (M.iidLaw 0 n) =ᵐ[M.iidLaw 0 n] fun x => ∏ i, (M.law θ).rnDeriv (M.law 0) (x i) := by -- Induct over `Fin n`, using the binary product Radon--Nikodym formula. Probability -- measures supply every sigma-finiteness instance required by the product theorem. let _ : IsProbabilityMeasure (M.law θ) := M.probability θ let _ : IsProbabilityMeasure (M.law 0) := M.probability 0 exact rnDeriv_pi_const (M.law θ) (M.law 0) n -
sqrtLikelihoodIncrement_L2theorem — DQM makes the one-observation square-root likelihood increment equal to the projected score divided by sqrt n, with squared error o(1/n) under the base law.hypothesesX :sharedType u_1qmd :h :HProof (Lean source)
theorem sqrtLikelihoodIncrement_L2 (qmd : IIDQuadraticMeanDifferentiable M) (h : H) : Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, (qmd.sqrtLikelihoodIncrement n h x - (sqrt (n : ℝ))⁻¹ * inner ℝ h (qmd.score x)) ^ 2 ∂M.law 0) atTop (𝓝 0) := by -- Restrict the dominating-measure DQM remainder to the support of the base density, -- cancel that density against `d(M.law 0)`, and compose the little-o estimate with -- `n ↦ h / sqrt n`. Handle the harmless `n = 0` row separately. letI : SigmaFinite M.dominating := M.dominating_sigmaFinite let _ : IsProbabilityMeasure (M.law 0) := M.probability 0 let err (n : ℕ) (x : X) : ℝ := qmd.sqrtLikelihoodIncrement n h x - (sqrt (n : ℝ))⁻¹ * inner ℝ h (qmd.score x) have hpoint (n : ℕ) (x : X) : ((M.law 0).rnDeriv M.dominating x).toReal * err n x ^ 2 ≤ 4 * qmd.dqmRemainder ((sqrt (n : ℝ))⁻¹ • h) x ^ 2 := by rw [← Real.sq_sqrt ENNReal.toReal_nonneg] change M.sqrtDensity 0 x ^ 2 * err n x ^ 2 ≤ _ by_cases hp : M.sqrtDensity 0 x = 0 · simp [hp, sq_nonneg] · simp only [err, sqrtLikelihoodIncrement, hp, if_false, dqmRemainder, inner_smul_left, starRingEnd_apply, star_trivial] field_simp ring exact le_rfl have hupper (n : ℕ) : ∫ x, err n x ^ 2 ∂M.law 0 ≤ 4 * ∫ x, qmd.dqmRemainder ((sqrt (n : ℝ))⁻¹ • h) x ^ 2 ∂M.dominating := by rw [← integral_toReal_rnDeriv_mul (M.absolutelyContinuous 0)] have hg : Integrable (fun x => 4 * qmd.dqmRemainder ((sqrt (n : ℝ))⁻¹ • h) x ^ 2) M.dominating := (qmd.dqmRemainder_sq_integrable _).const_mul 4 have hf : Integrable (fun x => ((M.law 0).rnDeriv M.dominating x).toReal * err n x ^ 2) M.dominating := by have hsqrt_meas (u : H) : Measurable (M.sqrtDensity u) := by unfold DominatedIIDModel.sqrtDensity exact Real.continuous_sqrt.measurable.comp (ENNReal.measurable_toReal.comp (Measure.measurable_rnDeriv _ _)) have hzero : MeasurableSet {x | M.sqrtDensity 0 x = 0} := (hsqrt_meas 0) (measurableSet_singleton 0) have hinc : Measurable (qmd.sqrtLikelihoodIncrement n h) := by unfold sqrtLikelihoodIncrement apply Measurable.ite hzero measurable_const exact (((hsqrt_meas _).div (hsqrt_meas 0)).sub_const 1).const_mul 2 have herr : Measurable (err n) := by unfold err exact hinc.sub ((qmd.score_measurable.const_inner (c := h)).const_mul _) refine Integrable.mono' hg (((ENNReal.measurable_toReal.comp (Measure.measurable_rnDeriv _ _)).mul (herr.pow_const 2)).aestronglyMeasurable) ?_ filter_upwards [] with x simpa only [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg ENNReal.toReal_nonneg (sq_nonneg _)), abs_of_nonneg (mul_nonneg (by norm_num) (sq_nonneg _))] using hpoint n x calc (∫ x, ((M.law 0).rnDeriv M.dominating x).toReal * err n x ^ 2 ∂M.dominating) ≤ ∫ x, 4 * qmd.dqmRemainder ((sqrt (n : ℝ))⁻¹ • h) x ^ 2 ∂M.dominating := integral_mono_ae hf hg (ae_of_all _ (hpoint n)) _ = 4 * ∫ x, qmd.dqmRemainder ((sqrt (n : ℝ))⁻¹ • h) x ^ 2 ∂M.dominating := integral_const_mul 4 _ change Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, err n x ^ 2 ∂M.law 0) atTop (𝓝 0) apply squeeze_zero · intro n exact mul_nonneg (Nat.cast_nonneg _) (integral_nonneg fun x => sq_nonneg _) · intro n exact mul_le_mul_of_nonneg_left (hupper n) (Nat.cast_nonneg _) · convert (qmd.scaledDqmRemainder_tendsto h).const_mul 4 using 1 <;> ring
Convolution 1 core · 4 supporting This module derives the scalar Hájek--Le Cam convolution conclusion from LAN, regularity under local alternatives, and a canonical-gradient representation. ★ regular_convolution_limit
Scalar convolution theorem for regular LAN estimators
This module derives the scalar Hájek--Le Cam convolution conclusion from LAN, regularity under local alternatives, and a canonical-gradient representation. It identifies every regular estimator limit as an efficient centered Gaussian law convolved with an independent residual law.
theorem regular_convolution_limit reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
In a finite-dimensional experiment with local asymptotic normality, a scalar estimator regular under each fixed local alternative, and a canonical-gradient representation of its target derivative, the common estimator limit is the efficient centered Gaussian law convolved with a residual probability law.
Formal statement
hypotheses
Ω :
ℕ → Type u_1
H :
Type u_2
K :
E :
LocalExperiment Ω H
centralSequence :
(n : ℕ) → Ω n → H
information :
BilinForm ℝ H
statistic :
(n : ℕ) → Ω n → ℝ
targetDerivative :
H →ₗ[ℝ] ℝ
scoreMap :
H →ₗ[ℝ] K
gradient :
K
limitLaw :
Measure ℝ
scoreLimit :
Measure H
lan :
IsLAN E centralSequence information scoreLimit
regular :
IsRegularEstimator E statistic targetDerivative limitLaw
canonical :
CanonicalGradientPairing information targetDerivative scoreMap gradient
conclusion
∃ residualLaw : Measure ℝ,
conclusion 1
IsProbabilityMeasure residualLaw
conclusion 2
limitLaw = (efficientGaussianLaw gradient).conv residualLaw
Proof (Lean source)
theorem regular_convolution_limit
{K : Type*} [NormedAddCommGroup K] [InnerProductSpace ℝ K]
{E : LocalExperiment Ω H} {centralSequence : (n : ℕ) → Ω n → H}
{information : BilinForm ℝ H}
{statistic : (n : ℕ) → Ω n → ℝ} {targetDerivative : H →ₗ[ℝ] ℝ}
{scoreMap : H →ₗ[ℝ] K} {gradient : K} {limitLaw : Measure ℝ}
{scoreLimit : Measure H}
(lan : IsLAN E centralSequence information scoreLimit)
(regular : IsRegularEstimator E statistic targetDerivative limitLaw)
(canonical : CanonicalGradientPairing information targetDerivative scoreMap gradient) :
∃ residualLaw : Measure ℝ, IsProbabilityMeasure residualLaw ∧
limitLaw = (efficientGaussianLaw gradient).conv residualLaw := by
obtain ⟨jointLaw, joint⟩ := exists_regularLANJointLimit lan regular
exact jointLimit_convolution_factorization lan.gaussian_probability
lan.gaussian_charFun joint canonical
4 supporting declarations (lemmas, instances)
-
lan_tilted_charFun_tendsto_of_jointWeakSubsequencetheorem — Given a LAN experiment, a selected joint weak limit, measurability under its local laws, and normalized likelihood-ratio means, the local-law characteristic functions converge to the corresponding exponentially tilted joint-limit integrals.hypothesesΩ :sharedℕ → Type u_1statistic :(n : ℕ) → Ω n → ℝlimitLaw :Measure ℝscoreLimit :Measure HjointLaw :Measure (ℝ × H)subsequence :ℕ → ℕlan :IsLAN E centralSequence information scoreLimitjoint :JointWeakSubsequence subsequence E.baseLaw statistic centralSequence limitLaw scoreLimit jointLawhlocalMeasurable :∀ n h, AEMeasurable (statistic n) (E.localLaw n h)hnormalized :t :ℝh :HProof (Lean source)
theorem lan_tilted_charFun_tendsto_of_jointWeakSubsequence {E : LocalExperiment Ω H} {centralSequence : (n : ℕ) → Ω n → H} {information : BilinForm ℝ H} {statistic : (n : ℕ) → Ω n → ℝ} {limitLaw : Measure ℝ} {scoreLimit : Measure H} {jointLaw : Measure (ℝ × H)} {subsequence : ℕ → ℕ} (lan : IsLAN E centralSequence information scoreLimit) (joint : JointWeakSubsequence subsequence E.baseLaw statistic centralSequence limitLaw scoreLimit jointLaw) (hlocalMeasurable : ∀ n h, AEMeasurable (statistic n) (E.localLaw n h)) (hnormalized : ∀ h : H, Tendsto (fun n => ∫ ω, exp (E.logLikelihoodRatio n h ω) ∂E.baseLaw n) atTop (𝓝 1)) : ∀ (t : ℝ) (h : H), Tendsto (fun n => ∫ ω, exp ((t * statistic (subsequence n) ω : ℂ) * I) ∂E.localLaw (subsequence n) h) atTop (𝓝 (∫ z, exp ((t * z.1 : ℂ) * I) * exp ((inner ℝ h z.2 - (1 / 2 : ℝ) * information h h : ℝ)) ∂jointLaw)) := by intro t h let Y : (n : ℕ) → Ω (subsequence n) → ℝ × H := fun n ω => (statistic (subsequence n) ω, centralSequence (subsequence n) ω) let a : C(ℝ × H, ℝ) := ⟨fun z => inner ℝ h z.2 - (1 / 2 : ℝ) * information h h, by fun_prop⟩ let f : BoundedContinuousFunction (ℝ × H) ℂ := BoundedContinuousFunction.ofNormedAddCommGroup (fun z => exp ((t * z.1 : ℂ) * I)) (by fun_prop) 1 (fun z => by simp [Complex.norm_exp]) let R : (n : ℕ) → Ω (subsequence n) → ℝ := fun n ω => E.logLikelihoodRatio (subsequence n) h ω - inner ℝ h (centralSequence (subsequence n) ω) + (1 / 2 : ℝ) * information h h have hstatBase (n : ℕ) : AEMeasurable (statistic n) (E.baseLaw n) := by simpa [E.local_zero] using hlocalMeasurable n (0 : H) have hY : WeaklyConverges (fun n => E.baseLaw (subsequence n)) Y jointLaw := by refine ⟨fun n => (hstatBase _).prodMk (lan.central_measurable _), ?_⟩ intro g exact joint.converges g have hR : TendstoInProbability (fun n => E.baseLaw (subsequence n)) R 0 := by intro ε hε exact (lan.expansion h ε hε).comp joint.subsequence_strictMono.tendsto_atTop have hllr (n : ℕ) : AEMeasurable (E.logLikelihoodRatio n h) (E.baseLaw n) := by let r : Ω n → ℝ := fun ω => ((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal have hr : Measurable r := (Measure.measurable_rnDeriv _ _).ennreal_toReal unfold LocalExperiment.logLikelihoodRatio exact (Measurable.ite (hr (measurableSet_singleton 0)) measurable_const hr.log).aemeasurable have hRmeas (n : ℕ) : AEMeasurable (R n) (E.baseLaw (subsequence n)) := by dsimp only [R] have hi : Continuous (fun z : H => inner ℝ h z) := by fun_prop exact ((hllr _).sub (hi.aemeasurable.comp_aemeasurable (lan.central_measurable _))).add aemeasurable_const have hrowIntegrable (n : ℕ) : Integrable (fun ω => exp (E.logLikelihoodRatio n h ω)) (E.baseLaw n) := by letI : IsProbabilityMeasure (E.baseLaw n) := E.base_probability n letI : IsProbabilityMeasure (E.localLaw n h) := E.local_probability n h let r : Ω n → ℝ := fun ω => ((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal have hr_meas : Measurable r := (Measure.measurable_rnDeriv _ _).ennreal_toReal have hr_int : Integrable r (E.baseLaw n) := by simpa only [integrableOn_univ] using (Measure.integrableOn_toReal_rnDeriv (μ := E.localLaw n h) (ν := E.baseLaw n) (s := univ) (measure_ne_top _ _)) apply (hr_int.add (integrable_const (exp (-(n : ℝ))))).mono' (hllr n).exp.aestronglyMeasurable exact ae_of_all _ fun ω => by rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] change exp (E.logLikelihoodRatio n h ω) ≤ r ω + exp (-(n : ℝ)) unfold LocalExperiment.logLikelihoodRatio dsimp only by_cases hz : r ω = 0 · rw [if_pos hz, hz, zero_add] · rw [if_neg hz, Real.exp_log (lt_of_le_of_ne ENNReal.toReal_nonneg (Ne.symm hz))] exact le_add_of_nonneg_right (Real.exp_pos _).le have hv : 0 ≤ information h h := lan.information_nonnegative h have hproj : Measure.map (fun z => inner ℝ h z) scoreLimit = gaussianReal 0 (information h h).toNNReal := by letI : IsProbabilityMeasure scoreLimit := lan.gaussian_probability apply Measure.ext_of_charFun funext s rw [charFun_apply, integral_map (by fun_prop) (by fun_prop)] have heq : (∫ x, exp ((inner ℝ (inner ℝ h x) s : ℂ) * I) ∂scoreLimit) = charFun scoreLimit (s • h) := by rw [charFun_apply] congr with x congr 2 simp [inner_smul_right, real_inner_comm] rw [heq, lan.gaussian_charFun (s • h), charFun_gaussianReal] simp [Real.coe_toNNReal _ hv, map_smul] congr 1 ring have hscoreIntegrable : Integrable (fun y => exp (inner ℝ h y - (1 / 2 : ℝ) * information h h)) scoreLimit := by have hg : Integrable (fun x => exp (x - (1 / 2 : ℝ) * information h h)) (gaussianReal 0 (information h h).toNNReal) := by convert (integrable_exp_mul_gaussianReal (μ := 0) (v := (information h h).toNNReal) 1).mul_const (exp (-(1 / 2 : ℝ) * information h h)) using 1 funext x rw [Real.exp_sub] simp only [one_mul, div_eq_mul_inv] rw [← Real.exp_neg] congr 2 ring rw [← hproj] at hg exact (integrable_map_measure (f := fun y : H => inner ℝ h y) (g := fun x : ℝ => exp (x - (1 / 2 : ℝ) * information h h)) (by fun_prop) (by fun_prop)).mp hg have hlimitIntegrable : Integrable (fun z => exp (a z)) jointLaw := by rw [show (fun z => exp (a z)) = (fun y => exp (inner ℝ h y - (1 / 2 : ℝ) * information h h)) ∘ snd by rfl] have hs := hscoreIntegrable rw [← joint.snd_marginal] at hs exact (integrable_map_measure (f := snd) (g := fun y : H => exp (inner ℝ h y - (1 / 2 : ℝ) * information h h)) (by fun_prop) (by fun_prop)).mp hs have hlimitIntegral : (∫ z, exp (a z) ∂jointLaw) = 1 := by calc (∫ z, exp (a z) ∂jointLaw) = ∫ y, exp (inner ℝ h y - (1 / 2 : ℝ) * information h h) ∂scoreLimit := by rw [← joint.snd_marginal, integral_map (by fun_prop) (by fun_prop)] rfl _ = ∫ x, exp x ∂lanLogLikelihoodLimit information scoreLimit h := by unfold lanLogLikelihoodLimit rw [integral_map (by fun_prop) (by fun_prop)] _ = 1 := integral_exp_lanLogLikelihoodLimit lan.gaussian_probability lan.gaussian_charFun h have hweighted := integral_boundedContinuous_mul_exp_tendsto_of_normalized a f (fun n => E.base_probability (subsequence n)) joint.probability hY hR hRmeas (fun n => by convert hrowIntegrable (subsequence n) using 1 funext ω dsimp only [a, Y, R, ContinuousMap.coe_mk] congr 1 ring) hlimitIntegrable (by rw [hlimitIntegral] convert (hnormalized h).comp joint.subsequence_strictMono.tendsto_atTop using 1 funext n congr 1 with ω dsimp only [a, Y, R, ContinuousMap.coe_mk] congr 1 ring) have hφlocal (n : ℕ) : AEMeasurable (fun ω => exp ((t * statistic n ω : ℂ) * I)) (E.localLaw n h) := by fun_prop have hφbase (n : ℕ) : AEMeasurable (fun ω => exp ((t * statistic n ω : ℂ) * I)) (E.baseLaw n) := by fun_prop have hreplace := (local_integral_sub_exp_logLikelihoodRatio_integral_tendsto_zero (E := E) h (φ := fun n ω => exp ((t * statistic n ω : ℂ) * I)) hφlocal hφbase ⟨1, by positivity, fun n ω => by simp [Complex.norm_exp]⟩ (hnormalized h)).comp joint.subsequence_strictMono.tendsto_atTop convert hreplace.add hweighted using 1 <;> simp [f, Y, a, R] -
lan_tilt_identity_of_jointWeakSubsequencetheorem — Along any joint weak subsequence of the base-law estimator and central sequence, LAN and regularity identify the exponentially tilted characteristic function. This is the scalar Le Cam third-lemma step; in particular, contiguity and control of the unbounded likelihood weight are conclusions of LAN rather than extra assumptions.hypothesesΩ :sharedℕ → Type u_1statistic :(n : ℕ) → Ω n → ℝtargetDerivative :H →ₗ[ℝ] ℝlimitLaw :Measure ℝscoreLimit :Measure HjointLaw :Measure (ℝ × H)subsequence :ℕ → ℕlan :IsLAN E centralSequence information scoreLimitregular :IsRegularEstimator E statistic targetDerivative limitLawjoint :JointWeakSubsequence subsequence E.baseLaw statistic centralSequence limitLaw scoreLimit jointLawt :ℝh :HProof (Lean source)
theorem lan_tilt_identity_of_jointWeakSubsequence {E : LocalExperiment Ω H} {centralSequence : (n : ℕ) → Ω n → H} {information : BilinForm ℝ H} {statistic : (n : ℕ) → Ω n → ℝ} {targetDerivative : H →ₗ[ℝ] ℝ} {limitLaw : Measure ℝ} {scoreLimit : Measure H} {jointLaw : Measure (ℝ × H)} {subsequence : ℕ → ℕ} (lan : IsLAN E centralSequence information scoreLimit) (regular : IsRegularEstimator E statistic targetDerivative limitLaw) (joint : JointWeakSubsequence subsequence E.baseLaw statistic centralSequence limitLaw scoreLimit jointLaw) : ∀ (t : ℝ) (h : H), ∫ z, exp ((t * z.1 : ℂ) * I) * exp ((inner ℝ h z.2 - (1 / 2 : ℝ) * information h h : ℝ)) ∂jointLaw = exp ((t * targetDerivative h : ℂ) * I) * charFun limitLaw t := by intro t h have htilt := lan_tilted_charFun_tendsto_of_jointWeakSubsequence lan joint regular.measurable (fun g => lan_likelihoodRatio_integral_tendsto_one lan g) t h let localPM : ℕ → ProbabilityMeasure ℝ := fun n => ⟨Measure.map (fun ω => statistic n ω - targetDerivative h) (E.localLaw n h), by letI : IsProbabilityMeasure (E.localLaw n h) := E.local_probability n h exact Measure.isProbabilityMeasure_map ((regular.regular h).1 n)⟩ let limitPM : ProbabilityMeasure ℝ := ⟨limitLaw, regular.limit_probability⟩ have hPM : Tendsto localPM atTop (𝓝 limitPM) := by rw [ProbabilityMeasure.tendsto_iff_forall_integral_tendsto] intro g simpa only [localPM, limitPM, ProbabilityMeasure.coe_mk, integral_map ((regular.regular h).1 _) g.continuous.aestronglyMeasurable] using (regular.regular h).2 g let g : BoundedContinuousFunction ℝ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup (fun x => exp ((t * (x + targetDerivative h) : ℂ) * I)) (by fun_prop) 1 (fun x => by simp [Complex.norm_exp]) have hg := (ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto ℂ).mp hPM g have hlocal : Tendsto (fun n => ∫ ω, exp ((t * statistic n ω : ℂ) * I) ∂E.localLaw n h) atTop (𝓝 (exp ((t * targetDerivative h : ℂ) * I) * charFun limitLaw t)) := by convert hg using 1 · funext n rw [show (localPM n : Measure ℝ) = Measure.map (fun ω => statistic n ω - targetDerivative h) (E.localLaw n h) from rfl, integral_map ((regular.regular h).1 n) g.continuous.aestronglyMeasurable] congr 1 with ω simp only [g, BoundedContinuousFunction.coe_ofNormedAddCommGroup] congr 1 push_cast ring · simp only [limitPM, ProbabilityMeasure.coe_mk, g, BoundedContinuousFunction.coe_ofNormedAddCommGroup] rw [charFun_apply, ← integral_const_mul] congr 1 apply integral_congr_ae exact ae_of_all _ fun x => by simp only rw [← Complex.exp_add] congr 1 simp ring exact tendsto_nhds_unique htilt (hlocal.comp joint.subsequence_strictMono.tendsto_atTop) -
exists_regularLANJointLimittheorem — LAN, convergence of the estimator at the base law, and regularity under every fixed local alternative produce a joint subsequential limit satisfying the Gaussian-shift tilt identity. The tightness needed to choose a joint limit follows from the two convergent marginals in finite dimension.hypothesesΩ :sharedℕ → Type u_1statistic :(n : ℕ) → Ω n → ℝtargetDerivative :H →ₗ[ℝ] ℝlimitLaw :Measure ℝscoreLimit :Measure Hlan :regular :IsRegularEstimator E statistic targetDerivative limitLawconclusion∃ jointLaw : Measure (ℝ × H),RegularLANJointLimit information targetDerivative limitLaw scoreLimit jointLawProof (Lean source)
theorem exists_regularLANJointLimit {E : LocalExperiment Ω H} {centralSequence : (n : ℕ) → Ω n → H} {information : BilinForm ℝ H} {statistic : (n : ℕ) → Ω n → ℝ} {targetDerivative : H →ₗ[ℝ] ℝ} {limitLaw : Measure ℝ} {scoreLimit : Measure H} (lan : IsLAN E centralSequence information scoreLimit) (regular : IsRegularEstimator E statistic targetDerivative limitLaw) : ∃ jointLaw : Measure (ℝ × H), RegularLANJointLimit information targetDerivative limitLaw scoreLimit jointLaw := by have hbase : WeaklyConverges E.baseLaw statistic limitLaw := by simpa [E.local_zero] using regular.regular (0 : H) obtain ⟨jointLaw, subsequence, joint⟩ := exists_jointWeakSubsequence E.base_probability regular.limit_probability lan.gaussian_probability hbase lan.central_converges refine ⟨jointLaw, ?_⟩ exact { probability := joint.probability fst_marginal := joint.fst_marginal snd_marginal := joint.snd_marginal tilt_identity := lan_tilt_identity_of_jointWeakSubsequence lan regular joint } -
jointLimit_convolution_factorizationtheorem — The Gaussian-shift tilt identity and a canonical-gradient representer imply that the scalar estimator marginal is the convolution of the efficient centered Gaussian law with a residual probability law. This is the limit-experiment form of the convolution argument.hypothesesH :sharedType u_2K :information :BilinForm ℝ HtargetDerivative :H →ₗ[ℝ] ℝscoreMap :H →ₗ[ℝ] Kgradient :KlimitLaw :Measure ℝscoreLimit :Measure HjointLaw :Measure (ℝ × H)hscoreProb :IsProbabilityMeasure scoreLimitjoint :RegularLANJointLimit information targetDerivative limitLaw scoreLimit jointLawcanonical :CanonicalGradientPairing information targetDerivative scoreMap gradientconclusion∃ residualLaw : Measure ℝ,conclusion 1IsProbabilityMeasure residualLawconclusion 2limitLaw = (efficientGaussianLaw gradient).conv residualLawProof (Lean source)
theorem jointLimit_convolution_factorization {K : Type*} [NormedAddCommGroup K] [InnerProductSpace ℝ K] {information : BilinForm ℝ H} {targetDerivative : H →ₗ[ℝ] ℝ} {scoreMap : H →ₗ[ℝ] K} {gradient : K} {limitLaw : Measure ℝ} {scoreLimit : Measure H} {jointLaw : Measure (ℝ × H)} (hscoreProb : IsProbabilityMeasure scoreLimit) (hscoreChar : ∀ t : H, charFun scoreLimit t = exp (-((information t t : ℂ) / 2))) (joint : RegularLANJointLimit information targetDerivative limitLaw scoreLimit jointLaw) (canonical : CanonicalGradientPairing information targetDerivative scoreMap gradient) : ∃ residualLaw : Measure ℝ, IsProbabilityMeasure residualLaw ∧ limitLaw = (efficientGaussianLaw gradient).conv residualLaw := by rcases canonical.gradient_mem_range with ⟨a, ha⟩ let X : ℝ × H → ℝ := Prod.fst let Y : ℝ × H → ℝ := fun z => inner ℝ a z.2 let v : ℝ := ‖gradient‖ ^ 2 letI : IsProbabilityMeasure scoreLimit := hscoreProb letI : IsProbabilityMeasure jointLaw := joint.probability have hcoord : Measure.map (fun z : H => inner ℝ a z) scoreLimit = efficientGaussianLaw gradient := by apply Measure.ext_of_charFun funext t rw [charFun_apply_real, integral_map (by fun_prop) (by fun_prop)] have heq : (∫ x : H, exp ((t * inner ℝ a x : ℂ) * I) ∂scoreLimit) = charFun scoreLimit (t • a) := by rw [charFun_apply] congr 1 funext x congr 1 norm_cast rw [real_inner_comm, inner_smul_right] rw [heq, hscoreChar] unfold efficientGaussianLaw rw [ProbabilityTheory.charFun_gaussianReal] rw [canonical.information_eq_inner] simp [ha, norm_smul, Real.norm_eq_abs] congr 1 norm_cast rw [mul_pow, sq_abs] ring have hYmap : Measure.map Y jointLaw = efficientGaussianLaw gradient := by calc Measure.map Y jointLaw = Measure.map (fun z : H => inner ℝ a z) (Measure.map snd jointLaw) := by rw [Measure.map_map (by fun_prop) (by fun_prop)] rfl _ = Measure.map (fun z : H => inner ℝ a z) scoreLimit := by rw [joint.snd_marginal] _ = efficientGaussianLaw gradient := hcoord have hexp (q : ℝ) : Integrable (fun z => exp (q * Y z)) jointLaw := by have h := ProbabilityTheory.integrable_exp_mul_gaussianReal (μ := 0) (v := (‖gradient‖ ^ 2).toNNReal) q change Integrable (fun x => exp (q * x)) (efficientGaussianLaw gradient) at h rw [← hYmap] at h exact h.comp_aemeasurable (by fun_prop) let F : ℝ → ℂ → ℂ := fun t z => ∫ w, exp ((t * X w : ℂ) * I) * exp (z * Y w) ∂jointLaw have hFanalytic (t : ℝ) : AnalyticOnNhd ℂ (F t) univ := by exact analyticOnNhd_weightedExp X Y (by fun_prop) (by fun_prop) hexp t have hreal (t q : ℝ) : F t q = exp ((v / 2 : ℂ) * (q : ℂ) ^ 2 + ((t * v : ℂ) * I) * q) * charFun limitLaw t := by have ht := joint.tilt_identity t (q • a) rw [canonical.information_eq_inner, canonical.derivative_eq_inner] at ht simp [ha, inner_smul_left, inner_smul_right] at ht have hqnorm : ‖q • gradient‖ ^ 2 = q ^ 2 * v := by simp [v, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs] have hqnormc : (‖q • gradient‖ ^ 2 : ℂ) = ((q ^ 2 * v : ℝ) : ℂ) := by exact_mod_cast hqnorm rw [hqnormc] at ht simp_rw [Complex.exp_sub] at ht have hc : exp ((2 : ℂ)⁻¹ * ((q ^ 2 * v : ℝ) : ℂ)) = exp (((q ^ 2 * v : ℝ) : ℂ) / 2) := by congr 1 ring rw [hc] at ht simp only [div_eq_mul_inv, mul_assoc] at ht have ht' : (∫ z : ℝ × H, exp ((t * z.1 : ℂ) * I) * exp ((q : ℂ) * inner ℝ a z.2) ∂jointLaw) * (exp (((q ^ 2 * v : ℝ) : ℂ) * (2 : ℂ)⁻¹))⁻¹ = exp ((t * (q * ‖gradient‖ ^ 2) : ℂ) * I) * charFun limitLaw t := by rw [← integral_mul_const] simpa only [mul_assoc] using ht dsimp [F, X, Y] calc (∫ w : ℝ × H, exp ((t * w.1 : ℂ) * I) * exp ((q : ℂ) * inner ℝ a w.2) ∂jointLaw) = ((∫ w : ℝ × H, exp ((t * w.1 : ℂ) * I) * exp ((q : ℂ) * inner ℝ a w.2) ∂jointLaw) * (exp (((q ^ 2 * v : ℝ) : ℂ) * (2 : ℂ)⁻¹))⁻¹) * exp (((q ^ 2 * v : ℝ) : ℂ) * (2 : ℂ)⁻¹) := by rw [mul_assoc, inv_mul_cancel₀ (Complex.exp_ne_zero _), mul_one] _ = (exp ((t * (q * ‖gradient‖ ^ 2) : ℂ) * I) * charFun limitLaw t) * exp (((q ^ 2 * v : ℝ) : ℂ) * (2 : ℂ)⁻¹) := by rw [ht'] _ = (exp (((q ^ 2 * v : ℝ) : ℂ) * (2 : ℂ)⁻¹) * exp ((t * (q * ‖gradient‖ ^ 2) : ℂ) * I)) * charFun limitLaw t := by ring _ = exp (((q ^ 2 * v : ℝ) : ℂ) * (2 : ℂ)⁻¹ + (t * (q * ‖gradient‖ ^ 2) : ℂ) * I) * charFun limitLaw t := by rw [Complex.exp_add] _ = exp ((v / 2 : ℂ) * (q : ℂ) ^ 2 + ((t * v : ℂ) * I) * q) * charFun limitLaw t := by congr 2 push_cast simp [v] ring have hcomplex (t : ℝ) (z : ℂ) : F t z = exp ((v / 2 : ℂ) * z ^ 2 + ((t * v : ℂ) * I) * z) * charFun limitLaw t := weightedExp_eq_of_eq_real (F t) v t (charFun limitLaw t) (hFanalytic t) (hreal t) z let R : ℝ × H → ℝ := fun w => X w - Y w let residualLaw : Measure ℝ := Measure.map R jointLaw have hRchar (t : ℝ) : charFun residualLaw t = exp ((v / 2 : ℂ) * (t : ℂ) ^ 2) * charFun limitLaw t := by rw [charFun_apply_real, integral_map (by fun_prop) (by fun_prop)] have hc := hcomplex t ((-t : ℂ) * I) dsimp [F, R, residualLaw, X, Y] at hc ⊢ convert hc using 1 · apply integral_congr_ae filter_upwards with w rw [← Complex.exp_add] congr 1 push_cast ring · congr 1 ring_nf rw [Complex.I_sq] ring have hfactor (s t : ℝ) : (∫ w, exp (((s * Y w + t * R w : ℝ) : ℂ) * I) ∂jointLaw) = charFun (Measure.map Y jointLaw) s * charFun residualLaw t := by have hc := hcomplex t (((s - t : ℝ) : ℂ) * I) rw [hYmap] unfold efficientGaussianLaw rw [ProbabilityTheory.charFun_gaussianReal, hRchar] dsimp [F, R, X, Y] at hc ⊢ convert hc using 1 · apply integral_congr_ae filter_upwards with w rw [← Complex.exp_add] congr 1 push_cast ring · simp [v] rw [← mul_assoc, ← Complex.exp_add] congr 2 ring_nf rw [Complex.I_sq] ring have hIndep : IndepFun Y R jointLaw := by rw [indepFun_iff_charFun_prod (by fun_prop) (by fun_prop)] intro p rw [charFun_apply, integral_map (by fun_prop) (by fun_prop)] simpa [WithLp.prod_inner_apply] using hfactor p.ofLp.1 p.ofLp.2 have hresidualProb : IsProbabilityMeasure residualLaw := by dsimp [residualLaw] exact Measure.isProbabilityMeasure_map (by fun_prop) refine ⟨residualLaw, hresidualProb, ?_⟩ have hadd := hIndep.map_add_eq_map_conv_map (by fun_prop) (by fun_prop) calc limitLaw = Measure.map X jointLaw := by simpa [X] using joint.fst_marginal.symm _ = Measure.map (Y + R) jointLaw := by congr 1 funext w simp [R] _ = Measure.map Y jointLaw ∗ Measure.map R jointLaw := hadd _ = efficientGaussianLaw gradient ∗ residualLaw := by rw [hYmap]
ExponentialTilt 1 core · 0 supporting 1 to review This module provides the uniform-integrability core of Le Cam's third lemma. ★ integral_boundedContinuous_mul_exp_tendsto_of_normalized
Exponentially tilted weak limits
This module provides the uniform-integrability core of Le Cam's third lemma. It turns joint weak convergence plus a negligible log-weight remainder and convergence of exponential means into convergence of bounded observables under exponential tilting.
theorem integral_boundedContinuous_mul_exp_tendsto_of_normalized unreviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
Given probability laws in every row and in the limit, joint weak convergence, a negligible additive remainder, its measurability, row integrability of the exponential weights, integrability of the limiting weight, and normalization of their expectations, bounded complex observables converge under exponential tilting.
Formal statement
hypotheses
Ω :
ℕ → Type u_1
S :
P :
(n : ℕ) → Measure (Ω n)
Y :
(n : ℕ) → Ω n → S
Q :
Measure S
R :
(n : ℕ) → Ω n → ℝ
a :
C(S, ℝ)
f :
hP :
∀ n, IsProbabilityMeasure (P n)
hQ :
hY :
WeaklyConverges P Y Q
hR :
TendstoInProbability P R 0
hRmeas :
∀ n, AEMeasurable (R n) (P n)
hweight :
∀ n, Integrable (fun ω => exp (a (Y n ω) + R n ω)) (P n)
hlimitWeight :
Integrable (fun y => exp (a y)) Q
Proof (Lean source)
theorem integral_boundedContinuous_mul_exp_tendsto_of_normalized
{S : Type*} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S]
[MeasurableSpace S] [BorelSpace S]
{P : (n : ℕ) → Measure (Ω n)} {Y : (n : ℕ) → Ω n → S} {Q : Measure S}
{R : (n : ℕ) → Ω n → ℝ} (a : C(S, ℝ)) (f : BoundedContinuousFunction S ℂ)
(hP : ∀ n, IsProbabilityMeasure (P n)) (hQ : IsProbabilityMeasure Q)
(hY : WeaklyConverges P Y Q)
(hR : TendstoInProbability P R 0)
(hRmeas : ∀ n, AEMeasurable (R n) (P n))
(hweight : ∀ n, Integrable (fun ω => exp (a (Y n ω) + R n ω)) (P n))
(hlimitWeight : Integrable (fun y => exp (a y)) Q)
(hnormalized : Tendsto
(fun n => ∫ ω, exp (a (Y n ω) + R n ω) ∂P n)
atTop (𝓝 (∫ y, exp (a y) ∂Q))) :
Tendsto (fun n => ∫ ω,
f (Y n ω) * (exp (a (Y n ω) + R n ω) : ℂ) ∂P n) atTop
(𝓝 (∫ y, f y * (exp (a y) : ℂ) ∂Q)) := by
let b : S → S × ℝ := fun y => (y, a y)
have hb : Continuous b := by fun_prop
have hbase : WeaklyConverges P (fun n ω => b (Y n ω)) (Measure.map b Q) := by
refine ⟨fun n => hb.aemeasurable.comp_aemeasurable (hY.1 n), ?_⟩
intro g
have hg := hY.2 (g.compContinuous ⟨b, hb⟩)
simpa only [BoundedContinuousFunction.compContinuous_apply, ContinuousMap.coe_mk,
Function.comp_apply, integral_map hb.aemeasurable
g.continuous.aestronglyMeasurable] using hg
have hQb : IsProbabilityMeasure (Measure.map b Q) :=
Measure.isProbabilityMeasure_map hb.aemeasurable
let V : (n : ℕ) → Ω n → S × ℝ := fun n ω => (0, R n ω)
have hVmeas (n : ℕ) : AEMeasurable (V n) (P n) :=
aemeasurable_const.prodMk (hRmeas n)
have hVprob : ∀ ε : ℝ, 0 < ε →
Tendsto (fun n => P n {ω | ε ≤ ‖V n ω‖}) atTop (𝓝 0) := by
intro ε hε
convert hR ε hε using 1 with n ω
simp [V, Real.norm_eq_abs]
have hpair0 := weaklyConverges_add_tendstoInProbability_norm
(E := S × ℝ) hP hQb hbase hVprob hVmeas
have hpair : WeaklyConverges P
(fun n ω => (Y n ω, a (Y n ω) + R n ω)) (Measure.map b Q) := by
simpa [b, V] using hpair0
let pairPM : ℕ → ProbabilityMeasure (S × ℝ) := fun n =>
⟨Measure.map (fun ω => (Y n ω, a (Y n ω) + R n ω)) (P n),
Measure.isProbabilityMeasure_map (hpair.1 n)⟩
let limitPM : ProbabilityMeasure (S × ℝ) := ⟨Measure.map b Q, hQb⟩
have hpairPM : Tendsto pairPM atTop (𝓝 limitPM) := by
rw [ProbabilityMeasure.tendsto_iff_forall_integral_tendsto]
intro g
simpa only [pairPM, limitPM, ProbabilityMeasure.coe_mk,
integral_map (hpair.1 _) g.continuous.aestronglyMeasurable] using hpair.2 g
have hpairPM_complex :=
(ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto ℂ).mp hpairPM
let truncWeight (K : ℕ) : S × ℝ → ℝ := fun z => min (exp z.2) K
have htruncWeight_cont (K : ℕ) : Continuous (truncWeight K) := by
fun_prop
have htruncWeight_nonneg (K : ℕ) (z : S × ℝ) : 0 ≤ truncWeight K z := by
exact le_min (Real.exp_pos _).le (Nat.cast_nonneg K)
have htruncWeight_le (K : ℕ) (z : S × ℝ) : truncWeight K z ≤ K :=
min_le_right _ _
let truncComplex (K : ℕ) : BoundedContinuousFunction (S × ℝ) ℂ :=
BoundedContinuousFunction.ofNormedAddCommGroup
(fun z => f z.1 * (truncWeight K z : ℂ))
(by fun_prop) (‖f‖ * K) (fun z => by
rw [norm_mul, Complex.norm_real, Real.norm_eq_abs,
abs_of_nonneg (htruncWeight_nonneg K z)]
exact mul_le_mul (f.norm_coe_le_norm z.1) (htruncWeight_le K z)
(htruncWeight_nonneg K z) (norm_nonneg f))
have htrunc (K : ℕ) : Tendsto (fun n => ∫ ω,
f (Y n ω) * (truncWeight K (Y n ω, a (Y n ω) + R n ω) : ℂ) ∂P n)
atTop (𝓝 (∫ y, f y * (truncWeight K (y, a y) : ℂ) ∂Q)) := by
have ht := hpairPM_complex (truncComplex K)
change Tendsto (fun n => ∫ z, truncComplex K z ∂(pairPM n : Measure (S × ℝ)))
atTop (𝓝 (∫ z, truncComplex K z ∂(limitPM : Measure (S × ℝ)))) at ht
convert ht using 1
· funext n
rw [show (pairPM n : Measure (S × ℝ)) =
Measure.map (fun ω => (Y n ω, a (Y n ω) + R n ω)) (P n) from rfl,
integral_map (hpair.1 n) (truncComplex K).continuous.aestronglyMeasurable]
rfl
· rw [show (limitPM : Measure (S × ℝ)) = Measure.map b Q from rfl,
integral_map hb.aemeasurable (truncComplex K).continuous.aestronglyMeasurable]
rfl
let truncReal (K : ℕ) : BoundedContinuousFunction (S × ℝ) ℝ :=
BoundedContinuousFunction.ofNormedAddCommGroup (truncWeight K)
(htruncWeight_cont K) K (fun z => by
rw [Real.norm_eq_abs, abs_of_nonneg (htruncWeight_nonneg K z)]
exact htruncWeight_le K z)
have htruncMean (K : ℕ) : Tendsto (fun n => ∫ ω,
truncWeight K (Y n ω, a (Y n ω) + R n ω) ∂P n) atTop
(𝓝 (∫ y, truncWeight K (y, a y) ∂Q)) := by
have ht := hpair.2 (truncReal K)
convert ht using 1
· rfl
· rw [integral_map hb.aemeasurable (truncReal K).continuous.aestronglyMeasurable]
rfl
have hlimitTrunc : Tendsto (fun K : ℕ => ∫ y, truncWeight K (y, a y) ∂Q)
atTop (𝓝 (∫ y, exp (a y) ∂Q)) := by
apply tendsto_integral_filter_of_dominated_convergence (fun y => exp (a y))
· exact Filter.Eventually.of_forall fun K =>
(htruncWeight_cont K).aestronglyMeasurable.comp_aemeasurable hb.aemeasurable
· refine Filter.Eventually.of_forall fun K => ae_of_all Q fun y => ?_
rw [Real.norm_eq_abs, abs_of_nonneg (htruncWeight_nonneg K (y, a y))]
exact min_le_left _ _
· exact hlimitWeight
· refine ae_of_all Q fun y => tendsto_const_nhds.congr' ?_
filter_upwards
[(tendsto_natCast_atTop_atTop.eventually_gt_atTop (exp (a y)))] with K hK
exact (min_eq_left hK.le).symm
have htruncRowInt (n K : ℕ) : Integrable
(fun ω => truncWeight K (Y n ω, a (Y n ω) + R n ω)) (P n) := by
apply (hweight n).mono'
· exact (htruncWeight_cont K).aestronglyMeasurable.comp_aemeasurable (hpair.1 n)
· refine ae_of_all _ fun ω => ?_
rw [Real.norm_eq_abs, abs_of_nonneg (htruncWeight_nonneg K _)]
exact min_le_left _ _
have htruncLimitInt (K : ℕ) : Integrable
(fun y => truncWeight K (y, a y)) Q := by
apply hlimitWeight.mono'
· exact (htruncWeight_cont K).aestronglyMeasurable.comp_aemeasurable hb.aemeasurable
· refine ae_of_all _ fun y => ?_
rw [Real.norm_eq_abs, abs_of_nonneg (htruncWeight_nonneg K _)]
exact min_le_left _ _
have hfullRowInt (n : ℕ) : Integrable
(fun ω => f (Y n ω) * (exp (a (Y n ω) + R n ω) : ℂ)) (P n) := by
exact (hweight n).ofReal.bdd_mul
(f.continuous.aestronglyMeasurable.comp_aemeasurable (hY.1 n))
(ae_of_all _ fun ω => f.norm_coe_le_norm (Y n ω))
have hfullLimitInt : Integrable
(fun y => f y * (exp (a y) : ℂ)) Q := by
exact hlimitWeight.ofReal.bdd_mul f.continuous.aestronglyMeasurable
(ae_of_all _ fun y => f.norm_coe_le_norm y)
have htruncRowComplexInt (n K : ℕ) : Integrable
(fun ω => f (Y n ω) *
(truncWeight K (Y n ω, a (Y n ω) + R n ω) : ℂ)) (P n) := by
exact (htruncRowInt n K).ofReal.bdd_mul
(f.continuous.aestronglyMeasurable.comp_aemeasurable (hY.1 n))
(ae_of_all _ fun ω => f.norm_coe_le_norm (Y n ω))
have htruncLimitComplexInt (K : ℕ) : Integrable
(fun y => f y * (truncWeight K (y, a y) : ℂ)) Q := by
exact (htruncLimitInt K).ofReal.bdd_mul f.continuous.aestronglyMeasurable
(ae_of_all _ fun y => f.norm_coe_le_norm y)
have htailRow (n K : ℕ) :
‖(∫ ω, f (Y n ω) * (exp (a (Y n ω) + R n ω) : ℂ) ∂P n) -
∫ ω, f (Y n ω) *
(truncWeight K (Y n ω, a (Y n ω) + R n ω) : ℂ) ∂P n‖ ≤
‖f‖ * ((∫ ω, exp (a (Y n ω) + R n ω) ∂P n) -
∫ ω, truncWeight K (Y n ω, a (Y n ω) + R n ω) ∂P n) := by
rw [← integral_sub (hfullRowInt n) (htruncRowComplexInt n K)]
calc
‖∫ ω, f (Y n ω) * (exp (a (Y n ω) + R n ω) : ℂ) -
f (Y n ω) *
(truncWeight K (Y n ω, a (Y n ω) + R n ω) : ℂ) ∂P n‖
≤ ∫ ω, ‖f (Y n ω) * (exp (a (Y n ω) + R n ω) : ℂ) -
f (Y n ω) *
(truncWeight K (Y n ω, a (Y n ω) + R n ω) : ℂ)‖ ∂P n :=
norm_integral_le_integral_norm _
_ ≤ ∫ ω, ‖f‖ * (exp (a (Y n ω) + R n ω) -
truncWeight K (Y n ω, a (Y n ω) + R n ω)) ∂P n := by
apply integral_mono (hfullRowInt n |>.sub (htruncRowComplexInt n K) |>.norm)
((hweight n).sub (htruncRowInt n K) |>.const_mul ‖f‖)
intro ω
have hd : 0 ≤ exp (a (Y n ω) + R n ω) -
truncWeight K (Y n ω, a (Y n ω) + R n ω) :=
sub_nonneg.mpr (min_le_left _ _)
calc
‖f (Y n ω) * (exp (a (Y n ω) + R n ω) : ℂ) -
f (Y n ω) *
(truncWeight K (Y n ω, a (Y n ω) + R n ω) : ℂ)‖ =
‖f (Y n ω)‖ * (exp (a (Y n ω) + R n ω) -
truncWeight K (Y n ω, a (Y n ω) + R n ω)) := by
rw [← mul_sub, ← Complex.ofReal_sub, norm_mul, Complex.norm_real,
Real.norm_eq_abs, abs_of_nonneg hd]
_ ≤ _ := mul_le_mul_of_nonneg_right (f.norm_coe_le_norm _) hd
_ = _ := by
rw [integral_const_mul, integral_sub (hweight n) (htruncRowInt n K)]
have htailLimit (K : ℕ) :
‖(∫ y, f y * (exp (a y) : ℂ) ∂Q) -
∫ y, f y * (truncWeight K (y, a y) : ℂ) ∂Q‖ ≤
‖f‖ * ((∫ y, exp (a y) ∂Q) -
∫ y, truncWeight K (y, a y) ∂Q) := by
rw [← integral_sub hfullLimitInt (htruncLimitComplexInt K)]
calc
‖∫ y, f y * (exp (a y) : ℂ) -
f y * (truncWeight K (y, a y) : ℂ) ∂Q‖
≤ ∫ y, ‖f y * (exp (a y) : ℂ) -
f y * (truncWeight K (y, a y) : ℂ)‖ ∂Q :=
norm_integral_le_integral_norm _
_ ≤ ∫ y, ‖f‖ * (exp (a y) - truncWeight K (y, a y)) ∂Q := by
apply integral_mono (hfullLimitInt.sub (htruncLimitComplexInt K)).norm
(hlimitWeight.sub (htruncLimitInt K) |>.const_mul ‖f‖)
intro y
have hd : 0 ≤ exp (a y) - truncWeight K (y, a y) :=
sub_nonneg.mpr (min_le_left _ _)
calc
‖f y * (exp (a y) : ℂ) -
f y * (truncWeight K (y, a y) : ℂ)‖ =
‖f y‖ * (exp (a y) - truncWeight K (y, a y)) := by
rw [← mul_sub, ← Complex.ofReal_sub, norm_mul, Complex.norm_real,
Real.norm_eq_abs, abs_of_nonneg hd]
_ ≤ _ := mul_le_mul_of_nonneg_right (f.norm_coe_le_norm _) hd
_ = _ := by
rw [integral_const_mul, integral_sub hlimitWeight (htruncLimitInt K)]
by_cases hfzero : ‖f‖ = 0
· have : f = 0 := norm_eq_zero.mp hfzero
subst f
simp
have hfpos : 0 < ‖f‖ := lt_of_le_of_ne (norm_nonneg f) (Ne.symm hfzero)
rw [Metric.tendsto_nhds]
intro ε hε
have hD : Tendsto (fun K : ℕ =>
(∫ y, exp (a y) ∂Q) - ∫ y, truncWeight K (y, a y) ∂Q)
atTop (𝓝 0) := by
have hc : Tendsto (fun _ : ℕ => ∫ y, exp (a y) ∂Q) atTop
(𝓝 (∫ y, exp (a y) ∂Q)) := tendsto_const_nhds
simpa using hc.sub hlimitTrunc
have hsmall : 0 < ε / (6 * ‖f‖) := by positivity
have hDev : ∀ᶠ K : ℕ in atTop,
dist ((∫ y, exp (a y) ∂Q) - ∫ y, truncWeight K (y, a y) ∂Q) 0 <
ε / (6 * ‖f‖) :=
(Metric.tendsto_nhds.mp hD) _ hsmall
obtain ⟨K, hKdist⟩ := hDev.exists
have hDnonneg : 0 ≤ (∫ y, exp (a y) ∂Q) -
∫ y, truncWeight K (y, a y) ∂Q := by
rw [sub_nonneg]
exact integral_mono (htruncLimitInt K) hlimitWeight fun y => min_le_left _ _
have hKsmall : (∫ y, exp (a y) ∂Q) -
∫ y, truncWeight K (y, a y) ∂Q < ε / (6 * ‖f‖) := by
simpa [Real.dist_eq, abs_of_nonneg hDnonneg] using hKdist
have hrowMean : Tendsto (fun n =>
(∫ ω, exp (a (Y n ω) + R n ω) ∂P n) -
∫ ω, truncWeight K (Y n ω, a (Y n ω) + R n ω) ∂P n)
atTop (𝓝 ((∫ y, exp (a y) ∂Q) -
∫ y, truncWeight K (y, a y) ∂Q)) :=
hnormalized.sub (htruncMean K)
have hcut : (∫ y, exp (a y) ∂Q) -
∫ y, truncWeight K (y, a y) ∂Q < ε / (3 * ‖f‖) := by
exact hKsmall.trans (by
apply div_lt_div_of_pos_left hε (by positivity)
nlinarith [hfpos])
have hrowEv : ∀ᶠ n in atTop,
(∫ ω, exp (a (Y n ω) + R n ω) ∂P n) -
∫ ω, truncWeight K (Y n ω, a (Y n ω) + R n ω) ∂P n <
ε / (3 * ‖f‖) :=
hrowMean.eventually_lt_const hcut
have htruncEv : ∀ᶠ n in atTop,
dist (∫ ω, f (Y n ω) *
(truncWeight K (Y n ω, a (Y n ω) + R n ω) : ℂ) ∂P n)
(∫ y, f y * (truncWeight K (y, a y) : ℂ) ∂Q) < ε / 3 :=
(Metric.tendsto_nhds.mp (htrunc K)) _ (by positivity)
-- … truncated; follow the source link for the rest …
IIDDQMLAN 1 core · 3 supporting This module completes the product-likelihood and triangular-array argument that turns the dominated i.i.d. ★ iidDQM_implies_LAN
LAN expansion for i.i.d. DQM models
This module completes the product-likelihood and triangular-array argument that turns the dominated i.i.d. quadratic-mean differentiability interface into local asymptotic normality. It supplies the score central-limit step, the log-likelihood expansion, and the reusable LAN theorem.
theorem iidDQM_implies_LAN reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution.IIDQuadraticMeanDifferentiable
A quadratic-mean differentiable dominated finite-dimensional i.i.d. model is locally asymptotically normal at its base parameter, with normalized score-sum central sequence and score-second-moment information form.
Formal statement
hypotheses
conclusion
IsLAN (localExperiment M) qmd.centralSequence (qmd.information M) (gaussianLimit qmd.score_measurable qmd.score_squareIntegrable)
Proof (Lean source)
theorem iidDQM_implies_LAN (qmd : IIDQuadraticMeanDifferentiable M) :
IsLAN (localExperiment M) qmd.centralSequence (qmd.information M)
(gaussianLimit qmd.score_measurable qmd.score_squareIntegrable) := by
rcases qmd.information_isSymm_nonnegative with ⟨hsymm, hnonneg⟩
refine
{ central_measurable := qmd.centralSequence_weaklyConverges.1
information_symmetric := hsymm
information_nonnegative := hnonneg
gaussian_probability := inferInstance
gaussian_charFun := fun t => ?_
central_converges := qmd.centralSequence_weaklyConverges
expansion := qmd.iid_logLikelihoodRatio_expansion }
rw [gaussianLimit_charFun]
congr 2
rw [qmd.information_apply]
simp only [pow_two]
ring
3 supporting declarations (lemmas, instances)
-
iid_logLikelihoodRatio_taylortheorem — The triangular-array likelihood Taylor lemma: product-density factorization, the DQM L² increment approximation, and the vanishing singular mass imply the quadratic LAN expansion of the guarded log likelihood ratio.hypothesesX :sharedType u_1qmd :h :Hhincrement :conclusionTendstoInProbability (fun n => M.iidLaw 0 n) (fun n x => (localExperiment M).logLikelihoodRatio n h x - inner ℝ h (qmd.centralSequence n x) + (1 / 2 : ℝ) * qmd.information M h h) 0Proof (Lean source)
theorem iid_logLikelihoodRatio_taylor (qmd : IIDQuadraticMeanDifferentiable M) (h : H) (hincrement : Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, (qmd.sqrtLikelihoodIncrement n h x - (sqrt (n : ℝ))⁻¹ * inner ℝ h (qmd.score x)) ^ 2 ∂M.law 0) atTop (𝓝 0)) (hsingular : Tendsto (fun n : ℕ => (n : ℝ) * (M.law ((sqrt (n : ℝ))⁻¹ • h) {x | M.sqrtDensity 0 x = 0}).toReal) atTop (𝓝 0)) : TendstoInProbability (fun n => M.iidLaw 0 n) (fun n x => (localExperiment M).logLikelihoodRatio n h x - inner ℝ h (qmd.centralSequence n x) + (1 / 2 : ℝ) * qmd.information M h h) 0 := by -- Use `iidLaw_rnDeriv_eq_prod`; expand each `2 * log (1 + W/2)`; show the -- maximum increment vanishes, replace the linear sum by the score sum, and apply the -- weak law to the quadratic sum. The three preceding lemmas isolate these steps. have hmoments := qmd.sqrtLikelihoodIncrement_moments h hincrement hsingular obtain ⟨hlinear, hquadratic, hmax⟩ := qmd.iid_sqrtLikelihoodIncrement_array_limits h hincrement hmoments have htaylor := qmd.iid_guardedLogLikelihood_taylor_remainder h hlinear hquadratic hmax let P := fun n => M.iidLaw 0 n let T : ∀ n, (Fin n → X) → ℝ := fun n x => (localExperiment M).logLikelihoodRatio n h x - (∑ i, qmd.sqrtLikelihoodIncrement n h (x i)) + (1 / 4 : ℝ) * ∑ i, qmd.sqrtLikelihoodIncrement n h (x i) ^ 2 let L : ∀ n, (Fin n → X) → ℝ := fun n x => (∑ i, qmd.sqrtLikelihoodIncrement n h (x i)) - inner ℝ h (qmd.centralSequence n x) + (1 / 4 : ℝ) * qmd.information M h h let Q : ∀ n, (Fin n → X) → ℝ := fun n x => (∑ i, qmd.sqrtLikelihoodIncrement n h (x i) ^ 2) - qmd.information M h h have hTL : TendstoInProbability P (fun n x => T n x + L n x) 0 := tendstoInProbability_add_zero P T L (by simpa [P, T] using htaylor) (by simpa [P, L] using hlinear) have hQ : TendstoInProbability P (fun n x => -(1 / 4 : ℝ) * Q n x) 0 := tendstoInProbability_const_mul_zero P (-(1 / 4 : ℝ)) Q (by simpa [P, Q] using hquadratic) have hall := tendstoInProbability_add_zero P (fun n x => T n x + L n x) (fun n x => -(1 / 4 : ℝ) * Q n x) hTL hQ unfold TendstoInProbability at hall ⊢ intro ε hε exact (hall ε hε).congr' (Filter.Eventually.of_forall fun n => by congr 1 ext x simp only [Set.mem_ofPred_eq, sub_zero] simp only [T, L, Q] ring) -
centralSequence_weaklyConvergestheorem — Under the base product laws, the normalized i.i.d. score sums converge weakly to the centered Gaussian law whose covariance is the score second moment.hypothesesconclusionWeaklyConverges (fun n => M.iidLaw 0 n) qmd.centralSequence (gaussianLimit qmd.score_measurable qmd.score_squareIntegrable)Proof (Lean source)
theorem centralSequence_weaklyConverges (qmd : IIDQuadraticMeanDifferentiable M) : WeaklyConverges (fun n => M.iidLaw 0 n) qmd.centralSequence (gaussianLimit qmd.score_measurable qmd.score_squareIntegrable) := by -- Use coordinate projections on `(Fin n → X, Measure.pi ...)` as the canonical IID sample, -- then apply `IIDSample.clt_normalizedSum_vec` and unfold the bounded-test-function form. constructor · intro n unfold centralSequence exact ((measurable_sum _ fun i _ => qmd.score_measurable.comp (measurable_pi_apply i)).const_smul _).aemeasurable · let P : Measure X := M.law 0 let _ : IsProbabilityMeasure P := M.probability 0 let μ : Measure (ℕ → X) := Measure.infinitePi (fun _ : ℕ => P) let S : IIDSample (ℕ → X) X μ P := { Z i ω := ω i meas i := measurable_pi_apply i indep := ProbabilityTheory.iIndepFun_infinitePi (X := fun _ x => x) (by fun_prop) identDist i := ⟨(measurable_pi_apply 0).aemeasurable, (measurable_pi_apply i).aemeasurable, by simp only [μ, Measure.infinitePi_map_eval]⟩ law := by simp only [μ, Measure.infinitePi_map_eval] } have hclt := S.clt_normalizedSum_vec qmd.score_measurable qmd.score_squareIntegrable qmd.score_integral_eq_zero unfold Tendsto_dist_vec at hclt intro f have ht := (ProbabilityMeasure.tendsto_iff_forall_integral_tendsto.mp hclt) f simp only [ProbabilityMeasure.coe_mk] at ht have hsum_meas : ∀ n, AEMeasurable (normalizedSum S qmd.score (fun m => range m) n) μ := by intro n unfold normalizedSum exact ((measurable_sum _ fun i _ => qmd.score_measurable.comp (S.meas i)).const_smul _).aemeasurable simp_rw [integral_map (hsum_meas _) f.continuous.aestronglyMeasurable] at ht convert ht using 1 funext n let proj : (ℕ → X) → (Fin n → X) := fun ω i => ω i have hproj_meas : Measurable proj := by unfold proj exact measurable_pi_lambda _ fun i => measurable_pi_apply (i : ℕ) have hproj : μ.map proj = M.iidLaw 0 n := by change (Measure.infinitePi (fun _ : ℕ => P)).map (fun (ω : ℕ → X) (i : Fin n) => ω (i : ℕ)) = Measure.pi (fun _ : Fin n => M.law 0) rw [Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective, Measure.infinitePi_eq_pi] change (∫ ω, f (qmd.centralSequence n ω) ∂M.iidLaw 0 n) = _ rw [← hproj, integral_map hproj_meas.aemeasurable] · apply integral_congr_ae filter_upwards [] with ω congr 2 simp only [centralSequence, proj, normalizedSum, S, Finset.card_range] exact congrArg (fun z : H => (sqrt (n : ℝ))⁻¹ • z) (Fin.sum_univ_eq_sum_range (fun i => qmd.score (ω i)) n) · apply (f.continuous.measurable.comp _).aestronglyMeasurable unfold centralSequence exact (measurable_sum _ fun i _ => qmd.score_measurable.comp (measurable_pi_apply i)).const_smul _ -
iid_logLikelihoodRatio_expansiontheorem — The generalized Radon--Nikodym log likelihood ratio of the finite product experiment admits the DQM quadratic expansion: normalized score sum minus half the Fisher-information quadratic form, with a remainder vanishing in base-law probability.hypothesesX :sharedType u_1qmd :h :HconclusionTendstoInProbability (fun n => M.iidLaw 0 n) (fun n x => (localExperiment M).logLikelihoodRatio n h x - inner ℝ h (qmd.centralSequence n x) + (1 / 2 : ℝ) * qmd.information M h h) 0Proof (Lean source)
theorem iid_logLikelihoodRatio_expansion (qmd : IIDQuadraticMeanDifferentiable M) (h : H) : TendstoInProbability (fun n => M.iidLaw 0 n) (fun n x => (localExperiment M).logLikelihoodRatio n h x - inner ℝ h (qmd.centralSequence n x) + (1 / 2 : ℝ) * qmd.information M h h) 0 := by exact iid_logLikelihoodRatio_taylor qmd h (sqrtLikelihoodIncrement_L2 qmd h) (local_zeroBaseDensity_mass qmd h)
LikelihoodNormalization 1 core · 1 supporting This module isolates the measure-theoretic normalization facts used by Le Cam's change-of-measure argument. ★ local_integral_sub_exp_logLikelihoodRatio_integral_tendsto_zero
Likelihood-ratio normalization
This module isolates the measure-theoretic normalization facts used by Le Cam's change-of-measure argument. They apply to varying sample spaces and do not depend on the Gaussian structure of a LAN experiment.
theorem local_integral_sub_exp_logLikelihoodRatio_integral_tendsto_zero reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
For a fixed local direction, a complex observable measurable under both the local and base laws, a uniform bound for that observable, and asymptotic likelihood-ratio normalization, its local-law integral and guarded likelihood-ratio base-law integral have vanishing difference.
Formal statement
hypotheses
Ω :
ℕ → Type u_1
H :
h :
H
φ :
(n : ℕ) → Ω n → ℂ
hlocal :
∀ n, AEMeasurable (φ n) (E.localLaw n h)
hbase :
∀ n, AEMeasurable (φ n) (E.baseLaw n)
hbounded :
∃ C : ℝ, 0 ≤ C ∧ ∀ n ω, ‖φ n ω‖ ≤ C
Proof (Lean source)
theorem local_integral_sub_exp_logLikelihoodRatio_integral_tendsto_zero
{H : Type*} [NormedAddCommGroup H] {E : LocalExperiment Ω H} (h : H)
{φ : (n : ℕ) → Ω n → ℂ}
(hlocal : ∀ n, AEMeasurable (φ n) (E.localLaw n h))
(hbase : ∀ n, AEMeasurable (φ n) (E.baseLaw n))
(hbounded : ∃ C : ℝ, 0 ≤ C ∧ ∀ n ω, ‖φ n ω‖ ≤ C)
(hnormalized : Tendsto
(fun n => ∫ ω, exp (E.logLikelihoodRatio n h ω) ∂E.baseLaw n)
atTop (𝓝 1)) :
Tendsto (fun n =>
(∫ ω, φ n ω ∂E.localLaw n h) -
∫ ω, φ n ω * (exp (E.logLikelihoodRatio n h ω) : ℂ) ∂E.baseLaw n)
atTop (𝓝 0) := by
-- Decompose the local measure into its absolutely continuous and singular parts. On the
-- positive-density set the guarded exponential is the RN derivative; on its zero set it is
-- `exp (-n)`. Normalization forces the missing singular mass to zero, and boundedness of `φ`
-- controls both errors.
rcases hbounded with ⟨C, hC, hφ⟩
have hexp : Tendsto (fun n : ℕ => exp (-(n : ℝ))) atTop (𝓝 0) :=
Real.tendsto_exp_atBot.comp
(tendsto_neg_atTop_atBot.comp tendsto_natCast_atTop_atTop)
have hnormalization (n : ℕ) :
(∫ ω, exp (E.logLikelihoodRatio n h ω) ∂E.baseLaw n) =
1 - ((E.localLaw n h).singularPart (E.baseLaw n)).real univ +
exp (-(n : ℝ)) *
(E.baseLaw n).real {ω |
((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal = 0} := by
letI : IsProbabilityMeasure (E.baseLaw n) := E.base_probability n
letI : IsProbabilityMeasure (E.localLaw n h) := E.local_probability n h
let r : Ω n → ℝ := fun ω =>
((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal
let z : Set (Ω n) := {ω | r ω = 0}
have hr : Measurable r :=
(Measure.measurable_rnDeriv _ _).ennreal_toReal
have hz : MeasurableSet z := hr (measurableSet_singleton 0)
have hr_int : Integrable r (E.baseLaw n) := by
simpa only [integrableOn_univ] using
(Measure.integrableOn_toReal_rnDeriv
(μ := E.localLaw n h) (ν := E.baseLaw n) (s := univ)
(measure_ne_top _ _))
have hi_int : Integrable (z.indicator fun _ => exp (-(n : ℝ)))
(E.baseLaw n) :=
(integrable_const _).indicator hz
have hpoint : (fun ω => exp (E.logLikelihoodRatio n h ω)) =
fun ω => r ω + z.indicator (fun _ => exp (-(n : ℝ))) ω := by
funext ω
unfold LocalExperiment.logLikelihoodRatio
dsimp only
by_cases hzero : r ω = 0
· simp [r, z, hzero]
· have hpos : 0 < r ω := lt_of_le_of_ne ENNReal.toReal_nonneg (Ne.symm hzero)
simp [r, z, hzero, Real.exp_log hpos]
rw [hpoint, integral_add hr_int hi_int, integral_indicator hz,
setIntegral_const, Measure.integral_toReal_rnDeriv']
simp [r, z]
ring
have hsmall : Tendsto (fun n : ℕ =>
exp (-(n : ℝ)) *
(E.baseLaw n).real {ω |
((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal = 0})
atTop (𝓝 0) := by
apply squeeze_zero'
(Filter.Eventually.of_forall fun n : ℕ =>
mul_nonneg (Real.exp_pos _).le measureReal_nonneg)
(Filter.Eventually.of_forall fun n : ℕ => ?_) hexp
haveI : IsProbabilityMeasure (E.baseLaw n) := E.base_probability n
exact mul_le_of_le_one_right (Real.exp_pos _).le measureReal_le_one
have hsing : Tendsto (fun n =>
((E.localLaw n h).singularPart (E.baseLaw n)).real univ)
atTop (𝓝 0) := by
have heq : (fun n : ℕ =>
((E.localLaw n h).singularPart (E.baseLaw n)).real univ) =
fun n : ℕ => 1 +
(exp (-(n : ℝ)) *
(E.baseLaw n).real {ω |
((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal = 0}) -
(∫ ω, exp (E.logLikelihoodRatio n h ω) ∂E.baseLaw n) := by
funext n
rw [hnormalization n]
ring
rw [heq]
convert (tendsto_const_nhds.add hsmall).sub hnormalized using 1 <;> norm_num
have herror (n : ℕ) :
(∫ ω, φ n ω ∂E.localLaw n h) -
∫ ω, φ n ω * (exp (E.logLikelihoodRatio n h ω) : ℂ) ∂E.baseLaw n =
(∫ ω, φ n ω ∂(E.localLaw n h).singularPart (E.baseLaw n)) -
(exp (-(n : ℝ)) : ℂ) *
∫ ω in {ω |
((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal = 0}, φ n ω ∂E.baseLaw n := by
letI : IsProbabilityMeasure (E.baseLaw n) := E.base_probability n
letI : IsProbabilityMeasure (E.localLaw n h) := E.local_probability n h
let r : Ω n → ℝ := fun ω =>
((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal
let z : Set (Ω n) := {ω | r ω = 0}
have hr : Measurable r :=
(Measure.measurable_rnDeriv _ _).ennreal_toReal
have hz : MeasurableSet z := hr (measurableSet_singleton 0)
have hφlocal : Integrable (φ n) (E.localLaw n h) :=
Integrable.of_bound (hlocal n).aestronglyMeasurable C
(ae_of_all _ (hφ n))
have hφsing : Integrable (φ n)
((E.localLaw n h).singularPart (E.baseLaw n)) :=
hφlocal.mono_measure (Measure.singularPart_le _ _)
have hφdensity : Integrable (φ n)
((E.baseLaw n).withDensity ((E.localLaw n h).rnDeriv (E.baseLaw n))) := by
have hi := hφlocal
rw [← Measure.singularPart_add_rnDeriv
(E.localLaw n h) (E.baseLaw n)] at hi
exact (integrable_add_measure.mp hi).2
have hdecomp :
(∫ ω, φ n ω ∂E.localLaw n h) =
(∫ ω, φ n ω ∂(E.localLaw n h).singularPart (E.baseLaw n)) +
∫ ω, φ n ω ∂(E.baseLaw n).withDensity
((E.localLaw n h).rnDeriv (E.baseLaw n)) := by
calc
(∫ ω, φ n ω ∂E.localLaw n h) =
∫ ω, φ n ω ∂((E.localLaw n h).singularPart (E.baseLaw n) +
(E.baseLaw n).withDensity
((E.localLaw n h).rnDeriv (E.baseLaw n))) := by
rw [Measure.singularPart_add_rnDeriv]
_ = _ := integral_add_measure hφsing hφdensity
have hweight_point : (fun ω =>
φ n ω * (exp (E.logLikelihoodRatio n h ω) : ℂ)) =
fun ω => φ n ω * (r ω : ℂ) +
(z.indicator fun ω =>
φ n ω * (exp (-(n : ℝ)) : ℂ)) ω := by
funext ω
unfold LocalExperiment.logLikelihoodRatio
dsimp only
by_cases hzero : r ω = 0
· simp [r, z, hzero]
· have hpos : 0 < r ω := lt_of_le_of_ne ENNReal.toReal_nonneg (Ne.symm hzero)
simp [r, z, hzero, Real.exp_log hpos]
have hdensity :
(∫ ω, φ n ω ∂(E.baseLaw n).withDensity
((E.localLaw n h).rnDeriv (E.baseLaw n))) =
∫ ω, φ n ω * (r ω : ℂ) ∂E.baseLaw n := by
rw [integral_withDensity_eq_integral_toReal_smul
(Measure.measurable_rnDeriv _ _) (Measure.rnDeriv_lt_top _ _) (φ n)]
apply integral_congr_ae
filter_upwards with ω
simp [r, mul_comm]
have hmul_int : Integrable (fun ω => φ n ω * (r ω : ℂ)) (E.baseLaw n) := by
have hi := (integrable_withDensity_iff_integrable_smul'
(Measure.measurable_rnDeriv _ _) (Measure.rnDeriv_lt_top _ _)).mp hφdensity
exact hi.congr (ae_of_all _ fun ω => by simp [r, mul_comm])
have hind_int : Integrable
(z.indicator fun ω => φ n ω * (exp (-(n : ℝ)) : ℂ))
(E.baseLaw n) := by
have hi := ((Integrable.of_bound (hbase n).aestronglyMeasurable C
(ae_of_all _ (hφ n))).indicator hz).mul_const
(exp (-(n : ℝ)) : ℂ)
exact hi.congr (ae_of_all _ fun ω => by
by_cases hw : ω ∈ z <;> simp [hw])
rw [hdecomp, hweight_point, integral_add, hdensity]
· rw [integral_indicator hz, integral_mul_const]
ring
· exact hmul_int
· exact hind_int
rw [show (fun n =>
(∫ ω, φ n ω ∂E.localLaw n h) -
∫ ω, φ n ω * (exp (E.logLikelihoodRatio n h ω) : ℂ) ∂E.baseLaw n) =
fun n =>
(∫ ω, φ n ω ∂(E.localLaw n h).singularPart (E.baseLaw n)) -
(exp (-(n : ℝ)) : ℂ) *
∫ ω in {ω |
((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal = 0}, φ n ω ∂E.baseLaw n from
funext herror]
rw [tendsto_zero_iff_norm_tendsto_zero]
apply squeeze_zero
· intro n
exact norm_nonneg _
· intro n
letI : IsProbabilityMeasure (E.baseLaw n) := E.base_probability n
letI : IsProbabilityMeasure (E.localLaw n h) := E.local_probability n h
calc
‖(∫ ω, φ n ω ∂(E.localLaw n h).singularPart (E.baseLaw n)) -
(exp (-(n : ℝ)) : ℂ) *
∫ ω in {ω |
((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal = 0}, φ n ω ∂E.baseLaw n‖
≤ C * ((E.localLaw n h).singularPart (E.baseLaw n)).real univ +
exp (-(n : ℝ)) * C := by
calc
_ ≤ ‖∫ ω, φ n ω ∂(E.localLaw n h).singularPart (E.baseLaw n)‖ +
‖(exp (-(n : ℝ)) : ℂ) *
∫ ω in {ω |
((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal = 0},
φ n ω ∂E.baseLaw n‖ := norm_sub_le _ _
_ ≤ C * ((E.localLaw n h).singularPart (E.baseLaw n)).real univ +
exp (-(n : ℝ)) *
(C * (E.baseLaw n).real {ω |
((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal = 0}) := by
gcongr
· exact norm_integral_le_of_norm_le_const (ae_of_all _ (hφ n))
· rw [norm_mul, Complex.norm_real, Real.norm_eq_abs,
abs_of_pos (Real.exp_pos _)]
gcongr
have hb := norm_integral_le_of_norm_le_const
(μ := (E.baseLaw n).restrict {ω |
((E.localLaw n h).rnDeriv (E.baseLaw n) ω).toReal = 0})
(ae_of_all _ (hφ n))
simpa [measureReal_restrict_apply] using hb
_ ≤ C * ((E.localLaw n h).singularPart (E.baseLaw n)).real univ +
exp (-(n : ℝ)) * C := by
gcongr
exact mul_le_of_le_one_right hC measureReal_le_one
_ = C * ((E.localLaw n h).singularPart (E.baseLaw n)).real univ +
C * exp (-(n : ℝ)) := by ring
· convert (tendsto_const_nhds.mul hsing).add
(tendsto_const_nhds.mul hexp) using 1 <;> norm_num
1 supporting declaration (lemmas, instances)
-
exp_integral_tendsto_one_of_weaklyConvergestheorem — If real random variables converge weakly, their exponential limit has expectation one, and the row exponential expectations have asymptotic upper bound one, then those expectations tend to one. This is the nonnegative lower-semicontinuous Portmanteau step.hypothesesQ :Measure ℝhP :∀ n, IsProbabilityMeasure (P n)hQ :hweak :WeaklyConverges P X QhrowIntegrable :∀ n, Integrable (fun ω => exp (X n ω)) (P n)hlimit :∫ x, exp x ∂Q = 1Proof (Lean source)
theorem exp_integral_tendsto_one_of_weaklyConverges {P : (n : ℕ) → Measure (Ω n)} {X : (n : ℕ) → Ω n → ℝ} {Q : Measure ℝ} (hP : ∀ n, IsProbabilityMeasure (P n)) (hQ : IsProbabilityMeasure Q) (hweak : WeaklyConverges P X Q) (hrowIntegrable : ∀ n, Integrable (fun ω => exp (X n ω)) (P n)) (hlimit : ∫ x, exp x ∂Q = 1) (hupper : ∀ n, ∫ ω, exp (X n ω) ∂P n ≤ 1 + exp (-(n : ℝ))) : Tendsto (fun n => ∫ ω, exp (X n ω) ∂P n) atTop (𝓝 1) := by -- Approximate `exp` from below by bounded continuous truncations. Weak convergence gives -- their integral limits, monotone convergence recovers `hlimit`, and `hupper` supplies limsup. -- `hrowIntegrable` is essential because Lean's Bochner integral is defined as zero for a -- non-integrable function; without it the statement is false despite the numerical upper bound. let trunc (k : ℕ) : BoundedContinuousFunction ℝ ℝ := BoundedContinuousFunction.mkOfBound ⟨fun x => min (exp x) (k : ℝ), Real.continuous_exp.min continuous_const⟩ (k : ℝ) (by intro x y change |min (exp x) (k : ℝ) - min (exp y) (k : ℝ)| ≤ k have hx0 : 0 ≤ min (exp x) (k : ℝ) := le_min (Real.exp_pos x).le (Nat.cast_nonneg k) have hy0 : 0 ≤ min (exp y) (k : ℝ) := le_min (Real.exp_pos y).le (Nat.cast_nonneg k) have hxk : min (exp x) (k : ℝ) ≤ k := min_le_right _ _ have hyk : min (exp y) (k : ℝ) ≤ k := min_le_right _ _ rw [abs_le] constructor <;> linarith) have hexp_integrable : Integrable (fun x : ℝ => exp x) Q := by by_contra h rw [integral_undef h] at hlimit norm_num at hlimit have htrunc_limit : Tendsto (fun k : ℕ => ∫ x, trunc k x ∂Q) atTop (𝓝 1) := by have hdom : Tendsto (fun k : ℕ => ∫ x, min (exp x) (k : ℝ) ∂Q) atTop (𝓝 (∫ x, exp x ∂Q)) := by apply tendsto_integral_of_dominated_convergence (fun x : ℝ => exp x) · intro k exact (Real.continuous_exp.min continuous_const).aestronglyMeasurable · exact hexp_integrable · intro k filter_upwards with x rw [Real.norm_eq_abs, abs_of_nonneg (le_min (Real.exp_pos x).le (Nat.cast_nonneg k))] exact min_le_left _ _ · filter_upwards with x apply tendsto_nhds_of_eventually_eq have hx : ∀ᶠ k : ℕ in atTop, exp x ≤ (k : ℝ) := tendsto_natCast_atTop_atTop.eventually (eventually_ge_atTop (exp x)) filter_upwards [hx] with k hk exact min_eq_left hk simpa [trunc, hlimit] using hdom have htrunc_row_integrable (k n : ℕ) : Integrable (fun ω => trunc k (X n ω)) (P n) := by apply (hrowIntegrable n).mono' · exact (trunc k).continuous.measurable.comp_aemeasurable (hweak.1 n) |>.aestronglyMeasurable · filter_upwards with ω change |min (exp (X n ω)) (k : ℝ)| ≤ exp (X n ω) rw [abs_of_nonneg (le_min (Real.exp_pos (X n ω)).le (Nat.cast_nonneg k))] exact min_le_left _ _ have hexp_zero : Tendsto (fun n : ℕ => exp (-(n : ℝ))) atTop (𝓝 0) := Real.tendsto_exp_atBot.comp (tendsto_neg_atTop_atBot.comp tendsto_natCast_atTop_atTop) rw [tendsto_order] constructor · intro a ha obtain ⟨k, hk⟩ := ((tendsto_order.mp htrunc_limit).1 a ha).exists have hweak_k := hweak.2 (trunc k) filter_upwards [(tendsto_order.mp hweak_k).1 _ hk] with n hn exact hn.trans_le (integral_mono (htrunc_row_integrable k n) (hrowIntegrable n) fun ω => min_le_left _ _) · intro b hb have hup : Tendsto (fun n : ℕ => 1 + exp (-(n : ℝ))) atTop (𝓝 1) := by simpa using tendsto_const_nhds.add hexp_zero filter_upwards [(tendsto_order.mp hup).2 b hb] with n hn exact (hupper n).trans_lt hn
LogTaylor 1 core · 1 supporting This module contains the analytic and probabilistic Taylor estimates used after a likelihood ratio has been reduced to a sum of coordinate log likelihoods. ★ sum_log_taylor_remainder_tendstoInProbability
Logarithm Taylor bounds for LAN arrays
This module contains the analytic and probabilistic Taylor estimates used after a likelihood ratio has been reduced to a sum of coordinate log likelihoods. It is independent of any particular density model.
theorem sum_log_taylor_remainder_tendstoInProbability reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
If each row is a probability law, its log likelihood has the stated coordinate representation on the small-increment event, its quadratic sum converges in probability, and its largest coordinate vanishes in probability, the summed quadratic Taylor remainder converges in probability to zero.
Formal statement
hypotheses
Ω :
ℕ → Type*
∀ n, MeasurableSpace (Ω n)
P :
(n : ℕ) → Measure (Ω n)
L :
(n : ℕ) → Ω n → ℝ
W :
(n : ℕ) → Ω n → Fin n → ℝ
q :
ℝ
hP :
∀ n, IsProbabilityMeasure (P n)
hidentity :
∀ n, ∀ᵐ x ∂P n, (∀ i, |W n x i| ≤ 1) → L n x = ∑ i, 2 * log (1 + W n x i / 2)
hquadratic :
TendstoInProbability P (fun n x => (∑ i, W n x i ^ 2)) q
conclusion
TendstoInProbability P (fun n x => L n x - (∑ i, W n x i) + (1 / 4 : ℝ) * ∑ i, W n x i ^ 2) 0
Proof (Lean source)
theorem sum_log_taylor_remainder_tendstoInProbability
{Ω : ℕ → Type*} [∀ n, MeasurableSpace (Ω n)]
(P : (n : ℕ) → Measure (Ω n)) (L : (n : ℕ) → Ω n → ℝ)
(W : (n : ℕ) → Ω n → Fin n → ℝ) (q : ℝ)
(hP : ∀ n, IsProbabilityMeasure (P n))
(hidentity : ∀ n, ∀ᵐ x ∂P n, (∀ i, |W n x i| ≤ 1) →
L n x = ∑ i, 2 * log (1 + W n x i / 2))
(hquadratic : TendstoInProbability P
(fun n x => (∑ i, W n x i ^ 2)) q)
(hmax : ∀ ε : ℝ, 0 < ε → Tendsto (fun n => P n
{x | ∃ i, ε ≤ |W n x i|}) atTop (𝓝 0)) :
TendstoInProbability P
(fun n x => L n x - (∑ i, W n x i) +
(1 / 4 : ℝ) * ∑ i, W n x i ^ 2) 0 := by
intro ε hε
let K : ℝ := |q| + 1
have hK : 0 < K := by
dsimp [K]
linarith [abs_nonneg q]
let δ : ℝ := min 1 (ε / (2 * K))
have hδpos : 0 < δ := by
dsimp [δ]
exact lt_min one_pos (div_pos hε (by positivity))
have hδle : δ ≤ 1 := by exact min_le_left _ _
have hδK : δ * K < ε := by
have hle : δ ≤ ε / (2 * K) := min_le_right _ _
have hmul : δ * K ≤ ε / 2 := by
calc
δ * K ≤ (ε / (2 * K)) * K :=
mul_le_mul_of_nonneg_right hle (le_of_lt hK)
_ = ε / 2 := by field_simp
linarith
have hupper : Tendsto (fun n =>
P n {x | ∃ i, δ ≤ |W n x i|} +
P n {x | 1 ≤ |(∑ i, W n x i ^ 2) - q|}) atTop (𝓝 0) := by
convert (hmax δ hδpos).add (hquadratic 1 one_pos) using 1 <;> simp
refine tendsto_of_tendsto_of_tendsto_of_le_of_le'
tendsto_const_nhds hupper
(Eventually.of_forall fun n => bot_le) (Eventually.of_forall fun n => ?_)
calc
P n {x | ε ≤ |(L n x - (∑ i, W n x i) +
(1 / 4 : ℝ) * ∑ i, W n x i ^ 2) - 0|}
≤ P n ({x | ∃ i, δ ≤ |W n x i|} ∪
{x | 1 ≤ |(∑ i, W n x i ^ 2) - q|}) := by
apply measure_mono_ae
filter_upwards [hidentity n] with x hx
intro hxrem
change (∃ i, δ ≤ |W n x i|) ∨
1 ≤ |(∑ i, W n x i ^ 2) - q|
by_contra hbad
push Not at hbad
have hcoord : ∀ i, |W n x i| < δ := hbad.1
have hsmall : ∀ i, |W n x i| ≤ 1 :=
fun i => (hcoord i).le.trans hδle
have hSlt : (∑ i, W n x i ^ 2) < K := by
have habs : |(∑ i, W n x i ^ 2) - q| < 1 := hbad.2
have hdifference :
(∑ i, W n x i ^ 2) - q < 1 :=
(le_abs_self _).trans_lt habs
have hq : q ≤ |q| := le_abs_self q
dsimp [K]
linarith
have hrem :
|L n x - (∑ i, W n x i) +
(1 / 4 : ℝ) * ∑ i, W n x i ^ 2| < ε := by
rw [hx hsmall]
calc
|(∑ i, 2 * log (1 + W n x i / 2)) -
(∑ i, W n x i) +
(1 / 4 : ℝ) * ∑ i, W n x i ^ 2|
= |∑ i, (2 * log (1 + W n x i / 2) -
W n x i + (1 / 4 : ℝ) * W n x i ^ 2)| := by
congr 1
rw [Finset.sum_add_distrib, Finset.sum_sub_distrib,
Finset.mul_sum]
_ ≤ ∑ i, |2 * log (1 + W n x i / 2) -
W n x i + (1 / 4 : ℝ) * W n x i ^ 2| :=
Finset.abs_sum_le_sum_abs _ _
_ ≤ ∑ i, δ * W n x i ^ 2 := by
apply Finset.sum_le_sum
intro i hi
refine (abs_two_mul_log_one_add_half_sub_quadratic_le_cube
(W n x i) ((hcoord i).le.trans hδle)).trans ?_
calc
|W n x i| ^ 3 = |W n x i| * W n x i ^ 2 := by
rw [← sq_abs]
ring
_ ≤ δ * W n x i ^ 2 :=
mul_le_mul_of_nonneg_right (hcoord i).le (sq_nonneg _)
_ = δ * (∑ i, W n x i ^ 2) := by rw [Finset.mul_sum]
_ < δ * K := mul_lt_mul_of_pos_left hSlt hδpos
_ < ε := hδK
change ε ≤ |L n x - (∑ i, W n x i) +
(1 / 4 : ℝ) * ∑ i, W n x i ^ 2 - 0| at hxrem
simp only [sub_zero] at hxrem
exact not_lt_of_ge hxrem hrem
_ ≤ P n {x | ∃ i, δ ≤ |W n x i|} +
P n {x | 1 ≤ |(∑ i, W n x i ^ 2) - q|} :=
measure_union_le _ _
1 supporting declaration (lemmas, instances)
-
abs_two_mul_log_one_add_half_sub_quadratic_le_cubetheorem — On [-1,1], the quadratic Taylor error of 2 log (1+w/2) is bounded by |w|³.Proof (Lean source)
theorem abs_two_mul_log_one_add_half_sub_quadratic_le_cube (w : ℝ) (hw : |w| ≤ 1) : |2 * log (1 + w / 2) - w + (1 / 4 : ℝ) * w ^ 2| ≤ |w| ^ 3 := by have hrad : |-w / 2| < (1 : ℝ) := by rw [abs_div, abs_neg] norm_num linarith have h := Real.abs_log_sub_add_sum_range_le (x := -w / 2) hrad 2 norm_num [Finset.sum_range_succ] at h rw [abs_div, abs_neg] at h norm_num at h have h' : |(-w / 2) + (-w / 2) ^ 2 / 2 + log (1 + w / 2)| ≤ (|w| / 2) ^ 3 / (1 - |w| / 2) := by convert h using 1 <;> ring have hden : (0 : ℝ) < 1 - |w| / 2 := by linarith [abs_nonneg w] have hscaled : 2 * |(-w / 2) + (-w / 2) ^ 2 / 2 + log (1 + w / 2)| ≤ |w| ^ 3 := by calc 2 * |(-w / 2) + (-w / 2) ^ 2 / 2 + log (1 + w / 2)| ≤ 2 * ((|w| / 2) ^ 3 / (1 - |w| / 2)) := by nlinarith _ ≤ |w| ^ 3 := by rw [← mul_div_assoc, div_le_iff₀ hden] have ha3 : 0 ≤ |w| ^ 3 := pow_nonneg (abs_nonneg w) _ nlinarith [mul_nonneg ha3 (sub_nonneg.mpr hw)] calc |2 * log (1 + w / 2) - w + (1 / 4 : ℝ) * w ^ 2| = 2 * |(-w / 2) + (-w / 2) ^ 2 / 2 + log (1 + w / 2)| := by rw [← abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 2), ← abs_mul] congr 1 ring _ ≤ |w| ^ 3 := hscaled
TriangularArray 1 core · 5 supporting This module isolates the generic probability estimates behind the quadratic log-likelihood Taylor expansion. ★ iid_max_tendsto_zero_of_lindeberg
Triangular-array estimates for i.i.d. LAN expansions
This module isolates the generic probability estimates behind the quadratic log-likelihood
Taylor expansion. The rows may change with n, but the coordinates within each row have one
common law. These results contain no statistical-model or density-specific definitions.
theorem iid_max_tendsto_zero_of_lindeberg reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
For an i.i.d. triangular row with measurable coordinates, finite second moments, and a Lindeberg tail condition, the probability that its largest absolute coordinate exceeds any positive threshold vanishes.
Formal statement
hypotheses
X :
Type u_1
P :
W :
ℕ → X → ℝ
hW :
∀ n, Measurable (W n)
hW2 :
∀ n, MemLp (W n) 2 P
hlindeberg :
ε :
ℝ
0 < ε
Proof (Lean source)
theorem iid_max_tendsto_zero_of_lindeberg
(P : Measure X) [IsProbabilityMeasure P]
(W : ℕ → X → ℝ)
(hW : ∀ n, Measurable (W n)) (hW2 : ∀ n, MemLp (W n) 2 P)
(hlindeberg : ∀ ε : ℝ, 0 < ε → Tendsto (fun n : ℕ => (n : ℝ) *
∫ x in {x | ε ≤ |W n x|}, W n x ^ 2 ∂P) atTop (𝓝 0)) :
∀ ε : ℝ, 0 < ε → Tendsto (fun n => Measure.pi (fun _ : Fin n => P)
{x | ∃ i, ε ≤ |W n (x i)|}) atTop (𝓝 0) := by
-- Use the finite union bound and Markov on `W² 1_{|W|≥ε}`. The explicit
-- `MemLp` premise is logically necessary with Mathlib's Bochner integral convention:
-- the integral of a non-integrable real function is definitionally zero, so the displayed
-- Lindeberg limit alone cannot rule out non-square-integrable rows.
intro ε hε
have hreal : Tendsto (fun n => (Measure.pi (fun _ : Fin n => P)).real
{x | ∃ i, ε ≤ |W n (x i)|}) atTop (𝓝 0) := by
apply squeeze_zero (g := fun n : ℕ => (ε ^ 2)⁻¹ *
((n : ℝ) * ∫ x in {x | ε ≤ |W n x|}, W n x ^ 2 ∂P))
· exact fun n => measureReal_nonneg
· intro n
calc
(Measure.pi (fun _ : Fin n => P)).real
{x | ∃ i, ε ≤ |W n (x i)|}
≤ (n : ℝ) * (ε ^ 2)⁻¹ *
∫ x in {x | ε ≤ |W n x|}, W n x ^ 2 ∂P :=
iid_large_coordinate_measureReal_le P (W n) (hW n) (hW2 n) n hε
_ = (ε ^ 2)⁻¹ *
((n : ℝ) * ∫ x in {x | ε ≤ |W n x|}, W n x ^ 2 ∂P) := by ring
· simpa using (hlindeberg ε hε).const_mul ((ε ^ 2)⁻¹)
exact (ENNReal.tendsto_toReal_zero_iff
(fun n => measure_ne_top (Measure.pi (fun _ : Fin n => P))
{x | ∃ i, ε ≤ |W n (x i)|})).1 hreal
5 supporting declarations (lemmas, instances)
-
scaledL2Approx_lindebergtheorem — An L² approximation of a triangular row by S / sqrt n transfers the fixed L² tail condition of S to the Lindeberg tail condition for the row.hypothesesX :sharedType u_1P :W :ℕ → X → ℝS :X → ℝhW :∀ n, Measurable (W n)hW2 :∀ n, MemLp (W n) 2 PhS :MemLp S 2 Pε :ℝ0 < εProof (Lean source)
theorem scaledL2Approx_lindeberg (P : Measure X) [IsProbabilityMeasure P] (W : ℕ → X → ℝ) (S : X → ℝ) (hW : ∀ n, Measurable (W n)) (hW2 : ∀ n, MemLp (W n) 2 P) (hS : MemLp S 2 P) (happrox : Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P) atTop (𝓝 0)) : ∀ ε : ℝ, 0 < ε → Tendsto (fun n : ℕ => (n : ℝ) * ∫ x in {x | ε ≤ |W n x|}, W n x ^ 2 ∂P) atTop (𝓝 0) := by intro ε hε classical let A : ℕ → Set X := fun n => {x | ε ≤ |W n x|} let good : ℕ → Prop := fun n => Integrable (fun x => W n x ^ 2) P let B : ℕ → Set X := fun n => if good n then A n else ∅ have hS2 : Integrable (fun x => S x ^ 2) P := hS.integrable_sq have hBmeas : ∀ n, MeasurableSet (B n) := by intro n simp only [B] split_ifs · exact measurableSet_Ici.preimage (hW n).abs · exact MeasurableSet.empty have hBmeasure_real : Tendsto (fun n => P.real (B n)) atTop (𝓝 0) := by apply squeeze_zero (g := fun (n : ℕ) => (ε ^ 2)⁻¹ * (2 * ∫ x, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P + 2 * ((sqrt (n : ℝ))⁻¹) ^ 2 * ∫ x, S x ^ 2 ∂P)) · intro n; positivity · intro n by_cases hn : good n · have hW2n : Integrable (fun x => W n x ^ 2) P := hn have hmarkov := mul_meas_ge_le_integral_of_nonneg (μ := P) (f := fun x => W n x ^ 2) (ae_of_all P fun x => sq_nonneg (W n x)) hW2n (ε ^ 2) have hset : {x | ε ^ 2 ≤ W n x ^ 2} = A n := by ext x simp only [A, Set.mem_ofPred_eq] rw [← sq_abs (W n x), sq_le_sq₀ hε.le (abs_nonneg _)] rw [hset] at hmarkov simp only [B, if_pos hn] calc P.real (A n) ≤ (ε ^ 2)⁻¹ * ∫ x, W n x ^ 2 ∂P := by calc P.real (A n) = (ε ^ 2)⁻¹ * ((ε ^ 2) * P.real (A n)) := by field_simp _ ≤ _ := mul_le_mul_of_nonneg_left hmarkov (inv_nonneg.2 (sq_nonneg ε)) _ ≤ (ε ^ 2)⁻¹ * (2 * ∫ x, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P + 2 * ((sqrt (n : ℝ))⁻¹) ^ 2 * ∫ x, S x ^ 2 ∂P) := by have hWmem : MemLp (W n) 2 P := (memLp_two_iff_integrable_sq (hW n).aestronglyMeasurable).2 hW2n have hSmem : MemLp (fun x => (sqrt (n : ℝ))⁻¹ * S x) 2 P := hS.const_mul _ have herrn : Integrable (fun x => (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2) P := (hWmem.sub hSmem).integrable_sq have hIntBound : ∫ x, W n x ^ 2 ∂P ≤ 2 * ∫ x, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P + 2 * ((sqrt (n : ℝ))⁻¹) ^ 2 * ∫ x, S x ^ 2 ∂P := by calc ∫ x, W n x ^ 2 ∂P ≤ ∫ x, 2 * (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 + (2 * ((sqrt (n : ℝ))⁻¹) ^ 2) * S x ^ 2 ∂P := by apply integral_mono hW2n ((herrn.const_mul 2).add (hS2.const_mul _)) intro x dsimp only [Pi.add_apply] nlinarith [sq_nonneg (W n x - 2 * (sqrt (n : ℝ))⁻¹ * S x)] _ = _ := by rw [integral_add (herrn.const_mul 2) (hS2.const_mul _), integral_const_mul, integral_const_mul] exact mul_le_mul_of_nonneg_left hIntBound (inv_nonneg.2 (sq_nonneg ε)) · simp only [B, if_neg hn, measureReal_empty] positivity · have herr : Tendsto (fun n : ℕ => ∫ x, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P) atTop (𝓝 0) := by apply squeeze_zero' (g := fun (n : ℕ) => (n : ℝ) * ∫ x, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P) · exact Eventually.of_forall fun n => integral_nonneg (μ := P) (fun x => sq_nonneg _) · filter_upwards [eventually_ge_atTop 1] with n hn have hi : 0 ≤ ∫ x, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P := integral_nonneg (μ := P) (fun x => sq_nonneg _) have hnreal : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn nlinarith · exact happrox have hsqrt : Tendsto (fun n : ℕ => ((sqrt (n : ℝ))⁻¹) ^ 2) atTop (𝓝 0) := by have hinv : Tendsto (fun n : ℕ => ((n : ℝ))⁻¹) atTop (𝓝 0) := tendsto_natCast_atTop_atTop.inv_tendsto_atTop apply hinv.congr' exact Eventually.of_forall fun n => by change ((n : ℝ))⁻¹ = ((sqrt (n : ℝ))⁻¹) ^ 2 rw [inv_pow, Real.sq_sqrt (Nat.cast_nonneg n)] have ht := ((herr.const_mul 2).add (hsqrt.const_mul (2 * ∫ x, S x ^ 2 ∂P))).const_mul ((ε ^ 2)⁻¹) convert ht using 1 · funext n ring · norm_num have hBmeasure : Tendsto (fun n => P (B n)) atTop (𝓝 0) := (ENNReal.tendsto_toReal_zero_iff (fun n => measure_ne_top P (B n))).1 hBmeasure_real have hsmall : Tendsto (fun n => ∫ x in B n, S x ^ 2 ∂P) atTop (𝓝 0) := hS2.tendsto_setIntegral_nhds_zero hBmeasure apply squeeze_zero (g := fun (n : ℕ) => 2 * ((n : ℝ) * ∫ x, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P) + 2 * ∫ x in B n, S x ^ 2 ∂P) · intro n exact mul_nonneg (Nat.cast_nonneg n) (integral_nonneg fun x => sq_nonneg _) · intro n by_cases hn : good n · have hW2n : Integrable (fun x => W n x ^ 2) P := hn have herrn : Integrable (fun x => (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2) P := by have hWmem : MemLp (W n) 2 P := (memLp_two_iff_integrable_sq (hW n).aestronglyMeasurable).2 hW2n exact (hWmem.sub (hS.const_mul _)).integrable_sq have hpoint : ∀ x, W n x ^ 2 ≤ 2 * (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 + 2 * ((sqrt (n : ℝ))⁻¹) ^ 2 * S x ^ 2 := by intro x nlinarith [sq_nonneg (W n x - 2 * (sqrt (n : ℝ))⁻¹ * S x)] have hBA : B n = A n := by simp [B, hn] calc (n : ℝ) * ∫ x in A n, W n x ^ 2 ∂P ≤ (n : ℝ) * ∫ x in A n, (2 * (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 + 2 * ((sqrt (n : ℝ))⁻¹) ^ 2 * S x ^ 2) ∂P := by apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg n) exact setIntegral_mono_on hW2n.integrableOn ((herrn.const_mul 2).add (hS2.const_mul _)).integrableOn (hBA ▸ hBmeas n) fun x _ => by exact hpoint x _ ≤ 2 * ((n : ℝ) * ∫ x, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P) + 2 * ∫ x in B n, S x ^ 2 ∂P := by rw [hBA] rw [integral_add (herrn.const_mul 2 |>.integrableOn) (hS2.const_mul _ |>.integrableOn), integral_const_mul, integral_const_mul] have hemono : ∫ x in A n, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P ≤ ∫ x, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P := integral_mono_measure P.restrict_le_self (ae_of_all _ fun x => sq_nonneg _) herrn have hsqrtn : (n : ℝ) * ((sqrt (n : ℝ))⁻¹) ^ 2 ≤ 1 := by by_cases hn0 : n = 0 · simp [hn0] · rw [inv_pow, Real.sq_sqrt (Nat.cast_nonneg n)] field_simp norm_num have hSint : 0 ≤ ∫ x in A n, S x ^ 2 ∂P := integral_nonneg (μ := P.restrict (A n)) (fun x => sq_nonneg (S x)) nlinarith · rw [integral_undef] · simp only [mul_zero] have hBn : B n = ∅ := by simp [B, hn] rw [hBn, setIntegral_empty] have herr_nonneg : 0 ≤ (n : ℝ) * ∫ x, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P := mul_nonneg (Nat.cast_nonneg n) (integral_nonneg (μ := P) (fun x => sq_nonneg _)) positivity · intro htail apply hn have hcomp : IntegrableOn (fun x => W n x ^ 2) (A n)ᶜ P := by apply (integrable_const (μ := P.restrict (A n)ᶜ) (c := ε ^ 2)).mono' · exact (hW n).pow_const 2 |>.aestronglyMeasurable.restrict · filter_upwards [ae_restrict_mem ((measurableSet_Ici.preimage (hW n).abs).compl)] with x hx simp only [A, Set.mem_compl_iff, Set.mem_ofPred_eq, not_le] at hx rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] have hs := (sq_lt_sq₀ (abs_nonneg (W n x)) hε.le).2 hx rw [sq_abs] at hs exact hs.le change Integrable (fun x => W n x ^ 2) P rw [← integrableOn_univ, ← Set.union_compl_self (A n), integrableOn_union] exact ⟨htail, hcomp⟩ · simpa using (happrox.const_mul 2).add (hsmall.const_mul 2) -
iid_sum_approx_tendstoInProbabilitytheorem — For an i.i.d. product row, a centered sum of errors converges in probability to zero when the row error has total second moment tending to zero. A convergent scaled row mean supplies the stated deterministic limit.hypothesesX :sharedType u_1P :W :ℕ → X → ℝS :X → ℝm :ℝhW :∀ n, Measurable (W n)hW2 :∀ n, MemLp (W n) 2 PhS :MemLp S 2 PhSmean :∫ x, S x ∂P = 0Proof (Lean source)
theorem iid_sum_approx_tendstoInProbability (P : Measure X) [IsProbabilityMeasure P] (W : ℕ → X → ℝ) (S : X → ℝ) (m : ℝ) (hW : ∀ n, Measurable (W n)) (hW2 : ∀ n, MemLp (W n) 2 P) (hS : MemLp S 2 P) (hSmean : ∫ x, S x ∂P = 0) (happrox : Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, (W n x - (sqrt (n : ℝ))⁻¹ * S x) ^ 2 ∂P) atTop (𝓝 0)) (hmean : Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, W n x ∂P) atTop (𝓝 m)) : TendstoInProbability (fun n => Measure.pi (fun _ : Fin n => P)) (fun n x => (∑ i, W n (x i)) - (sqrt (n : ℝ))⁻¹ * ∑ i, S (x i)) m := by -- Apply Chebyshev to the sum of the independent coordinate errors. Its variance is at most -- `n` times the one-coordinate second moment, while its expectation tends to `m`. Rowwise -- `MemLp` is explicit because a bare Bochner square integral does not imply integrability. let g : ℕ → X → ℝ := fun n x => W n x - (sqrt (n : ℝ))⁻¹ * S x have hg : ∀ n, MemLp (g n) 2 P := by intro n change MemLp (W n - fun x => (sqrt (n : ℝ))⁻¹ * S x) 2 P exact (hW2 n).sub (hS.const_mul (sqrt (n : ℝ))⁻¹) have hgmean : ∀ n, ∫ x, g n x ∂P = ∫ x, W n x ∂P := by intro n simp only [g] rw [integral_sub ((hW2 n).integrable (by norm_num)) ((hS.const_mul _).integrable (by norm_num)), integral_const_mul, hSmean] ring have hcenter : Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, g n x ∂P) atTop (𝓝 m) := by simpa only [hgmean] using hmean intro ε hε have hhalf : 0 < ε / 2 := half_pos hε have hcenter_close : ∀ᶠ n : ℕ in atTop, |(n : ℝ) * ∫ x, g n x ∂P - m| < ε / 2 := by rw [Metric.tendsto_atTop] at hcenter obtain ⟨N, hN⟩ := hcenter (ε / 2) hhalf filter_upwards [eventually_ge_atTop N] with n hn simpa [Real.dist_eq] using hN n hn have hbound_tend : Tendsto (fun n : ℕ => ofReal (((n : ℝ) * ∫ x, (g n x) ^ 2 ∂P) / (ε / 2) ^ 2)) atTop (𝓝 0) := by have ht := ENNReal.tendsto_ofReal (happrox.div_const ((ε / 2) ^ 2)) simpa [g] using ht apply tendsto_of_tendsto_of_tendsto_of_le_of_le' (f := fun n => Measure.pi (fun _ : Fin n => P) {x | ε ≤ |((∑ i, W n (x i)) - (sqrt (n : ℝ))⁻¹ * ∑ i, S (x i)) - m|}) (g := fun _ => 0) (h := fun n => ofReal (((n : ℝ) * ∫ x, (g n x) ^ 2 ∂P) / (ε / 2) ^ 2)) tendsto_const_nhds hbound_tend · exact Eventually.of_forall fun _ => bot_le · filter_upwards [hcenter_close] with n hn have hcheb := iid_sum_chebyshev (N := n) P (g n) (hg n) hhalf calc Measure.pi (fun _ : Fin n => P) {x | ε ≤ |((∑ i, W n (x i)) - (sqrt (n : ℝ))⁻¹ * ∑ i, S (x i)) - m|} ≤ Measure.pi (fun _ : Fin n => P) {x | ε / 2 ≤ |(∑ i, g n (x i)) - (n : ℝ) * ∫ y, g n y ∂P|} := by apply measure_mono intro x hx change ε ≤ |((∑ i, W n (x i)) - (sqrt (n : ℝ))⁻¹ * ∑ i, S (x i)) - m| at hx change ε / 2 ≤ |(∑ i, g n (x i)) - (n : ℝ) * ∫ y, g n y ∂P| have hsum : (∑ i, W n (x i)) - (sqrt (n : ℝ))⁻¹ * ∑ i, S (x i) = ∑ i, g n (x i) := by simp only [g, Finset.sum_sub_distrib] rw [Finset.mul_sum] rw [hsum] at hx have htri := abs_sub_le (∑ i, g n (x i)) ((n : ℝ) * ∫ y, g n y ∂P) m nlinarith _ ≤ ofReal ((n : ℝ) * Var[g n; P] / (ε / 2) ^ 2) := hcheb _ ≤ ofReal (((n : ℝ) * ∫ x, (g n x) ^ 2 ∂P) / (ε / 2) ^ 2) := by apply ENNReal.ofReal_le_ofReal apply div_le_div_of_nonneg_right _ (sq_nonneg _) exact mul_le_mul_of_nonneg_left (variance_le_expectation_sq (hg n).aestronglyMeasurable) (Nat.cast_nonneg n) -
iid_large_coordinate_measureReal_letheorem — For one square-integrable row, the probability that at least one i.i.d. coordinate exceeds δ is bounded by n / δ² times the second moment on the tail |W| ≥ δ.hypothesesProof (Lean source)
theorem iid_large_coordinate_measureReal_le (P : Measure X) [IsProbabilityMeasure P] (W : X → ℝ) (hW : Measurable W) (hW2 : MemLp W 2 P) (n : ℕ) {δ : ℝ} (hδ : 0 < δ) : (Measure.pi (fun _ : Fin n => P)).real {x | ∃ i, δ ≤ |W (x i)|} ≤ (n : ℝ) * (δ ^ 2)⁻¹ * ∫ x in {x | δ ≤ |W x|}, W x ^ 2 ∂P := by -- Rewrite the event as a finite union, use `measureReal_iUnion_fintype_le`, identify every -- coordinate marginal by `measurePreserving_eval`, and apply Markov to `W²` on the tail. let A : Set X := {x | δ ≤ |W x|} have hA : MeasurableSet A := measurableSet_Ici.preimage hW.abs have hsingle : P.real A ≤ (δ ^ 2)⁻¹ * ∫ x in A, W x ^ 2 ∂P := by let f : X → ℝ := A.indicator (fun x => W x ^ 2) have hfint : Integrable f P := hW2.integrable_sq.indicator hA have hfnonneg : ∀ᵐ x ∂P, 0 ≤ f x := ae_of_all P fun x => Set.indicator_nonneg (fun _ _ => sq_nonneg _) _ have hmarkov := mul_meas_ge_le_integral_of_nonneg (μ := P) hfnonneg hfint (δ ^ 2) have hset : {x | δ ^ 2 ≤ f x} = A := by ext x by_cases hx : x ∈ A · simp only [f, Set.indicator_of_mem hx, Set.mem_ofPred_eq, hx, iff_true] have habs : δ ≤ |W x| := hx simpa [sq_abs] using (sq_le_sq₀ hδ.le (abs_nonneg _)).2 habs · simp only [f, Set.indicator_of_notMem hx, Set.mem_ofPred_eq, hx, iff_false] exact not_le_of_gt (sq_pos_of_pos hδ) rw [hset, integral_indicator hA] at hmarkov calc P.real A = (δ ^ 2)⁻¹ * ((δ ^ 2) * P.real A) := by field_simp _ ≤ (δ ^ 2)⁻¹ * ∫ x in A, W x ^ 2 ∂P := mul_le_mul_of_nonneg_left hmarkov (inv_nonneg.2 (sq_nonneg δ)) have hevent : {x : Fin n → X | ∃ i, δ ≤ |W (x i)|} = ⋃ i : Fin n, (Function.eval i) ⁻¹' A := by ext x simp [A] rw [hevent] calc (Measure.pi (fun _ : Fin n => P)).real (⋃ i : Fin n, (Function.eval i) ⁻¹' A) ≤ ∑ i : Fin n, (Measure.pi (fun _ : Fin n => P)).real ((Function.eval i) ⁻¹' A) := measureReal_iUnion_fintype_le _ _ = ∑ _i : Fin n, P.real A := by apply Finset.sum_congr rfl intro i _ exact (measurePreserving_eval (fun _ : Fin n => P) i).measureReal_preimage hA.nullMeasurableSet _ ≤ ∑ _i : Fin n, ((δ ^ 2)⁻¹ * ∫ x in A, W x ^ 2 ∂P) := Finset.sum_le_sum fun _ _ => hsingle _ = (n : ℝ) * (δ ^ 2)⁻¹ * ∫ x in A, W x ^ 2 ∂P := by rw [Finset.sum_const, nsmul_eq_mul] simp only [Finset.card_univ, Fintype.card_fin] ring -
iid_truncated_sq_deviation_letheorem — The centered sum of the truncated squares W² 1{|W|<δ} under an i.i.d. product law obeys a Chebyshev bound controlled by n δ² E[W²].hypothesesProof (Lean source)
theorem iid_truncated_sq_deviation_le (P : Measure X) [IsProbabilityMeasure P] (W : X → ℝ) (hW : Measurable W) (hW2 : MemLp W 2 P) (n : ℕ) {δ ε : ℝ} (hδ : 0 < δ) (hε : 0 < ε) : Measure.pi (fun _ : Fin n => P) {x | ε ≤ |(∑ i, if |W (x i)| < δ then W (x i) ^ 2 else 0) - (n : ℝ) * ∫ y, (if |W y| < δ then W y ^ 2 else 0) ∂P|} ≤ ofReal (((n : ℝ) * δ ^ 2 * ∫ y, W y ^ 2 ∂P) / ε ^ 2) := by -- Apply `iid_sum_chebyshev` to the bounded truncation. Bound its -- variance by its second moment and use `(W² 1{|W|<δ})² ≤ δ² W²` under the base law. let g : X → ℝ := fun x => if |W x| < δ then W x ^ 2 else 0 have hgmeas : Measurable g := by exact (hW.pow_const 2).ite (measurableSet_Iio.preimage hW.abs) measurable_const have hgbound : ∀ x, ‖g x‖ ≤ δ ^ 2 := by intro x simp only [g] split_ifs with hx · rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] have hs := (sq_lt_sq₀ (abs_nonneg (W x)) hδ.le).2 hx simpa [sq_abs] using hs.le · simp only [norm_zero] exact sq_nonneg δ have hg : MemLp g 2 P := MemLp.of_bound hgmeas.aestronglyMeasurable (δ ^ 2) (ae_of_all P hgbound) have hvar : Var[g; P] ≤ δ ^ 2 * ∫ y, W y ^ 2 ∂P := by calc Var[g; P] ≤ ∫ y, g y ^ 2 ∂P := variance_le_expectation_sq hg.aestronglyMeasurable _ ≤ ∫ y, δ ^ 2 * W y ^ 2 ∂P := by apply integral_mono hg.integrable_sq (hW2.integrable_sq.const_mul _) intro y simp only [g] split_ifs with hy · have hs := (sq_lt_sq₀ (abs_nonneg (W y)) hδ.le).2 hy rw [sq_abs] at hs nlinarith [sq_nonneg (W y)] · simpa using mul_nonneg (sq_nonneg δ) (sq_nonneg (W y)) _ = δ ^ 2 * ∫ y, W y ^ 2 ∂P := by rw [integral_const_mul] have hcheb := iid_sum_chebyshev (N := n) P g hg hε change Measure.pi (fun _ : Fin n => P) {x | ε ≤ |(∑ i, g (x i)) - (n : ℝ) * ∫ y, g y ∂P|} ≤ _ refine hcheb.trans ?_ apply ENNReal.ofReal_le_ofReal calc (n : ℝ) * Var[g; P] / ε ^ 2 ≤ (n : ℝ) * (δ ^ 2 * ∫ y, W y ^ 2 ∂P) / ε ^ 2 := by apply div_le_div_of_nonneg_right _ (sq_nonneg ε) exact mul_le_mul_of_nonneg_left hvar (Nat.cast_nonneg n) _ = ((n : ℝ) * δ ^ 2 * ∫ y, W y ^ 2 ∂P) / ε ^ 2 := by ring -
iid_sum_sq_tendstoInProbability_of_lindebergtheorem — The sum of squares in an infinitesimal i.i.d. triangular row obeys a weak law when its scaled second moment converges and its Lindeberg tail vanishes.hypothesesconclusionTendstoInProbability (fun n => Measure.pi (fun _ : Fin n => P)) (fun n x => (∑ i, W n (x i) ^ 2)) qProof (Lean source)
theorem iid_sum_sq_tendstoInProbability_of_lindeberg (P : Measure X) [IsProbabilityMeasure P] (W : ℕ → X → ℝ) (q : ℝ) (hW : ∀ n, Measurable (W n)) (hW2 : ∀ n, MemLp (W n) 2 P) (hsecond : Tendsto (fun n : ℕ => (n : ℝ) * ∫ x, W n x ^ 2 ∂P) atTop (𝓝 q)) (hlindeberg : ∀ ε : ℝ, 0 < ε → Tendsto (fun n : ℕ => (n : ℝ) * ∫ x in {x | ε ≤ |W n x|}, W n x ^ 2 ∂P) atTop (𝓝 0)) : TendstoInProbability (fun n => Measure.pi (fun _ : Fin n => P)) (fun n x => (∑ i, W n (x i) ^ 2)) q := by -- Truncate `W²` at a fixed level, apply Chebyshev to the bounded independent summands, and -- remove the truncation with `hlindeberg`; then send the truncation level to zero. intro ε hε have hreal : Tendsto (fun n => (Measure.pi (fun _ : Fin n => P)).real {x | ε ≤ |(∑ i, W n (x i) ^ 2) - q|}) atTop (𝓝 0) := by rw [Metric.tendsto_atTop] intro η hη let ρ : ℝ := min η 1 have hρ : 0 < ρ := lt_min hη zero_lt_one have hρη : ρ ≤ η := min_le_left _ _ have hρ1 : ρ ≤ 1 := min_le_right _ _ let t : ℝ := ε / 2 have ht : 0 < t := half_pos hε let C : ℝ := |q| + 1 have hC : 0 < C := by positivity have hC1 : 1 ≤ C := by simp [C] let δ : ℝ := ρ * t / (4 * C) have hδ : 0 < δ := by dsimp [δ]; positivity let a : ℕ → ℝ := fun n => (n : ℝ) * ∫ x, (if |W n x| < δ then W n x ^ 2 else 0) ∂P let b : ℕ → ℝ := fun n => (n : ℝ) * ∫ x, W n x ^ 2 ∂P let r : ℕ → ℝ := fun n => (n : ℝ) * ∫ x in {x | δ ≤ |W n x|}, W n x ^ 2 ∂P have hsplit : ∀ n, b n = a n + r n := by intro n have hA : MeasurableSet {x | δ ≤ |W n x|} := measurableSet_Ici.preimage (hW n).abs have hsint : Integrable (fun x => W n x ^ 2) P := (hW2 n).integrable_sq have htint : Integrable (fun x => if |W n x| < δ then W n x ^ 2 else 0) P := by apply hsint.mono' · exact ((hW n).pow_const 2).ite (measurableSet_Iio.preimage (hW n).abs) measurable_const |>.aestronglyMeasurable · exact ae_of_all P fun x => by split_ifs <;> simp [sq_nonneg] have hrint : Integrable ({x | δ ≤ |W n x|}.indicator (fun x => W n x ^ 2)) P := hsint.indicator hA dsimp [a, b, r] rw [← integral_indicator hA, ← mul_add, ← integral_add htint hrint] congr 1 apply integral_congr_ae exact ae_of_all P fun x => by change W n x ^ 2 = (if |W n x| < δ then W n x ^ 2 else 0) + {x | δ ≤ |W n x|}.indicator (fun x => W n x ^ 2) x by_cases hx : δ ≤ |W n x| · simp [hx, not_lt_of_ge hx] · simp [hx, lt_of_not_ge hx] have ha : Tendsto a atTop (𝓝 q) := by have hbr : Tendsto (fun n => b n - r n) atTop (𝓝 q) := by simpa [b, r] using hsecond.sub (hlindeberg δ hδ) apply hbr.congr' exact Eventually.of_forall fun n => by change b n - r n = a n rw [hsplit n] ring have hlarge_tend : Tendsto (fun n => (δ ^ 2)⁻¹ * r n) atTop (𝓝 0) := by simpa [r] using (hlindeberg δ hδ).const_mul ((δ ^ 2)⁻¹) have hlarge_small : ∀ᶠ n in atTop, (δ ^ 2)⁻¹ * r n < ρ / 4 := by have hm := Metric.tendsto_atTop.mp hlarge_tend (ρ / 4) (by positivity) obtain ⟨N, hN⟩ := hm filter_upwards [eventually_ge_atTop N] with n hn have hh := hN n hn rw [Real.dist_eq, sub_zero, abs_of_nonneg] at hh · exact hh · exact mul_nonneg (inv_nonneg.2 (sq_nonneg δ)) (mul_nonneg (Nat.cast_nonneg n) (integral_nonneg (μ := P.restrict {x | δ ≤ |W n x|}) (fun x => sq_nonneg _))) have habias : ∀ᶠ n in atTop, |a n - q| < t := by have hm := Metric.tendsto_atTop.mp ha t ht obtain ⟨N, hN⟩ := hm filter_upwards [eventually_ge_atTop N] with n hn simpa [Real.dist_eq] using hN n hn have hbC : ∀ᶠ n in atTop, b n < C := by have hm := Metric.tendsto_atTop.mp (show Tendsto b atTop (𝓝 q) by simpa [b] using hsecond) 1 zero_lt_one obtain ⟨N, hN⟩ := hm filter_upwards [eventually_ge_atTop N] with n hn have hh := hN n hn rw [Real.dist_eq] at hh dsimp [C] have hsub : b n - q ≤ |b n - q| := le_abs_self _ linarith [le_abs_self q] rw [← eventually_atTop] filter_upwards [hlarge_small, habias, hbC] with n hnlarge hnbias hnb let μn : Measure (Fin n → X) := Measure.pi (fun _ : Fin n => P) let L : Set (Fin n → X) := {x | ∃ i, δ ≤ |W n (x i)|} let D : Set (Fin n → X) := {x | t ≤ |(∑ i, if |W n (x i)| < δ then W n (x i) ^ 2 else 0) - a n|} have hsubset : {x | ε ≤ |(∑ i, W n (x i) ^ 2) - q|} ⊆ L ∪ D := by intro x hx by_cases hxL : x ∈ L · exact Set.mem_union_left _ hxL · apply Set.mem_union_right change t ≤ |(∑ i, if |W n (x i)| < δ then W n (x i) ^ 2 else 0) - a n| have hall : ∀ i, |W n (x i)| < δ := by intro i exact lt_of_not_ge fun hi => hxL ⟨i, hi⟩ have hsum : (∑ i, if |W n (x i)| < δ then W n (x i) ^ 2 else 0) = ∑ i, W n (x i) ^ 2 := by apply Finset.sum_congr rfl intro i _ simp [hall i] rw [hsum] have htri := abs_sub_le (∑ i, W n (x i) ^ 2) (a n) q change ε ≤ |(∑ i, W n (x i) ^ 2) - q| at hx dsimp [t] at * nlinarith have hL : μn.real L ≤ (δ ^ 2)⁻¹ * r n := by dsimp [μn, L] calc (Measure.pi (fun _ : Fin n => P)).real {x | ∃ i, δ ≤ |W n (x i)|} ≤ (n : ℝ) * (δ ^ 2)⁻¹ * ∫ x in {x | δ ≤ |W n x|}, W n x ^ 2 ∂P := iid_large_coordinate_measureReal_le P (W n) (hW n) (hW2 n) n hδ _ = (δ ^ 2)⁻¹ * r n := by dsimp [r]; ring have hD_enn := iid_truncated_sq_deviation_le P (W n) (hW n) (hW2 n) n hδ ht have hD : μn.real D ≤ (b n * δ ^ 2) / t ^ 2 := by change (μn D).toReal ≤ (b n * δ ^ 2) / t ^ 2 have hh := (ENNReal.toReal_le_toReal (measure_ne_top μn D) ENNReal.ofReal_ne_top).2 hD_enn rw [ENNReal.toReal_ofReal] at hh · calc (μn D).toReal ≤ ((n : ℝ) * δ ^ 2 * ∫ y, W n y ^ 2 ∂P) / t ^ 2 := hh _ = (b n * δ ^ 2) / t ^ 2 := by dsimp [b]; ring · positivity have hdevsmall : (b n * δ ^ 2) / t ^ 2 < ρ / 4 := by have hnonneg : 0 ≤ b n := by dsimp [b] positivity dsimp [δ] field_simp nlinarith [sq_nonneg ρ, mul_nonneg hnonneg (sq_nonneg ρ)] have htotal : μn.real {x | ε ≤ |(∑ i, W n (x i) ^ 2) - q|} < η := by calc μn.real {x | ε ≤ |(∑ i, W n (x i) ^ 2) - q|} ≤ μn.real (L ∪ D) := measureReal_mono hsubset _ ≤ μn.real L + μn.real D := measureReal_union_le _ _ _ ≤ (δ ^ 2)⁻¹ * r n + (b n * δ ^ 2) / t ^ 2 := add_le_add hL hD _ < ρ / 4 + ρ / 4 := add_lt_add hnlarge hdevsmall _ ≤ η := by linarith simpa [μn, Real.dist_eq, abs_of_nonneg measureReal_nonneg] using htotal exact (ENNReal.tendsto_toReal_zero_iff (fun n => measure_ne_top (Measure.pi (fun _ : Fin n => P)) {x | ε ≤ |(∑ i, W n (x i) ^ 2) - q|})).1 hreal
Variance 1 core · 6 supporting This module derives the scalar asymptotic variance lower bound from convolution factorization. ★ regular_asymptoticVariance_ge_gradientNormSq
Variance consequence of the scalar convolution theorem
This module derives the scalar asymptotic variance lower bound from convolution factorization. The only finiteness hypothesis is a finite second moment of the estimator limit. In particular, finite variance of the residual is derived from the factorization rather than assumed.
theorem regular_asymptoticVariance_ge_gradientNormSq reviewed
⚑ flagged
Causalean.Estimation.Efficiency.AsymptoticLanConvolution
In a finite-dimensional experiment with local asymptotic normality, a regular scalar estimator, a canonical-gradient representation, and a finite second moment for its limit law, the limit variance is at least the squared canonical-gradient norm.
Formal statement
hypotheses
Ω :
ℕ → Type*
∀ n, MeasurableSpace (Ω n)
H :
K :
E :
LocalExperiment Ω H
centralSequence :
(n : ℕ) → Ω n → H
information :
BilinForm ℝ H
statistic :
(n : ℕ) → Ω n → ℝ
targetDerivative :
H →ₗ[ℝ] ℝ
scoreMap :
H →ₗ[ℝ] K
gradient :
K
limitLaw :
Measure ℝ
scoreLimit :
Measure H
lan :
IsLAN E centralSequence information scoreLimit
regular :
IsRegularEstimator E statistic targetDerivative limitLaw
canonical :
CanonicalGradientPairing information targetDerivative scoreMap gradient
hfinite :
MemLp id 2 limitLaw
conclusion
‖gradient‖ ^ 2 ≤ variance id limitLaw
Proof (Lean source)
theorem regular_asymptoticVariance_ge_gradientNormSq
{Ω : ℕ → Type*} [∀ n, MeasurableSpace (Ω n)]
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
[FiniteDimensional ℝ H] [MeasurableSpace H] [BorelSpace H]
{K : Type*} [NormedAddCommGroup K] [InnerProductSpace ℝ K]
{E : LocalExperiment Ω H} {centralSequence : (n : ℕ) → Ω n → H}
{information : BilinForm ℝ H}
{statistic : (n : ℕ) → Ω n → ℝ} {targetDerivative : H →ₗ[ℝ] ℝ}
{scoreMap : H →ₗ[ℝ] K} {gradient : K} {limitLaw : Measure ℝ}
{scoreLimit : Measure H}
(lan : IsLAN E centralSequence information scoreLimit)
(regular : IsRegularEstimator E statistic targetDerivative limitLaw)
(canonical : CanonicalGradientPairing information targetDerivative scoreMap gradient)
(hfinite : MemLp id 2 limitLaw) :
‖gradient‖ ^ 2 ≤ variance id limitLaw := by
-- Obtain the residual factorization from `regular_convolution_limit`, install the probability
-- instance for `limitLaw` from regularity, and invoke the factorization variance lemma.
obtain ⟨residualLaw, hresidualProbability, hfactor⟩ :=
regular_convolution_limit lan regular canonical
let _ : IsProbabilityMeasure limitLaw := regular.limit_probability
let _ : IsProbabilityMeasure residualLaw := hresidualProbability
exact asymptoticVariance_ge_gradientNormSq_of_factorization
gradient limitLaw residualLaw hfactor hfinite
6 supporting declarations (lemmas, instances)
-
memLp_two_right_of_convtheorem — If the convolution of two probability laws has a finite second moment and the left law has a finite second moment, then the right law also has a finite second moment.Proof (Lean source)
theorem memLp_two_right_of_conv (μ ν : Measure ℝ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hμ : MemLp id 2 μ) (hconv : MemLp id 2 (μ.conv ν)) : MemLp id 2 ν := by -- Realize convolution as the law of `x+y` under `μ.prod ν`; since `y=(x+y)-x`, pull -- `MemLp` across the relevant measure maps and use closure under subtraction. unfold Measure.conv at hconv have hsum : MemLp (fun z : ℝ × ℝ => z.1 + z.2) 2 (μ.prod ν) := by have h := (memLp_map_measure_iff (g := id) (f := fun z : ℝ × ℝ => z.1 + z.2) (μ := μ.prod ν) (by fun_prop) (by fun_prop)).1 hconv simpa [Function.comp_def] using h have hfst : MemLp (fun z : ℝ × ℝ => z.1) 2 (μ.prod ν) := by simpa using hμ.comp_fst ν have hsnd : MemLp (fun z : ℝ × ℝ => z.2) 2 (μ.prod ν) := by convert hsum.sub hfst using 1 ext z dsimp ring have hmap : MemLp id 2 (Measure.map snd (μ.prod ν)) := by apply (memLp_map_measure_iff (g := id) (f := snd) (μ := μ.prod ν) (by fun_prop) (by fun_prop)).2 simpa [Function.comp_def] using hsnd rw [measurePreserving_snd.map_eq] at hmap exact hmap -
variance_id_convtheorem — For probability laws with finite second moments, the variance of their convolution is the sum of their variances.hypothesesProof (Lean source)
theorem variance_id_conv (μ ν : Measure ℝ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hμ : MemLp id 2 μ) (hν : MemLp id 2 ν) : variance id (μ.conv ν) = variance id μ + variance id ν := by -- Represent the convolution by coordinate addition on `μ.prod ν` and apply -- `ProbabilityTheory.variance_add_prod` plus `HasLaw.variance_eq`. unfold Measure.conv calc variance id (Measure.map (fun z : ℝ × ℝ => z.1 + z.2) (μ.prod ν)) = variance (id ∘ fun z : ℝ × ℝ => z.1 + z.2) (μ.prod ν) := variance_map (X := id) (Y := fun z : ℝ × ℝ => z.1 + z.2) (μ := μ.prod ν) (by fun_prop) (by fun_prop) _ = variance id μ + variance id ν := by simpa [Function.comp_def] using (ProbabilityTheory.variance_add_prod (X := id) (Y := id) hμ hν) -
efficientGaussianLaw_memLp_twotheorem — The efficient centered Gaussian law has a finite second moment.Proof (Lean source)
theorem efficientGaussianLaw_memLp_two {K : Type*} [NormedAddCommGroup K] (gradient : K) : MemLp id 2 (efficientGaussianLaw gradient) := by -- Unfold to `gaussianReal` and use the Gaussian finite-moment theorem. unfold efficientGaussianLaw exact ProbabilityTheory.memLp_id_gaussianReal 2 -
efficientGaussianLaw_variancetheorem — The variance of the efficient centered Gaussian law is exactly the squared norm of the canonical gradient.hypothesesK :Type*gradient :Kconclusionvariance id (efficientGaussianLaw gradient) = ‖gradient‖ ^ 2Proof (Lean source)
theorem efficientGaussianLaw_variance {K : Type*} [NormedAddCommGroup K] (gradient : K) : variance id (efficientGaussianLaw gradient) = ‖gradient‖ ^ 2 := by -- Apply `ProbabilityTheory.variance_id_gaussianReal` and simplify `toNNReal` using -- nonnegativity of the squared norm. simp [efficientGaussianLaw] -
asymptoticVariance_ge_gradientNormSq_of_factorizationtheorem — Variance bound from convolution. If a probability limit law with finite second moment factors as the convolution of the efficient N(0, ‖gradient‖²) law and a residual probability law, then its variance is at least ‖gradient‖².hypothesesK :Type*gradient :KlimitLaw residualLaw :hfactor :limitLaw = (efficientGaussianLaw gradient).conv residualLawhfinite :MemLp id 2 limitLawconclusion‖gradient‖ ^ 2 ≤ variance id limitLawProof (Lean source)
theorem asymptoticVariance_ge_gradientNormSq_of_factorization {K : Type*} [NormedAddCommGroup K] (gradient : K) (limitLaw residualLaw : Measure ℝ) [IsProbabilityMeasure limitLaw] [IsProbabilityMeasure residualLaw] (hfactor : limitLaw = (efficientGaussianLaw gradient).conv residualLaw) (hfinite : MemLp id 2 limitLaw) : ‖gradient‖ ^ 2 ≤ variance id limitLaw := by -- Rewrite by `hfactor`, derive residual `MemLp` with `memLp_two_right_of_conv`, expand -- variance with `variance_id_conv`, and use nonnegativity of variance. have hefficient := efficientGaussianLaw_memLp_two gradient have hconvFinite : MemLp id 2 ((efficientGaussianLaw gradient).conv residualLaw) := by simpa [hfactor] using hfinite have hresidual := memLp_two_right_of_conv (efficientGaussianLaw gradient) residualLaw hefficient hconvFinite rw [hfactor, variance_id_conv _ _ hefficient hresidual, efficientGaussianLaw_variance] exact le_add_of_nonneg_right (variance_nonneg _ _) -
variance_ge_gradientNormSq_of_dense_scorestheorem — Compatibility with a paper's tangent-density argument: if every finite score collection gives a variance lower bound for an approximating gradient and those gradients converge in norm to the canonical gradient, then the limiting variance is bounded below by the full gradient norm.hypothesesK :gradient :KfiniteGradient :ℕ → Kv :ℝhfiniteBound :∀ j, ‖finiteGradient j‖ ^ 2 ≤ vconclusion‖gradient‖ ^ 2 ≤ vProof (Lean source)
theorem variance_ge_gradientNormSq_of_dense_scores {K : Type*} [NormedAddCommGroup K] [NormedSpace ℝ K] (gradient : K) (finiteGradient : ℕ → K) (v : ℝ) (hfiniteBound : ∀ j, ‖finiteGradient j‖ ^ 2 ≤ v) (hdense : Tendsto finiteGradient atTop (𝓝 gradient)) : ‖gradient‖ ^ 2 ≤ v := by -- Continuity of `x ↦ ‖x‖²` gives convergence of the left sides; pass the pointwise -- inequalities to the limit through the closed interval `Iic v`. apply le_of_tendsto ((continuous_norm.pow 2).continuousAt.tendsto.comp hdense) exact Filter.Eventually.of_forall hfiniteBound