Stat.Limit.Observation­Dependent­Van­Trees

theorem priorInformation_smoothPrior {ell u c a : ℝ} (ha : 0 < a) (hleft : ell ≤ c - a) (hright : c + a ≤ u) : priorInformation ell u (smoothPrior c a) (smoothPriorDeriv c a) = 10 / a ^ 2 := by unfold priorInformation rw [smoothPrior_scoreSq_eq_indicator ha] unfold parameterMeasure rw [← integral_indicator measurableSet_Icc] have hfun : (Icc ell u).indicator ((Ioo (c - a) (c + a)).indicator (fun θ => (15 / a ^ 5) * (θ - c) ^ 2)) = (Ioo (c - a) (c + a)).indicator (fun θ => (15 / a ^ 5) * (θ - c) ^ 2) := by funext θ by_cases hθ : θ ∈ Ioo (c - a) (c + a) · have hambient : θ ∈ Icc ell u := ⟨hleft.trans hθ.1.le, hθ.2.le.trans hright⟩ simp [hθ, hambient] · simp [hθ] rw [hfun, integral_indicator measurableSet_Ioo] rw [← integral_Ioc_eq_integral_Ioo] rw [← intervalIntegral.integral_of_le (by linarith : c - a ≤ c + a)] let f : ℝ → ℝ := fun x => (15 / a ^ 3) * x ^ 2 have hf : (∫ x : ℝ in (-1)..1, f x) = 10 / a ^ 3 := by dsimp [f] rw [intervalIntegral.integral_const_mul, integral_pow] norm_num field_simp [ha.ne'] norm_num have hcomp := intervalIntegral.integral_comp_div_sub (a := c - a) (b := c + a) f ha.ne' (c / a) have heq : (∫ θ in c - a..c + a, (15 / a ^ 5) * (θ - c) ^ 2) = a * (∫ x in (-1)..1, f x) := by rw [show (fun θ : ℝ => (15 / a ^ 5) * (θ - c) ^ 2) = fun θ => f (θ / a - c / a) by funext θ dsimp [f] field_simp [ha.ne']] rw [hcomp] congr 2 <;> field_simp [ha.ne'] <;> ring rw [heq, hf] field_simp [ha.ne']

theorem joint_score_information_decomposition {X : Type*} [MeasurableSpace X] {μ : Measure X} [SigmaFinite μ] {a b : ℝ} {w dw : ℝ → ℝ} {p dp : ℝ → X → ℝ} (hw : ∀ θ, 0 ≤ w θ) (hp : ∀ θ x, 0 ≤ p θ x) (hwzero : ∀ᵐ θ ∂parameterMeasure a b, w θ = 0 → dw θ = 0) (hpzero : ∀ᵐ z ∂((parameterMeasure a b).prod μ), p z.1 z.2 = 0 → dp z.1 z.2 = 0) (hnorm : ∀ᵐ θ ∂parameterMeasure a b, ∫ x, p θ x ∂μ = 1) (hcenter : ∀ᵐ θ ∂parameterMeasure a b, ∫ x, likelihoodScore p dp θ x * p θ x ∂μ = 0) (hscoreSm : AEStronglyMeasurable (scoreSqField w dw p dp) ((parameterMeasure a b).prod μ)) (hscoreInt : Integrable (scoreSqField w dw p dp) ((parameterMeasure a b).prod μ)) (hpriorSm : AEStronglyMeasurable (fun θ => w θ * (priorScore w dw θ) ^ 2) (parameterMeasure a b)) (hpriorInt : Integrable (fun θ => w θ * (priorScore w dw θ) ^ 2) (parameterMeasure a b)) (hpriorJointSm : AEStronglyMeasurable (fun z : ℝ × X => w z.1 * p z.1 z.2 * (priorScore w dw z.1) ^ 2) ((parameterMeasure a b).prod μ)) (hpriorJointInt : Integrable (fun z : ℝ × X => w z.1 * p z.1 z.2 * (priorScore w dw z.1) ^ 2) ((parameterMeasure a b).prod μ)) (hfisherSm : AEStronglyMeasurable (fun z : ℝ × X => w z.1 * p z.1 z.2 * (likelihoodScore p dp z.1 z.2) ^ 2) ((parameterMeasure a b).prod μ)) (hfisherInt : Integrable (fun z : ℝ × X => w z.1 * p z.1 z.2 * (likelihoodScore p dp z.1 z.2) ^ 2) ((parameterMeasure a b).prod μ)) (hcrossSm : AEStronglyMeasurable (fun z : ℝ × X => w z.1 * p z.1 z.2 * (priorScore w dw z.1 * likelihoodScore p dp z.1 z.2)) ((parameterMeasure a b).prod μ)) (hcrossInt : Integrable (fun z : ℝ × X => w z.1 * p z.1 z.2 * (priorScore w dw z.1 * likelihoodScore p dp z.1 z.2)) ((parameterMeasure a b).prod μ)) : ∫ z, scoreSqField w dw p dp z ∂((parameterMeasure a b).prod μ) = priorInformation a b w dw + ∫ θ, w θ * fisherInformation μ p dp θ ∂parameterMeasure a b := by letI : IsFiniteMeasure (parameterMeasure a b) := by unfold parameterMeasure infer_instance have hscore_expand (θ : ℝ) (x : X) : scoreSqField w dw p dp (θ, x) = w θ * p θ x * (priorScore w dw θ) ^ 2 + (w θ * p θ x * (likelihoodScore p dp θ x) ^ 2 + 2 * (w θ * p θ x * (priorScore w dw θ * likelihoodScore p dp θ x))) := by by_cases hwpos : 0 < w θ · by_cases hppos : 0 < p θ x · simp only [scoreSqField, jointScore, jointDensity, priorScore, likelihoodScore, hwpos, hppos, mul_pos, if_true] field_simp ring · have hpz : p θ x = 0 := le_antisymm (le_of_not_gt hppos) (hp θ x) simp [scoreSqField, jointScore, jointDensity, hpz] · have hwz : w θ = 0 := le_antisymm (le_of_not_gt hwpos) (hw θ) simp [scoreSqField, jointScore, jointDensity, hwz] have hsplit : (∫ z, scoreSqField w dw p dp z ∂((parameterMeasure a b).prod μ)) = (∫ z : ℝ × X, w z.1 * p z.1 z.2 * (priorScore w dw z.1) ^ 2 ∂((parameterMeasure a b).prod μ)) + (∫ z : ℝ × X, w z.1 * p z.1 z.2 * (likelihoodScore p dp z.1 z.2) ^ 2 ∂((parameterMeasure a b).prod μ)) + 2 * (∫ z : ℝ × X, w z.1 * p z.1 z.2 * (priorScore w dw z.1 * likelihoodScore p dp z.1 z.2) ∂((parameterMeasure a b).prod μ)) := by calc _ = ∫ z : ℝ × X, (w z.1 * p z.1 z.2 * (priorScore w dw z.1) ^ 2) + ((w z.1 * p z.1 z.2 * (likelihoodScore p dp z.1 z.2) ^ 2) + 2 * (w z.1 * p z.1 z.2 * (priorScore w dw z.1 * likelihoodScore p dp z.1 z.2))) ∂((parameterMeasure a b).prod μ) := by apply integral_congr_ae filter_upwards with z exact hscore_expand z.1 z.2 _ = (∫ z : ℝ × X, w z.1 * p z.1 z.2 * (priorScore w dw z.1) ^ 2 ∂((parameterMeasure a b).prod μ)) + ∫ z : ℝ × X, (w z.1 * p z.1 z.2 * (likelihoodScore p dp z.1 z.2) ^ 2) + 2 * (w z.1 * p z.1 z.2 * (priorScore w dw z.1 * likelihoodScore p dp z.1 z.2)) ∂((parameterMeasure a b).prod μ) := integral_add hpriorJointInt (hfisherInt.add (hcrossInt.const_mul 2)) _ = _ := by rw [integral_add hfisherInt (hcrossInt.const_mul 2), integral_const_mul] ring have hprior_eval : (∫ z : ℝ × X, w z.1 * p z.1 z.2 * (priorScore w dw z.1) ^ 2 ∂((parameterMeasure a b).prod μ)) = priorInformation a b w dw := by rw [integral_prod _ hpriorJointInt] unfold priorInformation apply integral_congr_ae filter_upwards [hnorm] with θ hnormθ calc (∫ x, w θ * p θ x * (priorScore w dw θ) ^ 2 ∂μ) = ∫ x, (w θ * (priorScore w dw θ) ^ 2) * p θ x ∂μ := by apply integral_congr_ae filter_upwards with x ring _ = (w θ * (priorScore w dw θ) ^ 2) * ∫ x, p θ x ∂μ := integral_const_mul (w θ * (priorScore w dw θ) ^ 2) (fun x => p θ x) _ = w θ * (priorScore w dw θ) ^ 2 := by rw [hnormθ]; ring have hfisher_eval : (∫ z : ℝ × X, w z.1 * p z.1 z.2 * (likelihoodScore p dp z.1 z.2) ^ 2 ∂((parameterMeasure a b).prod μ)) = ∫ θ, w θ * fisherInformation μ p dp θ ∂parameterMeasure a b := by rw [integral_prod _ hfisherInt] apply integral_congr_ae filter_upwards with θ unfold fisherInformation calc (∫ x, w θ * p θ x * (likelihoodScore p dp θ x) ^ 2 ∂μ) = ∫ x, w θ * (p θ x * (likelihoodScore p dp θ x) ^ 2) ∂μ := by apply integral_congr_ae filter_upwards with x ring _ = w θ * ∫ x, p θ x * (likelihoodScore p dp θ x) ^ 2 ∂μ := integral_const_mul (w θ) (fun x => p θ x * (likelihoodScore p dp θ x) ^ 2) have hcross_eval : (∫ z : ℝ × X, w z.1 * p z.1 z.2 * (priorScore w dw z.1 * likelihoodScore p dp z.1 z.2) ∂((parameterMeasure a b).prod μ)) = 0 := by rw [integral_prod _ hcrossInt] have hinner : ∀ᵐ θ ∂parameterMeasure a b, (∫ x, w θ * p θ x * (priorScore w dw θ * likelihoodScore p dp θ x) ∂μ) = 0 := by filter_upwards [hcenter] with θ hcenterθ calc (∫ x, w θ * p θ x * (priorScore w dw θ * likelihoodScore p dp θ x) ∂μ) = ∫ x, (w θ * priorScore w dw θ) * (likelihoodScore p dp θ x * p θ x) ∂μ := by apply integral_congr_ae filter_upwards with x ring _ = (w θ * priorScore w dw θ) * ∫ x, likelihoodScore p dp θ x * p θ x ∂μ := integral_const_mul (w θ * priorScore w dw θ) (fun x => likelihoodScore p dp θ x * p θ x) _ = 0 := by rw [hcenterθ, mul_zero] calc (∫ θ, ∫ x, w θ * p θ x * (priorScore w dw θ * likelihoodScore p dp θ x) ∂μ ∂parameterMeasure a b) = ∫ _θ : ℝ, 0 ∂parameterMeasure a b := integral_congr_ae hinner _ = 0 := by simp rw [hsplit, hprior_eval, hfisher_eval, hcross_eval] ring

theorem average_fisherInformation_le {X : Type*} [MeasurableSpace X] {μ : Measure X} {ell u I : ℝ} {w : ℝ → ℝ} {p dp : ℝ → X → ℝ} (hw_nonneg : ∀ θ, 0 ≤ w θ) (hw_norm : ∫ θ, w θ ∂parameterMeasure ell u = 1) (hw_int : Integrable w (parameterMeasure ell u)) (hweighted_int : Integrable (fun θ => w θ * fisherInformation μ p dp θ) (parameterMeasure ell u)) (hpointwise : ∀ θ, 0 < w θ → fisherInformation μ p dp θ ≤ I) : ∫ θ, w θ * fisherInformation μ p dp θ ∂parameterMeasure ell u ≤ I := by calc ∫ θ, w θ * fisherInformation μ p dp θ ∂parameterMeasure ell u ≤ ∫ θ, w θ * I ∂parameterMeasure ell u := by apply integral_mono hweighted_int (hw_int.mul_const I) intro θ by_cases hwpos : 0 < w θ · exact mul_le_mul_of_nonneg_left (hpointwise θ hwpos) (hw_nonneg θ) · have hwzero : w θ = 0 := le_antisymm (le_of_not_gt hwpos) (hw_nonneg θ) simp [hwzero] _ = (∫ θ, w θ ∂parameterMeasure ell u) * I := integral_mul_const I w _ = I := by rw [hw_norm, one_mul]

theorem product_integral_derivativeBalance_eq_zero {X : Type*} [MeasurableSpace X] {μ : Measure X} [SigmaFinite μ] {a b : ℝ} (hab : a ≤ b) {w dw : ℝ → ℝ} {p dp g dg : ℝ → X → ℝ} {T : X → ℝ} (hw : AbsolutelyContinuousOnInterval w a b) (hp : ∀ᵐ x ∂μ, AbsolutelyContinuousOnInterval (fun θ => p θ x) a b) (hg : ∀ᵐ x ∂μ, AbsolutelyContinuousOnInterval (fun θ => g θ x) a b) (hdw : ∀ᵐ θ ∂parameterMeasure a b, HasDerivAt w (dw θ) θ) (hdp : ∀ᵐ x ∂μ, ∀ᵐ θ ∂parameterMeasure a b, HasDerivAt (fun t => p t x) (dp θ x) θ) (hdg : ∀ᵐ x ∂μ, ∀ᵐ θ ∂parameterMeasure a b, HasDerivAt (fun t => g t x) (dg θ x) θ) (hboundary : ∀ᵐ x ∂μ, w b * p b x * (T x - g b x) = 0 ∧ w a * p a x * (T x - g a x) = 0) (hsm : AEStronglyMeasurable (derivativeBalanceField w dw p dp g dg T) ((parameterMeasure a b).prod μ)) (hint : Integrable (derivativeBalanceField w dw p dp g dg T) ((parameterMeasure a b).prod μ)) : ∫ z, derivativeBalanceField w dw p dp g dg T z ∂((parameterMeasure a b).prod μ) = 0 := by letI : IsFiniteMeasure (parameterMeasure a b) := by unfold parameterMeasure infer_instance rw [integral_prod_symm _ hint] apply integral_eq_zero_of_ae filter_upwards [hp, hg, hdp, hdg, hboundary, hint.prod_left_ae] with x hpx hgx hdpx hdgx hboundaryx hintx let q : ℝ → ℝ := fun θ => w θ * p θ x * (T x - g θ x) have hconst : AbsolutelyContinuousOnInterval (fun _ : ℝ => T x) a b := by rw [absolutelyContinuousOnInterval_iff] intro ε hε exact ⟨1, zero_lt_one, by intros; simpa using hε⟩ have hq : AbsolutelyContinuousOnInterval q a b := (hw.fun_mul hpx).fun_mul (hconst.sub hgx) have hqderiv : ∀ᵐ θ ∂parameterMeasure a b, HasDerivAt q (derivativeBalanceField w dw p dp g dg T (θ, x)) θ := by filter_upwards [hdw, hdpx, hdgx] with θ hdwθ hdpθ hdgθ have hmul := (hdwθ.mul hdpθ).mul (hdgθ.const_sub (T x)) simp only [Pi.mul_apply] at hmul have hder : (dw θ * p θ x + w θ * dp θ x) * (T x - g θ x) + w θ * p θ x * -dg θ x = derivativeBalanceField w dw p dp g dg T (θ, x) := by simp only [derivativeBalanceField, jointDensity] ring rw [hder] at hmul exact hmul calc ∫ θ, derivativeBalanceField w dw p dp g dg T (θ, x) ∂parameterMeasure a b = ∫ θ, deriv q θ ∂parameterMeasure a b := by apply MeasureTheory.integral_congr_ae filter_upwards [hqderiv] with θ hθ exact hθ.deriv.symm _ = ∫ θ in a..b, deriv q θ := by rw [intervalIntegral.integral_of_le hab, parameterMeasure, restrict_Ioc_eq_restrict_Icc] _ = q b - q a := hq.integral_deriv_eq_sub _ = 0 := by simp [q, hboundaryx.1, hboundaryx.2]

theorem observation_dependent_van_trees {X : Type*} [MeasurableSpace X] (μ : Measure X) [SigmaFinite μ] {ell u : ℝ} (hellu : ell < u) (w dw : ℝ → ℝ) (p dp g dg : ℝ → X → ℝ) (T : X → ℝ) -- Compactly supported C1 prior density and derivative representative. (hwC1 : ContDiff ℝ 1 w) (hwsupport : support w ⊆ Icc ell u) (hwderiv : ∀ θ, HasDerivAt w (dw θ) θ) (hwnonneg : ∀ θ, 0 ≤ w θ) (hwnorm : ∫ θ, w θ ∂parameterMeasure ell u = 1) -- Dominated likelihood density and normalization. (hpnonneg : ∀ θ x, 0 ≤ p θ x) (hpnorm : ∀ θ ∈ Icc ell u, ∫ x, p θ x ∂μ = 1) (hpint : ∀ θ ∈ Icc ell u, Integrable (fun x => p θ x) μ) (hdpint : ∀ θ ∈ Icc ell u, Integrable (fun x => dp θ x) μ) (hdiffUnder : ∀ θ ∈ Ioo ell u, HasDerivAt (fun t => ∫ x, p t x ∂μ) (∫ x, dp θ x ∂μ) θ) -- Absolute continuity of observation sections and joint-a.e. derivative representatives. (hpAC : ∀ᵐ x ∂μ, AbsolutelyContinuousOnInterval (fun θ => p θ x) ell u) (hgAC : ∀ᵐ x ∂μ, AbsolutelyContinuousOnInterval (fun θ => g θ x) ell u) (hdp : ∀ᵐ z ∂((parameterMeasure ell u).prod μ), HasDerivAt (fun t => p t z.2) (dp z.1 z.2) z.1) (hdg : ∀ᵐ z ∂((parameterMeasure ell u).prod μ), HasDerivAt (fun t => g t z.2) (dg z.1 z.2) z.1) -- Boundary product required by integration by parts. (hboundary : ∀ᵐ x ∂μ, w u * p u x * (T x - g u x) = 0 ∧ w ell * p ell x * (T x - g ell x) = 0) -- Explicit product-measure measurability and integrability of signed fields. (hbalanceSm : AEStronglyMeasurable (derivativeBalanceField w dw p dp g dg T) ((parameterMeasure ell u).prod μ)) (hbalanceInt : Integrable (derivativeBalanceField w dw p dp g dg T) ((parameterMeasure ell u).prod μ)) (herrorScoreSm : AEStronglyMeasurable (errorScoreField w dw p dp g T) ((parameterMeasure ell u).prod μ)) (herrorScoreInt : Integrable (errorScoreField w dw p dp g T) ((parameterMeasure ell u).prod μ)) (hsensitivitySm : AEStronglyMeasurable (sensitivityField w p dg) ((parameterMeasure ell u).prod μ)) (hsensitivityInt : Integrable (sensitivityField w p dg) ((parameterMeasure ell u).prod μ)) -- Explicit product-measure weighted-square and cross-integrability hypotheses. (herrorSqSm : AEStronglyMeasurable (errorSqField w p g T) ((parameterMeasure ell u).prod μ)) (herrorSqInt : Integrable (errorSqField w p g T) ((parameterMeasure ell u).prod μ)) (hscoreSqSm : AEStronglyMeasurable (scoreSqField w dw p dp) ((parameterMeasure ell u).prod μ)) (hscoreSqInt : Integrable (scoreSqField w dw p dp) ((parameterMeasure ell u).prod μ)) (hpriorSqSm : AEStronglyMeasurable (fun θ => w θ * (priorScore w dw θ) ^ 2) (parameterMeasure ell u)) (hpriorSqInt : Integrable (fun θ => w θ * (priorScore w dw θ) ^ 2) (parameterMeasure ell u)) (hpriorJointSqSm : AEStronglyMeasurable (fun z : ℝ × X => w z.1 * p z.1 z.2 * (priorScore w dw z.1) ^ 2) ((parameterMeasure ell u).prod μ)) (hpriorJointSqInt : Integrable (fun z : ℝ × X => w z.1 * p z.1 z.2 * (priorScore w dw z.1) ^ 2) ((parameterMeasure ell u).prod μ)) (hfisherSqSm : AEStronglyMeasurable (fun z : ℝ × X => w z.1 * p z.1 z.2 * (likelihoodScore p dp z.1 z.2) ^ 2) ((parameterMeasure ell u).prod μ)) (hfisherSqInt : Integrable (fun z : ℝ × X => w z.1 * p z.1 z.2 * (likelihoodScore p dp z.1 z.2) ^ 2) ((parameterMeasure ell u).prod μ)) (hcrossSm : AEStronglyMeasurable (fun z : ℝ × X => w z.1 * p z.1 z.2 * (priorScore w dw z.1 * likelihoodScore p dp z.1 z.2)) ((parameterMeasure ell u).prod μ)) (hcrossInt : Integrable (fun z : ℝ × X => w z.1 * p z.1 z.2 * (priorScore w dw z.1 * likelihoodScore p dp z.1 z.2)) ((parameterMeasure ell u).prod μ)) -- Positive finite total prior-plus-Fisher information. (hinfoPos : 0 < priorInformation ell u w dw + ∫ θ, w θ * fisherInformation μ p dp θ ∂parameterMeasure ell u) : (∫ z, sensitivityField w p dg z ∂((parameterMeasure ell u).prod μ)) ^ 2 / (priorInformation ell u w dw + ∫ θ, w θ * fisherInformation μ p dp θ ∂parameterMeasure ell u) ≤ ∫ z, errorSqField w p g T z ∂((parameterMeasure ell u).prod μ) := by -- Proof roadmap for the filler: -- 1. Obtain absolute continuity of `w` from `hwC1`, and obtain derivative-zero -- facts for `w` and (joint-a.e.) `p` from global nonnegativity. -- 2. Transport `hdp` and `hdg` across `Measure.measurePreserving_swap`, then use -- `ae_ae_of_ae_prod` to feed observation-first sections to -- `product_integral_derivativeBalance_eq_zero`. -- 3. Expand `errorScoreField` with `errorScoreField_eq_numerator`; the zero -- derivative-balance integral identifies its integral with sensitivity. -- 4. Exclude the two endpoints almost everywhere under `parameterMeasure`, -- derive likelihood-score centering, and invoke -- `joint_score_information_decomposition`. -- 5. Apply `weighted_integral_mul_sq_le` on the product measure with weight -- `jointDensity`, error `T - g`, and score `jointScore`, then divide by the -- strictly positive information denominator. letI : IsFiniteMeasure (parameterMeasure ell u) := by unfold parameterMeasure infer_instance have hwAC : AbsolutelyContinuousOnInterval w ell u := hwC1.contDiffOn.absolutelyContinuousOnInterval have hdw : ∀ᵐ θ ∂parameterMeasure ell u, HasDerivAt w (dw θ) θ := by filter_upwards with θ exact hwderiv θ have hwzero : ∀ θ, w θ = 0 → dw θ = 0 := by intro θ hzero exact derivative_eq_zero_of_nonnegative_of_eq_zero hwnonneg (hwderiv θ) hzero have hpzero : ∀ᵐ z ∂((parameterMeasure ell u).prod μ), p z.1 z.2 = 0 → dp z.1 z.2 = 0 := by filter_upwards [hdp] with z hdpz intro hzero exact derivative_eq_zero_of_nonnegative_of_eq_zero (fun t => hpnonneg t z.2) hdpz hzero have hdpSwap : ∀ᵐ z ∂(μ.prod (parameterMeasure ell u)), HasDerivAt (fun t => p t z.1) (dp z.2 z.1) z.2 := by have h := Measure.measurePreserving_swap.quasiMeasurePreserving.tendsto_ae.eventually hdp simpa [swap] using h have hdgSwap : ∀ᵐ z ∂(μ.prod (parameterMeasure ell u)), HasDerivAt (fun t => g t z.1) (dg z.2 z.1) z.2 := by have h := Measure.measurePreserving_swap.quasiMeasurePreserving.tendsto_ae.eventually hdg simpa [swap] using h have hdpSections : ∀ᵐ x ∂μ, ∀ᵐ θ ∂parameterMeasure ell u, HasDerivAt (fun t => p t x) (dp θ x) θ := by simpa using Measure.ae_ae_of_ae_prod hdpSwap have hdgSections : ∀ᵐ x ∂μ, ∀ᵐ θ ∂parameterMeasure ell u, HasDerivAt (fun t => g t x) (dg θ x) θ := by simpa using Measure.ae_ae_of_ae_prod hdgSwap have hbalanceZero : ∫ z, derivativeBalanceField w dw p dp g dg T z ∂((parameterMeasure ell u).prod μ) = 0 := product_integral_derivativeBalance_eq_zero hellu.le hwAC hpAC hgAC hdw hdpSections hdgSections hboundary hbalanceSm hbalanceInt have herrorSensitivity : (∫ z, errorScoreField w dw p dp g T z ∂((parameterMeasure ell u).prod μ)) = ∫ z, sensitivityField w p dg z ∂((parameterMeasure ell u).prod μ) := by have hbalanceRewrite : (∫ z, derivativeBalanceField w dw p dp g dg T z ∂((parameterMeasure ell u).prod μ)) = (∫ z, errorScoreField w dw p dp g T z ∂((parameterMeasure ell u).prod μ)) - ∫ z, sensitivityField w p dg z ∂((parameterMeasure ell u).prod μ) := by calc _ = ∫ z, errorScoreField w dw p dp g T z - sensitivityField w p dg z ∂((parameterMeasure ell u).prod μ) := by apply integral_congr_ae filter_upwards [hpzero] with z hpzeroz rw [errorScoreField_eq_numerator (hwnonneg z.1) (hpnonneg z.1 z.2) (hwzero z.1) hpzeroz] simp only [derivativeBalanceField, sensitivityField, jointDensity] ring _ = _ := integral_sub herrorScoreInt hsensitivityInt rw [hbalanceZero] at hbalanceRewrite linarith have hmemIcc : ∀ᵐ θ ∂parameterMeasure ell u, θ ∈ Icc ell u := by unfold parameterMeasure exact ae_restrict_mem measurableSet_Icc have hneEll : ∀ᵐ θ ∂parameterMeasure ell u, θ ≠ ell := by unfold parameterMeasure exact ae_restrict_of_ae (volume.ae_ne ell) have hneU : ∀ᵐ θ ∂parameterMeasure ell u, θ ≠ u := by unfold parameterMeasure exact ae_restrict_of_ae (volume.ae_ne u) have hmemIoo : ∀ᵐ θ ∂parameterMeasure ell u, θ ∈ Ioo ell u := by filter_upwards [hmemIcc, hneEll, hneU] with θ hθ hθell hθu exact ⟨lt_of_le_of_ne hθ.1 (Ne.symm hθell), lt_of_le_of_ne hθ.2 hθu⟩ have hpzeroSections : ∀ᵐ θ ∂parameterMeasure ell u, ∀ᵐ x ∂μ, p θ x = 0 → dp θ x = 0 := Measure.ae_ae_of_ae_prod hpzero have hnormAE : ∀ᵐ θ ∂parameterMeasure ell u, ∫ x, p θ x ∂μ = 1 := by filter_upwards [hmemIcc] with θ hθ exact hpnorm θ hθ have hcenter : ∀ᵐ θ ∂parameterMeasure ell u, ∫ x, likelihoodScore p dp θ x * p θ x ∂μ = 0 := by filter_upwards [hmemIoo, hpzeroSections] with θ hθ hpzeroθ exact likelihoodScore_integral_eq_zero_of_normalization hθ hpnorm (hdiffUnder θ hθ) (hpnonneg θ) hpzeroθ (hpint θ ⟨hθ.1.le, hθ.2.le⟩) (hdpint θ ⟨hθ.1.le, hθ.2.le⟩) have hinformation : (∫ z, scoreSqField w dw p dp z ∂((parameterMeasure ell u).prod μ)) = priorInformation ell u w dw + ∫ θ, w θ * fisherInformation μ p dp θ ∂parameterMeasure ell u := joint_score_information_decomposition hwnonneg hpnonneg (by filter_upwards with θ; exact hwzero θ) hpzero hnormAE hcenter hscoreSqSm hscoreSqInt hpriorSqSm hpriorSqInt hpriorJointSqSm hpriorJointSqInt hfisherSqSm hfisherSqInt hcrossSm hcrossInt have hcs : (∫ z, errorScoreField w dw p dp g T z ∂((parameterMeasure ell u).prod μ)) ^ 2 ≤ (∫ z, errorSqField w p g T z ∂((parameterMeasure ell u).prod μ)) * ∫ z, scoreSqField w dw p dp z ∂((parameterMeasure ell u).prod μ) := by simpa only [errorScoreField, errorSqField, scoreSqField] using (weighted_integral_mul_sq_le (μ := (parameterMeasure ell u).prod μ) (q := jointDensity w p) (f := fun z : ℝ × X => T z.2 - g z.1 z.2) (s := jointScore w dw p dp) (by filter_upwards with z; exact mul_nonneg (hwnonneg z.1) (hpnonneg z.1 z.2)) herrorSqSm hscoreSqSm herrorScoreSm herrorSqInt hscoreSqInt herrorScoreInt) apply (div_le_iff₀ hinfoPos).2 rw [← hinformation, ← herrorSensitivity] exact hcs

theorem smoothPrior_finite_vanTrees_lower_bound {X : Type*} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] {ell u c a s I : ℝ} {p dp g dg : ℝ → X → ℝ} {T : X → ℝ} (ha : 0 < a) (hleft : ell < c - a) (hright : c + a < u) (M : FiniteVanTreesModelRegularity X ell u (smoothPrior c a) (smoothPriorDeriv c a) p dp g dg T) (hs_nonneg : 0 ≤ s) (hsensitivity : s ≤ ∫ z, sensitivityField (smoothPrior c a) p dg z ∂((parameterMeasure ell u).prod Measure.count)) (hpointwise : ∀ θ, 0 < smoothPrior c a θ → fisherInformation Measure.count p dp θ ≤ I) (hinfoPos : 0 < priorInformation ell u (smoothPrior c a) (smoothPriorDeriv c a) + ∫ θ, smoothPrior c a θ * fisherInformation Measure.count p dp θ ∂parameterMeasure ell u) : s ^ 2 / (I + 40 / a ^ 2) ≤ ∫ z, errorSqField (smoothPrior c a) p g T z ∂((parameterMeasure ell u).prod Measure.count) := by have hellu : ell < u := by linarith have hendpoints := smoothPrior_ambient_endpoints ha hleft hright have hboundary : ∀ᵐ x ∂Measure.count, smoothPrior c a u * p u x * (T x - g u x) = 0 ∧ smoothPrior c a ell * p ell x * (T x - g ell x) = 0 := by filter_upwards with x simp [hendpoints.1, hendpoints.2] have hweightedInt : Integrable (fun θ => smoothPrior c a θ * fisherInformation Measure.count p dp θ) (parameterMeasure ell u) := by have h := M.hfisherSqInt.integral_prod_left convert h using 1 funext θ rw [fisherInformation, ← integral_const_mul] congr 1 funext x ring have hlike : ∫ θ, smoothPrior c a θ * fisherInformation Measure.count p dp θ ∂parameterMeasure ell u ≤ I := average_fisherInformation_le (smoothPrior_nonneg ha) (integral_smoothPrior_parameterMeasure ha hleft.le hright.le) (smoothPrior_integrable_parameterMeasure ha) hweightedInt hpointwise exact finite_vanTrees_lower_bound hellu M (smoothPrior_contDiff ha) (support_smoothPrior_subset_Icc ha hleft hright) (hasDerivAt_smoothPrior ha) (smoothPrior_nonneg ha) (integral_smoothPrior_parameterMeasure ha hleft.le hright.le) hboundary (smoothPrior_scoreSq_aestronglyMeasurable ha) (smoothPrior_scoreSq_integrable ha) hs_nonneg hsensitivity hlike (priorInformation_smoothPrior_le ha hleft.le hright.le) hinfoPos

theorem weighted_integral_mul_sq_le {A : Type*} [MeasurableSpace A] {μ : Measure A} {q f s : A → ℝ} (hq : ∀ᵐ a ∂μ, 0 ≤ q a) (hfsm : AEStronglyMeasurable (fun a => f a ^ 2 * q a) μ) (hssm : AEStronglyMeasurable (fun a => s a ^ 2 * q a) μ) (hfssm : AEStronglyMeasurable (fun a => f a * s a * q a) μ) (hfint : Integrable (fun a => f a ^ 2 * q a) μ) (hsint : Integrable (fun a => s a ^ 2 * q a) μ) (hfsint : Integrable (fun a => f a * s a * q a) μ) : (∫ a, f a * s a * q a ∂μ) ^ 2 ≤ (∫ a, f a ^ 2 * q a ∂μ) * (∫ a, s a ^ 2 * q a ∂μ) := by have hfint' : Integrable (fun a => f a ^ 2 * q a) μ := ⟨hfsm, hfint.hasFiniteIntegral⟩ have hsint' : Integrable (fun a => s a ^ 2 * q a) μ := ⟨hssm, hsint.hasFiniteIntegral⟩ have hfsint' : Integrable (fun a => f a * s a * q a) μ := ⟨hfssm, hfsint.hasFiniteIntegral⟩ have hquad : ∀ t : ℝ, 0 ≤ (∫ a, s a ^ 2 * q a ∂μ) * (t * t) + (-2 * (∫ a, f a * s a * q a ∂μ)) * t + (∫ a, f a ^ 2 * q a ∂μ) := by intro t have hnonneg : 0 ≤ ∫ a, (f a - t * s a) ^ 2 * q a ∂μ := by apply integral_nonneg_of_ae filter_upwards [hq] with a hqa exact mul_nonneg (sq_nonneg _) hqa have hcross : Integrable (fun a => (2 * t) * (f a * s a * q a)) μ := hfsint'.const_mul (2 * t) have hsquare : Integrable (fun a => t ^ 2 * (s a ^ 2 * q a)) μ := hsint'.const_mul (t ^ 2) have hexpand : (∫ a, (f a - t * s a) ^ 2 * q a ∂μ) = (∫ a, f a ^ 2 * q a ∂μ) - (2 * t) * (∫ a, f a * s a * q a ∂μ) + t ^ 2 * (∫ a, s a ^ 2 * q a ∂μ) := by calc (∫ a, (f a - t * s a) ^ 2 * q a ∂μ) = ∫ a, (f a ^ 2 * q a) - (2 * t) * (f a * s a * q a) + t ^ 2 * (s a ^ 2 * q a) ∂μ := by apply integral_congr_ae filter_upwards with a ring _ = (∫ a, (f a ^ 2 * q a) - (2 * t) * (f a * s a * q a) ∂μ) + (∫ a, t ^ 2 * (s a ^ 2 * q a) ∂μ) := integral_add (hfint'.sub hcross) hsquare _ = ((∫ a, f a ^ 2 * q a ∂μ) - (∫ a, (2 * t) * (f a * s a * q a) ∂μ)) + (∫ a, t ^ 2 * (s a ^ 2 * q a) ∂μ) := by rw [integral_sub hfint' hcross] _ = (∫ a, f a ^ 2 * q a ∂μ) - (2 * t) * (∫ a, f a * s a * q a ∂μ) + t ^ 2 * (∫ a, s a ^ 2 * q a ∂μ) := by rw [integral_const_mul, integral_const_mul] rw [hexpand] at hnonneg nlinarith [hnonneg] have hdisc : discrim (∫ a, s a ^ 2 * q a ∂μ) (-2 * (∫ a, f a * s a * q a ∂μ)) (∫ a, f a ^ 2 * q a ∂μ) ≤ 0 := by apply discrim_le_zero intro t exact hquad t unfold discrim at hdisc nlinarith [hdisc]