module
public import Papers.TsAdaptiveEstimationInference.Helpers.TRAESetup
public import Causalean.Stat.Minimax.HellingerAffinity
/-! Density-induced regression, conditional fitting, and the recorded RDIV atoms. -/
@[expose] public section
set_option linter.unusedVariables false
set_option linter.style.longLine false
namespace Papers.TsAdaptiveEstimationInference
open MeasureTheory Filter
open scoped Topology ENNReal
variable {𝒲 𝒳 𝒵 Ω : Type*} [MeasurableSpace 𝒲] [MeasurableSpace 𝒳]
  [MeasurableSpace 𝒵] [MeasurableSpace Ω]

-- @node: def:cr-deepiv-operator
/-- For [an input measure](hyp:mu), [a conditional density](hyp:g), [a regression function](hyp:h)
and [an instrument value](hyp:z), the [density-induced prediction](goal) integrates the regression
function against that conditional density over the input measure. -/
noncomputable def densityOperator (mu : Measure 𝒳) (g : 𝒳 → 𝒵 → ℝ) -- @realizes \mu(common dominating measure on the input domain) -- @realizes \mathcal T_g(integration of h against a conditional density)
    (h : 𝒳 → ℝ) (z : 𝒵) : ℝ := ∫ x, h x * g x z ∂mu

-- @node: def:cr-deepiv-likelihood-class
/-- Given [a candidate density class](hyp:G) and [a reference density](hyp:g₀), the
[likelihood-transform class](goal) consists of the square roots of the ratios of each candidate's
average with the reference density to the reference density, evaluated at input–instrument pairs. -/
noncomputable def likelihoodTransformClass (G : Set (𝒳 → 𝒵 → ℝ)) (g₀ : 𝒳 → 𝒵 → ℝ) : -- @realizes \mathcal G_0(square-root likelihood-transform class)
    Set (𝒳 × 𝒵 → ℝ) :=
  {f | ∃ g ∈ G, f = fun x => Real.sqrt ((g x.1 x.2 + g₀ x.1 x.2) / (2 * g₀ x.1 x.2))}

-- @node: def:hellinger
/-- For [a dominating measure](hyp:mu) and [two densities](hyp:g,g'), the
[squared Hellinger distance](goal) is the integral of their squared square-root difference,
without a factor of one half. -/
noncomputable def hellingerSqDensity (mu : Measure 𝒳) (g g' : 𝒳 → ℝ) : ℝ := -- @realizes H^2(unhalved integral of squared square-root density differences)
  Causalean.Stat.hellingerSqDensity mu g g'

variable (V : IVWorld 𝒲 𝒳 𝒵) (P : Measure Ω)
  (sample : AnalysisSample V P) (split : SampleSplit)

/-- In [the IV model](hyp:V), under [the sampling law](hyp:P) with [the observation sequence](hyp:sample)
and [the sample split](hyp:split), the [preliminary information](goal) at [block size n](hyp:n)
is the information generated by all observations in the preliminary block. -/
noncomputable abbrev preliminarySigma (n : ℕ) : MeasurableSpace Ω :=
  ⨆ i ∈ split.pre n, MeasurableSpace.comap (sample.Z i) inferInstance

/-- For [an IV model](hyp:V), [a dominating input measure](hyp:mu) and [a true conditional density](hyp:g₀),
the [RDIV setting](goal) requires [the instrument space to be the full space of square-integrable
instrument-measurable functions](step:1), [the joint input–instrument law to have the specified
conditional density relative to the input measure times the instrument marginal](step:2), and
[the moment representer's chosen version to equal the conditional mean of the outcome almost surely](step:3). -/
noncomputable def RDIVSetting (mu : Measure 𝒳) (g₀ : 𝒳 → 𝒵 → ℝ) : Prop :=
  V.Qbar.toSubmodule = lpMeas ℝ ℝ (.comap V.zOf inferInstance) 2 V.law ∧
  V.law.map (fun w => (V.xOf w, V.zOf w)) =
    (mu.prod (V.law.map V.zOf)).withDensity (fun x => ENNReal.ofReal (g₀ x.1 x.2)) ∧
  (fun w => dualVersion V (momentRepresenter V) (V.zOf w)) =ᵐ[V.law]
    V.law[V.Y | MeasurableSpace.comap V.zOf inferInstance]

/-- Given [an IV model](hyp:V), [a family of function representatives for its primal elements](hyp:versions),
[measurability of every representative](hyp:hmeas), and [almost-sure agreement with each original
square-integrable element](hyp:hcoherent), the [updated IV model](goal) uses this family as its
chosen primal representatives. -/
def rdivWithPrimalVersions
    (versions : V.Hbar.toSubmodule → 𝒳 → ℝ)
    (hmeas : ∀ h, Measurable (versions h))
    (hcoherent : ∀ h, (fun w => versions h (V.xOf w)) =ᵐ[V.law]
      ((h : Lp ℝ 2 V.law) : 𝒲 → ℝ)) : IVWorld 𝒲 𝒳 𝒵 :=
  { V with primalRealization := versions -- @realizes \mathcal H(chosen measurable coherent primal function representatives)
           primal_measurable := hmeas
           primal_coherent := hcoherent }

-- @node: ass:re-cd-realizability
/-- In [the IV model](hyp:V), for [a dominating measure](hyp:mu), [a candidate density class](hyp:G)
and [a true density](hyp:g₀), [density realizability](goal) means [the true density belongs to the
class](step:1) and [every candidate is jointly measurable, nonnegative everywhere, and integrates
to one for almost every instrument value](step:2). -/
noncomputable def DensityRealizable (mu : Measure 𝒳) (G : Set (𝒳 → 𝒵 → ℝ)) -- @realizes \mathcal G(class of conditional probability densities)
    (g₀ : 𝒳 → 𝒵 → ℝ) : Prop :=
  g₀ ∈ G ∧ ∀ g ∈ G, Measurable (Function.uncurry g) ∧ -- @realizes g_0(true density in the class, normalized almost everywhere)
    (∀ x z, 0 ≤ g x z) ∧ ∀ᵐ z ∂V.law.map V.zOf, (∫ x, g x z ∂mu) = 1

-- @node: ass:re-cd-density-bounds
/-- For [a density class](hyp:G), [a true density](hyp:g₀), [a common support](hyp:support),
[a lower bound](hyp:c₀), and [an upper bound](hyp:CG), the [density bounds condition](goal)
requires [a positive lower bound](step:1), [a positive upper bound](step:2),
[the true density to be at least the lower bound on the support](step:3), [every candidate to lie
below the upper bound there](step:4), and [every candidate to vanish off the support](step:5). -/
def DensityBounds (G : Set (𝒳 → 𝒵 → ℝ)) (g₀ : 𝒳 → 𝒵 → ℝ)
    (support : Set (𝒳 × 𝒵)) (c₀ CG : ℝ) : Prop :=
  0 < c₀ ∧ 0 < CG ∧ (∀ x ∈ support, c₀ ≤ g₀ x.1 x.2) ∧ -- @realizes c_0(strictly positive lower bound on the true density on common support)
  (∀ g ∈ G, ∀ x ∈ support, g x.1 x.2 ≤ CG) ∧ -- @realizes C_G(finite upper envelope on all conditional densities)
  ∀ g ∈ G, ∀ x ∉ support, g x.1 x.2 = 0

-- @node: ass:re-cd-nuisance-rate
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a sample split](hyp:split),
[a pilot regression estimate](hyp:rHat), and [an accuracy curve indexed by sample size and failure probability](hyp:δr),
the [pilot rate condition](goal) requires [at each positive sample size a preliminary-data-measurable
square-integrable selection agreeing almost surely with the pilot](step:1), and [at each failure
probability strictly between zero and one a nonnegative accuracy bound, almost-sure square
integrability of the pilot, and an L2 error bound relative to the moment representer holding
with probability at least one minus that failure probability](step:2). -/
noncomputable def PilotRegressionRate (rHat : ℕ → Ω → 𝒵 → ℝ) -- @realizes \hat r(preliminary-data measurable regression estimate)
    (δr : ℕ → ℝ → ℝ) : Prop :=
  (∀ n, 0 < n → ∃ selected : Ω → Lp ℝ 2 (V.law.map V.zOf),
    @Measurable Ω (Lp ℝ 2 (V.law.map V.zOf))
      (preliminarySigma V P sample split n) (borel _) selected ∧ -- @realizes \hat r(preliminary-measurable L2-valued pilot selection)
    ∀ᵐ ω ∂P, rHat n ω =ᵐ[V.law.map V.zOf] (selected ω : 𝒵 → ℝ)) ∧ -- @realizes \hat r(supplied representatives agree with the L2 pilot almost surely)
  ∀ n : ℕ, 0 < n → ∀ ξ ∈ Set.Ioo (0 : ℝ) 1, 0 ≤ δr n ξ ∧ -- @realizes \delta_{n,r}(nonnegative deterministic confidence-indexed pilot accuracy)
    (∀ᵐ ω ∂P, MemLp (rHat n ω) 2 (V.law.map V.zOf)) ∧
    1 - ξ ≤ P.real {ω | inputL2Norm (V.law.map V.zOf)
      (rHat n ω - dualVersion V (momentRepresenter V)) ≤ δr n ξ}

-- @node: ass:cr-deepiv-outcome
/-- For [an IV model](hyp:V) and [an outcome envelope](hyp:B), [outcome boundedness](goal)
requires [the envelope to be nonnegative](step:1) and [the absolute outcome to be at most
that envelope almost surely](step:2). -/
def OutcomeBounded (B : ℝ) : Prop := 0 ≤ B ∧ ∀ᵐ w ∂V.law, |V.Y w| ≤ B -- @realizes B(finite nonnegative envelope)

-- @node: ass:cr-deepiv-hypotheses
/-- For [an IV model](hyp:V), [an input–instrument support](hyp:support), and [an envelope](hyp:B),
[hypothesis-class boundedness](goal) means that every hypothesis's chosen function representative
has absolute value at most the envelope at every input appearing in the support. -/
noncomputable def HypothesisClassBounded (support : Set (𝒳 × 𝒵)) (B : ℝ) : Prop :=
  ∀ h ∈ V.H, ∀ x ∈ support, |primalVersion V h x.1| ≤ B

-- @node: ass:cr-deepiv-pilot
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [a pilot estimate](hyp:rHat),
[a fixed instrument support](hyp:pilotInputSupport), and [an envelope](hyp:B),
[pilot boundedness](goal) requires [the support to carry the entire instrument marginal law](step:1)
and [at every positive sample size, almost surely over the sample, the pilot's absolute value
to be at most the envelope simultaneously at every point of that support](step:2). -/
noncomputable def PilotBounded (rHat : ℕ → Ω → 𝒵 → ℝ)
    (pilotInputSupport : Set 𝒵) (B : ℝ) : Prop :=
  (∀ᵐ z ∂V.law.map V.zOf, z ∈ pilotInputSupport) ∧ -- @realizes Z(fixed pilot input support carries the marginal law)
  ∀ n : ℕ, 0 < n → ∀ᵐ ω ∂P,
    ∀ z ∈ pilotInputSupport, |rHat n ω z| ≤ B -- @realizes \hat r(pointwise envelope on its input support)

/-- For [a population law](hyp:law), [a function class](hyp:F), [a sample size](hyp:n),
and [an ordered sample](hyp:x), the [empirical supremum](goal) is the supremum over the class
of the absolute difference between the sample average and the population integral,
recorded as an extended nonnegative number. -/
noncomputable def empiricalSupremum {A : Type*} [MeasurableSpace A]
    (law : Measure A) (F : Set (A → ℝ)) (n : ℕ) (x : Fin n → A) : ℝ≥0∞ :=
  ⨆ f : F, ENNReal.ofReal |(n : ℝ)⁻¹ * ∑ i, f.1 (x i) - ∫ y, f.1 y ∂law|

/-- For [a population law](hyp:law) and [a function class](hyp:F), the
[localized-process measurability condition](goal) requires, for every positive sample size and
radius, [localizing the star-shaped difference class by its L2 norm](step:1) and requiring the
full empirical supremum, localized empirical supremum, and localized signed supremum to be
almost-everywhere measurable under the independent sampling law and, for the signed process,
independent uniform signs. -/
noncomputable def LocalizedProcessesMeasurable {A : Type*} [MeasurableSpace A]
    (law : Measure A) (F : Set (A → ℝ)) : Prop :=
  ∀ n : ℕ, 0 < n → ∀ r : ℝ, 0 < r →
    let localized := {f ∈ starClass (differenceClass F) |
      eLpNorm f 2 law ≤ ENNReal.ofReal r}
    AEMeasurable (empiricalSupremum law F n) (Measure.pi (fun _ => law)) ∧
    AEMeasurable (empiricalSupremum law localized n) (Measure.pi (fun _ => law)) ∧
    AEMeasurable (fun p : (Fin n → A) × (Fin n → Bool) =>
      signedSupremum localized n p.1 p.2)
      ((Measure.pi (fun _ => law)).prod
        ((Fintype.card (Fin n → Bool) : ℝ≥0∞)⁻¹ • Measure.count))

/-- For [an IV model](hyp:V), [a dominating input measure](hyp:mu), [a frozen density](hyp:g),
[a penalty weight](hyp:lam), [a localization radius](hyp:r), and [a comparator](hyp:hstar), the
[fitted loss class](goal) consists of penalized squared prediction losses minus the comparator's
loss, for hypotheses within the specified norm radius of the comparator; the penalty is the
weight times the squared chosen hypothesis value at the input. -/
noncomputable def rdivFittedLossClass (mu : Measure 𝒳) (g : 𝒳 → 𝒵 → ℝ)
    (lam r : ℝ) (hstar : V.Hbar.toSubmodule) : Set (𝒲 → ℝ) :=
  {f | ∃ h ∈ V.H, ‖h - hstar‖ ≤ r ∧ f = fun w =>
    ((V.Y w - densityOperator mu g (primalVersion V h) (V.zOf w)) ^ 2 +
      lam * primalVersion V h (V.xOf w) ^ 2) -
    ((V.Y w - densityOperator mu g (primalVersion V hstar) (V.zOf w)) ^ 2 +
      lam * primalVersion V hstar (V.xOf w) ^ 2)}

-- @node: ass:cr-deepiv-measurability
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample),
[a split](hyp:split), [an input measure](hyp:mu), [a density class](hyp:G),
[a reference density](hyp:g₀), and [a density selector](hyp:gHat), the
[RDIV class measurability condition](goal) [records the observation sequence](step:1),
[records the split](step:2), and [requires localized-process measurability for the hypothesis
representatives under the input marginal and for every candidate-density image under the
instrument marginal](step:3). The reference density and selector impose no additional restriction. -/
noncomputable def RDIVClassesMeasurable (mu : Measure 𝒳) (G : Set (𝒳 → 𝒵 → ℝ))
    (g₀ : 𝒳 → 𝒵 → ℝ) (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) : Prop :=
  let _ := sample
  let _ := split
  LocalizedProcessesMeasurable (V.law.map V.xOf) (primalVersion V '' V.H) ∧
  ∀ g ∈ G, LocalizedProcessesMeasurable (V.law.map V.zOf)
    (densityOperator mu g '' (primalVersion V '' V.H))

-- @node: ass:bk-owner-5
/-- For [an IV model](hyp:V), [a candidate density class](hyp:G), and [a reference density](hyp:g₀),
the [likelihood-process measurability condition](goal) [uses the joint input–instrument law](step:1),
[forms the square-root likelihood-transform class](step:2), and [for every positive sample size
and radius, localizes its star-shaped difference class by the L2 norm](step:3), requiring the
full empirical, localized empirical, and localized signed suprema to be measurable. -/
noncomputable def RDIVLikelihoodProcessesMeasurable
    (G : Set (𝒳 → 𝒵 → ℝ)) (g₀ : 𝒳 → 𝒵 → ℝ) : Prop :=
  let law := V.law.map (fun w => (V.xOf w, V.zOf w))
  let F := likelihoodTransformClass G g₀
  ∀ n : ℕ, 0 < n → ∀ r : ℝ, 0 < r →
    let localized := {f ∈ starClass (differenceClass F) |
      eLpNorm f 2 law ≤ ENNReal.ofReal r}
    Measurable (empiricalSupremum law F n) ∧
    Measurable (empiricalSupremum law localized n) ∧
    Measurable (fun p : (Fin n → 𝒳 × 𝒵) × (Fin n → Bool) =>
      signedSupremum localized n p.1 p.2)

/-- If [the full, localized, and signed likelihood processes are measurable](hyp:h), then
[they are almost-everywhere measurable under their independent sampling and uniform-sign laws](goal). -/
lemma rdiv_likelihood_processes_aemeasurable
    (G : Set (𝒳 → 𝒵 → ℝ)) (g₀ : 𝒳 → 𝒵 → ℝ)
    (h : RDIVLikelihoodProcessesMeasurable V G g₀) :
    LocalizedProcessesMeasurable (V.law.map (fun w => (V.xOf w, V.zOf w)))
      (likelihoodTransformClass G g₀) := by
  intro n hn r hr
  exact ⟨(h n hn r hr).1.aemeasurable,
    (h n hn r hr).2.1.aemeasurable, (h n hn r hr).2.2.aemeasurable⟩

-- @node: ass:bk-owner-1
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a split](hyp:split),
[an input measure](hyp:mu), [a selected density](hyp:gHat), and [a grid ratio](hyp:ρ), the
[fitting-supremum version condition](goal) requires [an admissible grid ratio](step:1) and
[for every positive sample size, grid penalty, and positive rational radius, a nonnegative
extended-valued version of the comparator-centered fitted-loss supremum, jointly measurable
in preliminary data and fresh observations, agreeing almost surely both on independent
fresh tuples and on the actual fitting block](step:2). -/
noncomputable def RDIVFittingSupremumVersion (mu : Measure 𝒳)
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) (ρ : ℝ) : Prop :=
  GridDomain ρ ∧ -- @realizes \lambda(fitting grid penalties are in the prescribed positive interval)
  ∀ n : ℕ, 0 < n → -- @realizes n(positive block size in the version convention)
    ∀ lam ∈ regGrid ρ n, ∀ q : ℚ, 0 < q →
    ∃ version : Ω × (Fin n → 𝒲) → ℝ≥0∞,
      @Measurable (Ω × (Fin n → 𝒲)) ℝ≥0∞
        ((preliminarySigma V P sample split n).prod inferInstance) inferInstance version ∧
      (∀ᵐ preliminary ∂P,
        (fun ws => version (preliminary, ws)) =ᵐ[Measure.pi (fun _ => V.law)]
          empiricalSupremum V.law
            (rdivFittedLossClass V mu (gHat n preliminary) lam (q : ℝ)
              (minNormSolution V)) n) ∧
      (fun ω => version (ω, fun j =>
        sample.Z ((Finset.equivFinOfCardEq (split.card_fit n)).symm j) ω)) =ᵐ[P]
        (fun ω => empiricalSupremum V.law
          (rdivFittedLossClass V mu (gHat n ω) lam (q : ℝ) (minNormSolution V)) n
          (fun j => sample.Z ((Finset.equivFinOfCardEq (split.card_fit n)).symm j) ω))

-- @node: ass:cr-deepiv-density-radius
/-- For [an IV model](hyp:V), [a density class](hyp:G), [a reference density](hyp:g₀), and
[a sample-size and confidence-indexed radius curve](hyp:δG), the [density critical-radius
condition](goal) requires that curve to bound the critical radius of the likelihood-transform
class under the joint input–instrument law at every positive sample size and failure
probability strictly between zero and one. -/
noncomputable def DensityCriticalRadiusBound (G : Set (𝒳 → 𝒵 → ℝ)) -- @realizes \delta_{n,\mathcal G}(confidence-indexed critical-radius upper bound)
    (g₀ : 𝒳 → 𝒵 → ℝ) (δG : ℕ → ℝ → ℝ) : Prop :=
  ∀ n : ℕ, 0 < n → ∀ ξ ∈ Set.Ioo (0 : ℝ) 1,
    IsCriticalRadiusBound (V.law.map fun w => (V.xOf w, V.zOf w))
      (likelihoodTransformClass G g₀) n (δG n ξ)

-- @node: ass:cr-deepiv-hypothesis-radius
/-- For [an IV model](hyp:V), [an input measure](hyp:mu), [a density class](hyp:G),
[a critical-radius curve](hyp:δH), and [a grid ratio](hyp:ρ), the [hypothesis critical-radius
condition](goal) [allocates each failure probability across the penalty grid](step:1) and
requires the resulting curve value to bound both the hypothesis class's critical radius
under the input marginal and every candidate-density image class's critical radius under
the instrument marginal, at every positive sample size. -/
noncomputable def HypothesisCriticalRadiusBound (mu : Measure 𝒳) -- @realizes \delta_{n,\mathcal H}(common bound for H and every density-induced image)
    (G : Set (𝒳 → 𝒵 → ℝ)) (δH : ℕ → ℝ → ℝ) (ρ : ℝ) : Prop :=
  ∀ n : ℕ, 0 < n → ∀ ξ ∈ Set.Ioo (0 : ℝ) 1,
    let η := gridConfidence ρ ξ n
    IsCriticalRadiusBound (V.law.map V.xOf) (primalVersion V '' V.H) n (δH n η) ∧
    ∀ g ∈ G, IsCriticalRadiusBound (V.law.map V.zOf)
      (densityOperator mu g '' (primalVersion V '' V.H)) n (δH n η)

-- @node: ass:cr-deepiv-radius-floor
/-- For [a density-radius curve](hyp:δG), [a hypothesis-radius curve](hyp:δH), and
[a grid ratio](hyp:ρ), the [RDIV radius-floor condition](goal) requires one positive constant
such that, at every positive sample size and failure probability strictly between zero and one,
[the density radius dominates that constant times the confidence floor](step:1) and
[the hypothesis radius dominates the same multiple of the floor at the grid-allocated
failure probability](step:2). -/
noncomputable def RDIVRadiusFloor (δG δH : ℕ → ℝ → ℝ) (ρ : ℝ) : Prop :=
  ∃ c > 0, ∀ n : ℕ, 0 < n → ∀ ξ ∈ Set.Ioo (0 : ℝ) 1,
    c * confidenceFloor n ξ ≤ δG n ξ ∧
    c * confidenceFloor n (gridConfidence ρ ξ n) ≤ δH n (gridConfidence ρ ξ n)

-- @node: lem:rdiv-mle-localized-concentration-li2024
/-- For [an IV model](hyp:V), the [likelihood localized-concentration assertion](goal) says that,
whenever the density model is correctly specified, realizable and bounded, its localized
processes are almost-everywhere measurable, and its critical-radius curve dominates a positive
multiple of the confidence floor, there is a positive constant uniform over sample sizes and
failure probabilities such that, with probability at least one minus half the failure
probability on an independent joint-input sample, every candidate's absolute empirical
negative-log-likelihood deviation is bounded by that constant times the sum of the critical
radius times the L2 distance of its square-root likelihood transform from one and the
squared critical radius, evaluated at half the failure probability.

Zihao Li, Hui Lan, Vasilis Syrgkanis, Mengdi Wang and Masatoshi Uehara
(2024), Regularized DeepIV with model selection, arXiv:2403.04236,
Localized Concentration (`lem:local-concen`, retained TeX lines 3456–3463),
credited to Foster and Syrgkanis. This carrier is exactly the likelihood
specialization recorded in the corrected proof: f_g in G0, fixed comparator 1,
loss -log, and failure probability ξ/2 on the canonical preliminary iid law.
The density, process-measurability and original G0 critical-radius assumptions
are retained; there is no critical-radius requirement on star(star(G0)-star(G0)).
The constant precedes n and ξ. MLE optimality, normalization, AM-GM, Young,
Hellinger conversion and preliminary-sample transport remain local proofs.
No arbitrary class, loss, comparator, MLE rate or Theorem-24 input is assumed. -/
noncomputable def LiLocalizedConcentration : Sort 0 :=
  ∀ (mu : Measure 𝒳) (G : Set (𝒳 → 𝒵 → ℝ)) (g₀ : 𝒳 → 𝒵 → ℝ)
    (support : Set (𝒳 × 𝒵)) (c₀ CG : ℝ),
    RDIVSetting V mu g₀ → DensityRealizable V mu G g₀ → DensityBounds G g₀ support c₀ CG →
    LocalizedProcessesMeasurable (V.law.map (fun w => (V.xOf w, V.zOf w)))
      (likelihoodTransformClass G g₀) →
    ∀ (δG : ℕ → ℝ → ℝ), DensityCriticalRadiusBound V G g₀ δG →
    (∃ c > 0, ∀ n : ℕ, 0 < n → ∀ ξ ∈ Set.Ioo (0 : ℝ) 1,
      c * confidenceFloor n ξ ≤ δG n ξ) →
    ∃ A > 0, ∀ n : ℕ, 0 < n → ∀ ξ ∈ Set.Ioo (0 : ℝ) 1,
      ∃ E : Set (Fin n → 𝒳 × 𝒵), MeasurableSet E ∧
        1 - ξ / 2 ≤ (Measure.pi (fun _ : Fin n =>
          V.law.map (fun w => (V.xOf w, V.zOf w)))).real E ∧
        ∀ x ∈ E, ∀ g ∈ G,
          let f := fun y : 𝒳 × 𝒵 =>
            Real.sqrt ((g y.1 y.2 + g₀ y.1 y.2) / (2 * g₀ y.1 y.2))
          |(n : ℝ)⁻¹ * (∑ i, -Real.log (f (x i))) -
            (∫ y, -Real.log (f y) ∂V.law.map (fun w => (V.xOf w, V.zOf w)))| ≤
            A * (δG n (ξ / 2) *
              inputL2Norm (V.law.map (fun w => (V.xOf w, V.zOf w)))
                (f - fun _ => 1) + δG n (ξ / 2) ^ 2)

/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a split](hyp:split),
[a conditional density](hyp:g), [a block size](hyp:n), and [a sample realization](hyp:ω), the
[preliminary likelihood](goal) is the product of that density evaluated at the observed
input–instrument pairs in the preliminary block. -/
noncomputable def preliminaryLikelihood (g : 𝒳 → 𝒵 → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
  ∏ i ∈ split.pre n, g (V.xOf (sample.Z i ω)) (V.zOf (sample.Z i ω))

-- @node: ass:pin-fix-4d0cd055
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a split](hyp:split),
[a candidate density class](hyp:G), and [a density selector](hyp:gHat), the [selected-MLE
condition](goal) requires, at every positive block size, [the selector almost surely to belong
to the class and maximize the preliminary likelihood over the class](step:1), and
[the density-valued selection to be measurable from the preliminary observations](step:2). -/
noncomputable def MLEMaximizerSelected (G : Set (𝒳 → 𝒵 → ℝ))
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) : Prop :=
  ∀ n : ℕ, 0 < n →
    (∀ᵐ ω ∂P, gHat n ω ∈ G ∧ ∀ g ∈ G, -- @realizes \hat g(exact selected empirical likelihood maximizer almost surely)
      preliminaryLikelihood V P sample split g n ω ≤
        preliminaryLikelihood V P sample split (gHat n ω) n ω) ∧
    @Measurable Ω (𝒳 → 𝒵 → ℝ)
      (preliminarySigma V P sample split n) inferInstance (gHat n) -- @realizes \hat g(preliminary-data measurable function-valued selection)

-- @node: ass:bk-owner-2
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a split](hyp:split),
[an input measure](hyp:mu), and [a selected density](hyp:gHat), the [selected-density version
condition](goal) requires, for each positive block size, a version that is
[jointly measurable in preliminary data and both input coordinates](step:1),
[nonnegative everywhere](step:2), [equal to the selected density almost everywhere in the
input measure for almost every preliminary sample and fresh instrument](step:3), and
[equal in the same input-measure sense at every actual calibration instrument, almost surely](step:4). -/
noncomputable def RDIVSelectedDensityVersion (mu : Measure 𝒳)
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) : Prop :=
  ∀ n : ℕ, 0 < n →
    ∃ gBar : Ω × (𝒳 × 𝒵) → ℝ,
      @Measurable (Ω × (𝒳 × 𝒵)) ℝ
        ((preliminarySigma V P sample split n).prod inferInstance) inferInstance gBar ∧
      (∀ p, 0 ≤ gBar p) ∧ -- @realizes \hat g(nonnegative measurable version; original selected density retained)
      (∀ᵐ a ∂P, ∀ᵐ z ∂V.law.map V.zOf,
        (fun x => gBar (a, (x, z))) =ᵐ[mu] (fun x => gHat n a x z)) ∧
      (∀ᵐ ω ∂P, ∀ i ∈ split.cal n, -- @realizes I_{\mathrm{cal}}(same version coherent at every actual calibration observation)
        (fun x => gBar (ω, (x, V.zOf (sample.Z i ω)))) =ᵐ[mu]
          (fun x => gHat n ω x (V.zOf (sample.Z i ω))))

-- @node: ass:bk-owner-3
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a split](hyp:split),
and [a pilot regression estimate](hyp:rHat), the [selected-pilot version condition](goal)
requires, at each positive block size, a version that is [jointly measurable in preliminary
data and the instrument](step:1), [equal to the pilot for almost every preliminary sample
and fresh instrument](step:2), and [equal to it at every actual calibration instrument,
almost surely over the sample](step:3). -/
noncomputable def RDIVSelectedPilotVersion
    (rHat : ℕ → Ω → 𝒵 → ℝ) : Prop :=
  ∀ n : ℕ, 0 < n → ∃ rBar : Ω × 𝒵 → ℝ,
    @Measurable (Ω × 𝒵) ℝ
      ((preliminarySigma V P sample split n).prod inferInstance) inferInstance rBar ∧
    (∀ᵐ a ∂P, (fun z => rBar (a, z)) =ᵐ[V.law.map V.zOf] rHat n a) ∧ -- @realizes \hat r(one jointly measurable version coherent under the fresh input law)
    (∀ᵐ ω ∂P, ∀ i ∈ split.cal n,
      rBar (ω, V.zOf (sample.Z i ω)) = rHat n ω (V.zOf (sample.Z i ω))) -- @realizes \hat r(the same version agrees at all actual calibration inputs)


-- @node: def:rdiv-preliminary
/-- Given [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a split](hyp:split),
[an input measure](hyp:mu), [a candidate density class](hyp:G), [a density selector](hyp:gHat),
and [a square-integrable pilot selector](hyp:rHat), with [the density selector a measurable
exact preliminary likelihood maximizer](hyp:_hMLE) and [the pilot selection measurable from
preliminary data at every positive block size](hyp:_hPilot), the [preliminary RDIV package](goal)
collects the selected density, its density-induced integration operator, and the pilot. -/
noncomputable def RDIVPreliminary (mu : Measure 𝒳) (G : Set (𝒳 → 𝒵 → ℝ))
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ)
    (rHat : ℕ → Ω → Lp ℝ 2 (V.law.map V.zOf)) -- @realizes \hat r(preliminary-data L₂-valued pilot; no chosen-representative joint evaluation requirement)
    (_hMLE : MLEMaximizerSelected V P sample split G gHat)
    (_hPilot : ∀ n, 0 < n →
      @Measurable Ω (Lp ℝ 2 (V.law.map V.zOf))
        (preliminarySigma V P sample split n) (borel _) (rHat n)) :=
  (gHat, (fun n ω => densityOperator mu (gHat n ω)), rHat)

/-- For [an IV model](hyp:V), [an input measure](hyp:mu), [a selected density family](hyp:gHat),
[a block size](hyp:n), [a sample realization](hyp:ω), and [a hypothesis](hyp:h), the
[estimated operator applied to the hypothesis](goal) integrates its chosen function
representative against the selected density, as a function of the instrument. -/
noncomputable def estimatedOperator (mu : Measure 𝒳) (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) -- @realizes \hat{\mathcal T}(integral operator induced by the selected density)
    (n : ℕ) (ω : Ω) (h : V.Hbar.toSubmodule) : 𝒵 → ℝ :=
  densityOperator mu (gHat n ω) (primalVersion V h)

/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a split](hyp:split),
[an input measure](hyp:mu), [a selected density family](hyp:gHat), [a block size](hyp:n),
[a sample realization](hyp:ω), and [a hypothesis](hyp:h), the [empirical RDIV loss](goal)
is the fitting-block average of squared outcome residuals using the density-induced
prediction of that hypothesis. -/
noncomputable def rdivEmpiricalLoss (mu : Measure 𝒳)
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) (n : ℕ) (ω : Ω) (h : V.Hbar.toSubmodule) : ℝ :=
  blockAverage V P sample (split.fit n)
    (fun w => (V.Y w - estimatedOperator V mu gHat n ω h (V.zOf w)) ^ 2) ω

-- @node: def:rdiv-population-loss
/-- For [an IV model](hyp:V) and [a hypothesis](hyp:h), the [population RDIV loss](goal)
is the expected squared difference between the outcome and the chosen instrument-function
representative of the hypothesis's projected conditional expectation. -/
noncomputable def rdivPopulationLoss (h : V.Hbar.toSubmodule) : ℝ :=
  ∫ w, (V.Y w - dualVersion V (projCondExpOp V h) (V.zOf w)) ^ 2 ∂V.law

/-- In [an IV model](hyp:V), the [outcome noise level](goal) is the expected squared difference
between the outcome and the moment representer's chosen instrument-function representative. -/
noncomputable def outcomeNoise : ℝ := -- @realizes \sigma^2_{Y\mid Z}(population squared regression residual)
  ∫ w, (V.Y w - dualVersion V (momentRepresenter V) (V.zOf w)) ^ 2 ∂V.law

-- @node: def:rdiv-projected-loss
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a split](hyp:split),
[an input measure](hyp:mu), [a selected density family](hyp:gHat), [a pilot regression](hyp:rHat),
[a block size](hyp:n), [a sample realization](hyp:ω), and [a hypothesis](hyp:h), the
[calibration statistic](goal) is the calibration-block average squared difference between
the pilot and the density-induced prediction, both evaluated at the observed instruments. -/
noncomputable def rdivCalibrationStat (mu : Measure 𝒳) -- @realizes D_n(projected calibration residual; adversarial loss in TRAE)
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) (rHat : ℕ → Ω → 𝒵 → ℝ)
    (n : ℕ) (ω : Ω) (h : V.Hbar.toSubmodule) : ℝ :=
  blockAverage V P sample (split.cal n)
    (fun w => (rHat n ω (V.zOf w) - estimatedOperator V mu gHat n ω h (V.zOf w)) ^ 2) ω

-- @node: def:rdiv-risks
/-- For [an IV model](hyp:V), [a penalty weight](hyp:lam), and [a hypothesis](hyp:h), the
[population penalized risk](goal) is the population RDIV loss plus the penalty weight
times the hypothesis's squared population norm. -/
noncomputable def populationRisk (lam : ℝ) (h : V.Hbar.toSubmodule) : ℝ := -- @realizes R^\lambda(population loss plus lambda times population norm squared)
  rdivPopulationLoss V h + lam * ‖h‖ ^ 2

/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a split](hyp:split),
[an input measure](hyp:mu), [a selected density family](hyp:gHat), [a block size](hyp:n),
[a sample realization](hyp:ω), [a penalty weight](hyp:lam), and [a hypothesis](hyp:h), the
[empirical penalized risk](goal) is the fitting-block squared prediction loss plus the
penalty weight times the empirical squared norm of the hypothesis's chosen representative. -/
noncomputable def empiricalRisk (mu : Measure 𝒳) -- @realizes R_n^\lambda(empirical loss plus empirical squared-norm penalty)
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) (n : ℕ) (ω : Ω) (lam : ℝ)
    (h : V.Hbar.toSubmodule) : ℝ :=
  rdivEmpiricalLoss V P sample split mu gHat n ω h +
    lam * primalEmpSq V P sample split n ω h

/-- For [an IV model](hyp:V), [an input measure](hyp:mu), [a selected density family](hyp:gHat),
[a block size](hyp:n), [a sample realization fixing the density fit](hyp:ω), and
[a hypothesis](hyp:h), the [conditional population loss](goal) is the population expected
squared outcome residual using the density-induced prediction with that fit held fixed. -/
noncomputable def conditionalPopulationLoss (mu : Measure 𝒳) -- @realizes \widehat L(population integration with the preliminary density fit frozen)
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) (n : ℕ) (ω : Ω) (h : V.Hbar.toSubmodule) : ℝ :=
  ∫ w, (V.Y w - estimatedOperator V mu gHat n ω h (V.zOf w)) ^ 2 ∂V.law

/-- For [an IV model](hyp:V), [an input measure](hyp:mu), [a selected density family](hyp:gHat),
[a block size](hyp:n), [a sample realization fixing the density fit](hyp:ω), [a penalty weight](hyp:lam),
and [a hypothesis](hyp:h), the [conditional penalized risk](goal) is the population squared
prediction loss with that density fit held fixed plus the penalty weight times the
hypothesis's squared population norm. -/
noncomputable def conditionalRisk (mu : Measure 𝒳) -- @realizes \widehat R^\lambda(conditional loss plus population squared-norm penalty)
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) (n : ℕ) (ω : Ω) (lam : ℝ)
    (h : V.Hbar.toSubmodule) : ℝ :=
  conditionalPopulationLoss V mu gHat n ω h + lam * ‖h‖ ^ 2

-- @node: def:rdiv-estimator
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a split](hyp:split),
[an input measure](hyp:mu), [a selected density family](hyp:gHat), [a block size](hyp:n),
[a penalty weight](hyp:lam), and [a hypothesis selector](hyp:candidate), the [RDIV estimator
condition](goal) requires [at every sample realization the selected hypothesis to belong to
the hypothesis class and minimize the empirical penalized risk over that class](step:1),
and [the selector to be measurable using only preliminary and fitting observations](step:2). -/
noncomputable def IsRDIVEstimator (mu : Measure 𝒳)
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) (n : ℕ) (lam : ℝ)
    (candidate : Ω → V.Hbar.toSubmodule) : Prop :=
  (∀ ω, candidate ω ∈ V.H ∧ ∀ h ∈ V.H,
    empiricalRisk V P sample split mu gHat n ω lam (candidate ω) ≤
      empiricalRisk V P sample split mu gHat n ω lam h) ∧
  @Measurable Ω V.Hbar.toSubmodule
    (⨆ i ∈ split.pre n ∪ split.fit n,
      MeasurableSpace.comap (sample.Z i) inferInstance)
    (borel _) candidate

-- @node: ass:rdiv-minima
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a split](hyp:split),
[an input measure](hyp:mu), [a selected density family](hyp:gHat), [a grid ratio](hyp:ρ), and
[a family of hypothesis selectors](hyp:candidate), the [attained-minima condition](goal)
requires, at every positive block size and grid penalty, [the selector always to belong to
the hypothesis class and minimize its empirical penalized risk](step:1), and
[the square-integrable hypothesis selection to be measurable from the preliminary and fitting
observations](step:2). -/
noncomputable def RDIVMinimaAttained (mu : Measure 𝒳)
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) (ρ : ℝ)
    (candidate : ℕ → ℝ → Ω → V.Hbar.toSubmodule) : Prop := -- @realizes \hat h_\lambda(measurable selected penalized regression fit at each grid point)
  ∀ n : ℕ, 0 < n → ∀ lam ∈ regGrid ρ n,
    (∀ ω, candidate n lam ω ∈ V.H ∧ ∀ h ∈ V.H,
      empiricalRisk V P sample split mu gHat n ω lam (candidate n lam ω) ≤
        empiricalRisk V P sample split mu gHat n ω lam h) ∧
    -- The paper selects the fit using the preliminary and fitting blocks.
    -- Measurability is of the L2-valued selection, not of supplied representatives.
    @Measurable Ω V.Hbar.toSubmodule
      (⨆ i ∈ split.pre n ∪ split.fit n,
        MeasurableSpace.comap (sample.Z i) inferInstance)
      (borel _) (candidate n lam)

/-- For [a raw accuracy curve indexed by sample size and failure probability](hyp:raw),
[a sample size](hyp:n), and [a public failure probability](hyp:ξ), the [evaluated accuracy](goal)
is the raw curve at that sample size and one quarter of the public failure probability. -/
noncomputable def rdivEvaluatedAccuracy (raw : ℕ → ℝ → ℝ) (n : ℕ) (ξ : ℝ) : ℝ :=
  raw n (ξ / 4)

/-- For [a grid ratio](hyp:ρ), [a public failure probability](hyp:ξ), and [a sample size](hyp:n),
the [component logarithmic scale](goal) is the square root of the logarithm of the grid size
divided by one quarter of the failure probability, all divided by the sample size. -/
noncomputable def rdivEvaluatedLogScale (ρ ξ : ℝ) (n : ℕ) : ℝ :=
  Real.sqrt (Real.log ((terminalIndex ρ n + 1) / (ξ / 4)) / n)

/-- For [a grid ratio](hyp:ρ), [a public failure probability](hyp:ξ), and [a sample size](hyp:n),
the [public logarithmic floor](goal) is the square root of the logarithm of the grid size
divided by the failure probability, all divided by the sample size. -/
noncomputable def rdivPublicLogScale (ρ ξ : ℝ) (n : ℕ) : ℝ :=
  Real.sqrt (Real.log ((terminalIndex ρ n + 1) / ξ) / n)
  -- @realizes \delta_{n,\xi}(the prescribed public logarithmic floor)

-- @node: rdivEvaluatedLogScale_le
/-- If [the grid ratio is at least one half and less than one](hyp:hρ),
[the failure probability is strictly between zero and one](hyp:hξ), and
[the sample size is positive](hyp:hn), then [the component logarithmic scale is at most
twice the public logarithmic floor](goal). -/
lemma rdivEvaluatedLogScale_le (ρ ξ : ℝ)
    (hρ : ρ ∈ Set.Ico (1 / 2 : ℝ) 1) (hξ : ξ ∈ Set.Ioo (0 : ℝ) 1)
    (n : ℕ) (hn : 0 < n) :
    rdivEvaluatedLogScale ρ ξ n ≤ 2 * rdivPublicLogScale ρ ξ n := by
  have hn1 : (1 : ℝ) ≤ n := by exact_mod_cast hn
  have hnpos : (0 : ℝ) < n := by exact_mod_cast hn
  have hρpos : 0 < ρ := by linarith [hρ.1]
  have hden : 0 < Real.log (1 / ρ) :=
    Real.log_pos ((lt_div_iff₀ hρpos).mpr (by linarith [hρ.2]))
  have hnum : 0 < Real.log (2 * (n : ℝ) ^ 2) :=
    Real.log_pos (by nlinarith)
  have hk : 0 < terminalIndex ρ n := Nat.ceil_pos.mpr (div_pos hnum hden)
  let x : ℝ := (terminalIndex ρ n + 1) / ξ
  have hk1 : (1 : ℝ) ≤ terminalIndex ρ n := by exact_mod_cast hk
  have hx : 2 ≤ x := by
    dsimp [x]
    apply (le_div_iff₀ hξ.1).mpr
    linarith [hξ.2]
  have hxpos : 0 < x := by linarith
  have hlog : Real.log 2 ≤ Real.log x :=
    Real.log_le_log (by norm_num) hx
  have hlog0 : 0 ≤ Real.log x := Real.log_nonneg (by linarith)
  have hlog4 : Real.log (4 : ℝ) = 2 * Real.log 2 := by
    rw [show (4 : ℝ) = 2 * 2 by norm_num, Real.log_mul (by norm_num) (by norm_num)]
    ring
  have heval : (terminalIndex ρ n + 1 : ℝ) / (ξ / 4) = x * 4 := by
    dsimp [x]
    ring
  have hbound : Real.log ((terminalIndex ρ n + 1 : ℝ) / (ξ / 4)) ≤
      4 * Real.log x := by
    rw [heval, Real.log_mul hxpos.ne' (by norm_num), hlog4]
    linarith
  unfold rdivEvaluatedLogScale rdivPublicLogScale
  change Real.sqrt _ ≤ 2 * Real.sqrt (Real.log x / n)
  apply Real.sqrt_le_iff.mpr
  refine ⟨by positivity, ?_⟩
  have hsq := Real.sq_sqrt (div_nonneg hlog0 hnpos.le)
  have hb := div_le_div_of_nonneg_right hbound hnpos.le
  rw [mul_div_assoc] at hb
  nlinarith only [hsq, hb]

-- keep: Names the exact evaluated fitting-radius sum referenced in the RDIV theorem signatures and their confidence-allocation audit.
/-- For [a grid ratio](hyp:ρ), [a failure probability](hyp:ξ), [raw density and fitting
accuracy curves](hyp:rawG,rawH), [an iteration horizon](hyp:iterations), and [a sample size](hyp:n),
the [fitting base scale](goal) sums the density accuracy at one quarter of the failure
probability, the fitting accuracy at one quarter of the iteration-grid confidence budget,
and the public logarithmic floor. -/
noncomputable def rdivFittingBaseScale (ρ ξ : ℝ) (rawG rawH : ℕ → ℝ → ℝ)
    (iterations n : ℕ) : ℝ :=
  rdivEvaluatedAccuracy rawG n ξ +
    rdivEvaluatedAccuracy rawH n (iterGridConfidence ρ ξ n iterations) +
    rdivPublicLogScale ρ ξ n

-- keep: Names the exact evaluated calibration-radius sum referenced in the RDIV theorem signatures and their confidence-allocation audit.
/-- For [a grid ratio](hyp:ρ), [a failure probability](hyp:ξ), [raw density and pilot
accuracy curves](hyp:rawG,rawR), and [a sample size](hyp:n), the [calibration base scale](goal)
is the sum of both accuracies evaluated at one quarter of the failure probability and
the public logarithmic floor. -/
noncomputable def rdivCalibrationBaseScale (ρ ξ : ℝ) (rawG rawR : ℕ → ℝ → ℝ)
    (n : ℕ) : ℝ :=
  rdivEvaluatedAccuracy rawG n ξ + rdivEvaluatedAccuracy rawR n ξ +
    rdivPublicLogScale ρ ξ n

-- @node: ass:delta-deepiv
/-- For [a grid ratio](hyp:ρ), [a failure probability](hyp:ξ), [fitting and calibration
scale sequences](hyp:δ,ν), and [public density, fitting, and pilot accuracy curves](hyp:publicG,publicH,publicR),
the [public scale calibration condition](goal) requires [at every positive sample size,
the density accuracy plus fitting accuracy at the grid confidence budget plus the public
logarithmic floor to be bounded by the fitting scale, and the density accuracy plus pilot
accuracy plus that floor to be bounded by the calibration scale](step:1), and
[the sum of the two scale sequences to converge to zero](step:2). -/
noncomputable def RDIVPublicScaleCalibration (ρ ξ : ℝ) (δ ν : ℕ → ℝ)
    (publicG publicH publicR : ℕ → ℝ → ℝ) : Prop :=
  (∀ n : ℕ, 0 < n →
    publicG n ξ + publicH n (gridConfidence ρ ξ n) +
      rdivPublicLogScale ρ ξ n ≤ δ n ∧
    publicG n ξ + publicR n ξ + rdivPublicLogScale ρ ξ n ≤ ν n) ∧
  Tendsto (fun n => δ n + ν n) atTop (𝓝 0)

/-- For [a grid ratio](hyp:ρ), [a failure probability](hyp:ξ), [fitting and calibration
scale sequences](hyp:δ,ν), [public density, fitting, and pilot accuracy curves](hyp:publicG,publicH,publicR),
and [an iteration horizon](hyp:iterations), the [iteration scale calibration condition](goal)
requires [at least one iteration](step:1), [at every positive sample size, the density
accuracy plus fitting accuracy at the iteration-grid confidence budget plus the public
logarithmic floor to be bounded by the fitting scale, and the density accuracy plus pilot
accuracy plus that floor to be bounded by the calibration scale](step:2), and
[the sum of the two scale sequences to converge to zero](step:3). -/
noncomputable def RDIVIterationScaleCalibration (ρ ξ : ℝ) (δ ν : ℕ → ℝ)
    (publicG publicH publicR : ℕ → ℝ → ℝ) (iterations : ℕ) : Prop :=
  1 ≤ iterations ∧ (∀ n : ℕ, 0 < n →
    publicG n ξ + publicH n (iterGridConfidence ρ ξ n iterations) +
      rdivPublicLogScale ρ ξ n ≤ δ n ∧
    publicG n ξ + publicR n ξ + rdivPublicLogScale ρ ξ n ≤ ν n) ∧
  Tendsto (fun n => δ n + ν n) atTop (𝓝 0)

/-- For [a grid ratio](hyp:ρ), [a failure probability](hyp:ξ), [fitting and calibration
scale sequences](hyp:δ,ν), [raw density, fitting, and pilot accuracy curves](hyp:rawG,rawH,rawR),
and [an iteration horizon](hyp:iterations), the [raw scale calibration condition](goal)
is iteration scale calibration with each raw curve evaluated at one quarter of its
confidence argument. -/
noncomputable def RDIVScaleCalibration (ρ ξ : ℝ) (δ ν : ℕ → ℝ)
    (rawG rawH rawR : ℕ → ℝ → ℝ) (iterations : ℕ) : Prop :=
  RDIVIterationScaleCalibration ρ ξ δ ν
    (rdivEvaluatedAccuracy rawG) (rdivEvaluatedAccuracy rawH)
    (rdivEvaluatedAccuracy rawR) iterations

-- keep: Checked raw-to-public calibration identity used to audit that relabelling preserves confidence arguments without comparing distinct curve values.
/-- [Raw scale calibration is equivalent to iteration scale calibration using the
density, fitting, and pilot curves evaluated at one quarter of their confidence arguments](goal). -/
lemma rdivScaleCalibration_iff_public (ρ ξ : ℝ) (δ ν : ℕ → ℝ)
    (rawG rawH rawR : ℕ → ℝ → ℝ) (iterations : ℕ) :
    RDIVScaleCalibration ρ ξ δ ν rawG rawH rawR iterations ↔
      RDIVIterationScaleCalibration ρ ξ δ ν
        (rdivEvaluatedAccuracy rawG) (rdivEvaluatedAccuracy rawH)
        (rdivEvaluatedAccuracy rawR) iterations := Iff.rfl

-- @node: rdivScaleCalibration_one_iff_public
/-- [Raw scale calibration with one iteration is equivalent to public scale calibration
using the density, fitting, and pilot curves evaluated at one quarter of their confidence arguments](goal). -/
lemma rdivScaleCalibration_one_iff_public (ρ ξ : ℝ) (δ ν : ℕ → ℝ)
    (rawG rawH rawR : ℕ → ℝ → ℝ) :
    RDIVScaleCalibration ρ ξ δ ν rawG rawH rawR 1 ↔
      RDIVPublicScaleCalibration ρ ξ δ ν
        (rdivEvaluatedAccuracy rawG) (rdivEvaluatedAccuracy rawH)
        (rdivEvaluatedAccuracy rawR) := by
  simp [RDIVScaleCalibration, RDIVIterationScaleCalibration,
    RDIVPublicScaleCalibration, iterGridConfidence, gridConfidence]

-- @node: rdivQuadraticLossLipschitz
/-- If [the envelope is nonnegative](hyp:hB), [the outcome has absolute value at most
the envelope](hyp:hy), [both prediction coordinates have absolute value at most the
envelope](hyp:hu,hu'), [both penalty coordinates have absolute value at most the
envelope](hyp:hv,hv'), and [the penalty weight is positive and at most two](hyp:hlam),
then [the absolute difference of the two penalized squared losses is at most four times
the envelope times the sum of the absolute coordinate differences](goal). -/
lemma rdivQuadraticLossLipschitz (B y u v u' v' lam : ℝ)
    (hB : 0 ≤ B) (hy : |y| ≤ B) (hu : |u| ≤ B) (hv : |v| ≤ B)
    (hu' : |u'| ≤ B) (hv' : |v'| ≤ B) (hlam : lam ∈ Set.Ioc (0 : ℝ) 2) :
    |((y - u) ^ 2 + lam * v ^ 2) - ((y - u') ^ 2 + lam * v' ^ 2)| ≤
      4 * B * (|u - u'| + |v - v'|) := by
  have hres (x : ℝ) (hx : |x| ≤ B) : |y - x| ≤ 2 * B := by
    calc
      |y - x| ≤ |y| + |x| := abs_sub y x
      _ ≤ 2 * B := by linarith
  have hfit := localizedSquaredLossLipschitz (2 * B) (y - u) (y - u')
    (by positivity) (hres u hu) (hres u' hu')
  have hpen := localizedSquaredLossLipschitz B v v' hB hv hv'
  have hdiff : (y - u) - (y - u') = -(u - u') := by ring
  rw [hdiff, abs_neg] at hfit
  calc
    _ = |((y - u) ^ 2 - (y - u') ^ 2) + lam * (v ^ 2 - v' ^ 2)| := by
      congr 1
      ring
    _ ≤ |(y - u) ^ 2 - (y - u') ^ 2| + |lam * (v ^ 2 - v' ^ 2)| := abs_add_le _ _
    _ = |(y - u) ^ 2 - (y - u') ^ 2| + lam * |v ^ 2 - v' ^ 2| := by
      rw [abs_mul, abs_of_pos hlam.1]
    _ ≤ 4 * B * |u - u'| + lam * (2 * B * |v - v'|) := by
      exact add_le_add (by nlinarith only [hfit])
        (mul_le_mul_of_nonneg_left hpen hlam.1.le)
    _ ≤ 4 * B * |u - u'| + 2 * (2 * B * |v - v'|) := by
      gcongr
      exact hlam.2
    _ = _ := by ring

-- @node: rdivCoordinateDistance
/-- If [the first coordinate is nonnegative](hyp:ha) and [the second coordinate is
nonnegative](hyp:hb), then [the square root of their sum of squares is at most their sum](goal). -/
lemma rdivCoordinateDistance (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) :
    Real.sqrt (a ^ 2 + b ^ 2) ≤ a + b := by
  apply (Real.sqrt_le_iff).2
  exact ⟨add_nonneg ha hb, by nlinarith [mul_nonneg ha hb]⟩

-- @node: def:rdiv-common-scales
/-- For [a fitting scale](hyp:δ), [a calibration scale](hyp:ν), and [a penalty weight](hyp:lam),
the [RDIV noise level](goal) is the squared fitting scale divided by the penalty weight
plus the squared calibration scale. -/
noncomputable def rdivNoiseLevel (δ ν lam : ℝ) : ℝ := δ ^ 2 / lam + ν ^ 2 -- @realizes A_n^{\mathrm R}(delta squared over lambda plus nu squared)
/-- For [a fitting scale](hyp:δ) and [a penalty weight](hyp:lam), the [RDIV stability
scale](goal) is the squared fitting scale divided by the squared penalty weight. -/
noncomputable def rdivStability (δ lam : ℝ) : ℝ := δ ^ 2 / lam ^ 2 -- @realizes V_n^{\mathrm R}(delta squared over lambda squared)

-- @node: def:rdiv-oracle-point
/-- For [a grid ratio](hyp:ρ), [a balancing multiplier](hyp:c), [a smoothness index](hyp:β),
[fitting and calibration scale sequences](hyp:δ,ν), and [a sample size](hyp:n), the
[RDIV oracle penalty](goal) is the first grid point below the multiplier times the larger
of the fitting scale raised to two divided by one plus the bias exponent and the calibration
scale raised to two divided by the bias exponent. -/
noncomputable def rdivOraclePoint (ρ c β : ℝ) (δ ν : ℕ → ℝ) (n : ℕ) : ℝ := -- @realizes \lambda_{\mathrm R}^\circ(first grid point below the RDIV balancing radius)
  oraclePoint ρ n (c * max (δ n ^ (2 / (biasExponent β + 1))) (ν n ^ (2 / biasExponent β)))

-- @node: def:rdiv-minimum-size
/-- For [an outcome envelope](hyp:B), the [minimum RDIV sample size](goal) is the larger
of two and the natural-number ceiling of eight times the squared envelope divided by
three times the natural logarithm of two. -/
noncomputable def rdivMinSampleSize (B : ℝ) : ℕ := max 2 ⌈8 * B ^ 2 / (3 * Real.log 2)⌉₊ -- @realizes N_{\mathrm R}(B)(maximum of two and the prescribed natural ceiling)

/-- For [an IV model](hyp:V), [an input measure](hyp:mu), [a true conditional density](hyp:g₀),
[a density estimator](hyp:gHat), [a pilot regression estimator](hyp:rHat), [a failure
probability](hyp:ξ), [density and pilot accuracy curves](hyp:δG,δr), [a sample size](hyp:n),
[a sample realization](hyp:ω), and [a comparison multiplier](hyp:C), the [preliminary
RDIV bounds](goal) require [the instrument-averaged squared Hellinger error to be at most
the multiplier times the squared density accuracy at one quarter of the failure probability](step:1),
[the pilot to be square integrable](step:2), [its L2 error relative to the moment representer
to be at most the pilot accuracy at that same confidence budget](step:3), [every hypothesis's
operator L2 error to be at most the multiplier times the density accuracy](step:4),
[the operator L1 error for every pairwise hypothesis difference to be at most that same
bound times the norm of the difference](step:5), and [the absolute error in each pairwise
population loss difference to satisfy that same norm-scaled bound](step:6). -/
noncomputable def RDIVPreliminaryOn (mu : Measure 𝒳)
    (g₀ : 𝒳 → 𝒵 → ℝ) (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ)
    (rHat : ℕ → Ω → 𝒵 → ℝ) (ξ : ℝ) (δG δr : ℕ → ℝ → ℝ)
    (n : ℕ) (ω : Ω) (C : ℝ) : Prop :=
  (∫ z, hellingerSqDensity mu (fun x => gHat n ω x z) (fun x => g₀ x z)
    ∂V.law.map V.zOf) ≤ C * δG n (ξ / 4) ^ 2 ∧
  MemLp (rHat n ω) 2 (V.law.map V.zOf) ∧
  inputL2Norm (V.law.map V.zOf)
    (rHat n ω - dualVersion V (momentRepresenter V)) ≤ δr n (ξ / 4) ∧
  (∀ h ∈ V.H, inputL2Norm (V.law.map V.zOf)
    (estimatedOperator V mu gHat n ω h - dualVersion V (projCondExpOp V h)) ≤
      C * δG n (ξ / 4)) ∧
  (∀ h ∈ V.H, ∀ h' ∈ V.H,
    inputL1Norm (V.law.map V.zOf)
      (estimatedOperator V mu gHat n ω (h - h') -
        dualVersion V (projCondExpOp V (h - h'))) ≤ C * δG n (ξ / 4) * ‖h - h'‖) ∧
  ∀ h ∈ V.H, ∀ h' ∈ V.H,
    |(conditionalPopulationLoss V mu gHat n ω h - conditionalPopulationLoss V mu gHat n ω h') -
      (rdivPopulationLoss V h - rdivPopulationLoss V h')| ≤
        C * δG n (ξ / 4) * ‖h - h'‖

/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a sample
split](hyp:split), [an input measure](hyp:mu), [a true density](hyp:g₀), [a density estimator](hyp:gHat),
[a pilot estimator](hyp:rHat), [a grid ratio](hyp:ρ), [a failure probability](hyp:ξ),
[a calibration scale sequence](hyp:ν), [density, fitting, and pilot accuracy curves](hyp:δG,δH,δr),
[candidate hypothesis selectors](hyp:candidate), [a sample size](hyp:n), [an event](hyp:E),
and [a comparison multiplier](hyp:C), the [common RDIV comparisons](goal) require at every
realization in the event [the preliminary RDIV bounds](step:1), [uniformly over grid penalties
and hypotheses, the error between conditional and empirical risk differences relative to the
minimum-norm solution to be bounded by the multiplier times fitting accuracy times hypothesis
distance plus squared fitting accuracy, using one quarter of the grid confidence budget](step:2),
and [each candidate's calibration statistic to differ from its squared projected error by
at most the multiplier times the calibration scale times projected error norm plus the
multiplier times squared calibration scale](step:3). -/
noncomputable def RDIVComparisonsOn (mu : Measure 𝒳)
    (g₀ : 𝒳 → 𝒵 → ℝ) (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ)
    (rHat : ℕ → Ω → 𝒵 → ℝ) (ρ ξ : ℝ) (ν : ℕ → ℝ)
    (δG δH δr : ℕ → ℝ → ℝ)
    (candidate : ℕ → ℝ → Ω → V.Hbar.toSubmodule)
    (n : ℕ) (E : Set Ω) (C : ℝ) : Prop :=
  ∀ ω ∈ E, -- @realizes \mathcal E_n^{\mathrm R}(common preliminary, fitting and calibration comparisons on one event)
    RDIVPreliminaryOn V mu g₀ gHat rHat ξ δG δr n ω C ∧
    (∀ lam ∈ regGrid ρ n, ∀ h ∈ V.H,
      |(conditionalRisk V mu gHat n ω lam h - conditionalRisk V mu gHat n ω lam (minNormSolution V)) -
        (empiricalRisk V P sample split mu gHat n ω lam h -
          empiricalRisk V P sample split mu gHat n ω lam (minNormSolution V))| ≤
        C * (δH n (gridConfidence ρ ξ n / 4) * ‖h - minNormSolution V‖ +
          δH n (gridConfidence ρ ξ n / 4) ^ 2)) ∧
    ∀ lam ∈ regGrid ρ n,
      |rdivCalibrationStat V P sample split mu gHat rHat n ω (candidate n lam ω) -
        ‖projCondExpOp V (candidate n lam ω - minNormSolution V)‖ ^ 2| ≤
      C * ν n * ‖projCondExpOp V (candidate n lam ω - minNormSolution V)‖ + C * ν n ^ 2

-- @node: def:rdiv-discrepancy-bound
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), [a sample
split](hyp:split), [an input measure](hyp:mu), [a density estimator](hyp:gHat), [a pilot
estimator](hyp:rHat), [a grid ratio](hyp:ρ), [a smoothness index](hyp:β), [fitting and calibration
scale sequences](hyp:δ,ν), [a source element](hyp:w₀), [candidate hypothesis selectors](hyp:candidate),
[a sample size](hyp:n), [an event](hyp:E), and [an envelope multiplier](hyp:C), the
[RDIV discrepancy envelope](goal) requires [the multiplier to be positive](step:1) and
[at every realization in the event and every grid penalty, the candidate's calibration
statistic to be at most the RDIV noise level plus the multiplier times the source element's
squared norm times the penalty raised to the bias exponent](step:2). -/
noncomputable def RDIVDiscrepancyEnvelope (mu : Measure 𝒳)
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) (rHat : ℕ → Ω → 𝒵 → ℝ)
    (ρ β : ℝ) (δ ν : ℕ → ℝ) (w₀ : V.Hbar.toSubmodule)
    (candidate : ℕ → ℝ → Ω → V.Hbar.toSubmodule) (n : ℕ) (E : Set Ω) (C : ℝ) : Prop :=
  0 < C ∧ ∀ ω ∈ E, ∀ lam ∈ regGrid ρ n,
    rdivCalibrationStat V P sample split mu gHat rHat n ω (candidate n lam ω) ≤
      rdivNoiseLevel (δ n) (ν n) lam + C * ‖w₀‖ ^ 2 * lam ^ biasExponent β

-- @node: def:rdiv-oracle-scales
/-- For [a grid ratio](hyp:ρ), [a balancing multiplier](hyp:c), [a smoothness index](hyp:β),
and [fitting and calibration scale sequences](hyp:δ,ν), the [RDIV oracle scale condition](goal)
asserts that one positive constant eventually bounds both [the noise level at the oracle
penalty by that constant times the sum of the fitting scale raised to twice the bias
exponent divided by one plus that exponent and the squared calibration scale](step:1),
and [the stability scale at the oracle penalty by that constant times the fitting scale
raised to twice the bias exponent minus two, divided by one plus the bias exponent](step:2). -/
noncomputable def RDIVOracleScales (ρ c β : ℝ) (δ ν : ℕ → ℝ) : Prop :=
  ∃ C > 0, ∀ᶠ n in atTop,
    rdivNoiseLevel (δ n) (ν n) (rdivOraclePoint ρ c β δ ν n) ≤
      C * (δ n ^ (2 * biasExponent β / (biasExponent β + 1)) + ν n ^ 2) ∧
    rdivStability (δ n) (rdivOraclePoint ρ c β δ ν n) ≤
      C * δ n ^ (2 * (biasExponent β - 1) / (biasExponent β + 1))


-- Internal rate target; its local proof is required by the repaired t_err_dp.
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), and
[a sample split](hyp:split), the [conditional maximum-likelihood Hellinger rate condition](goal)
asserts that, under the RDIV setting, density realizability and bounds, measurable exact
likelihood maximization, and class measurability, there is a positive constant such that
at every positive sample size and failure probability strictly between zero and one,
any likelihood-transform critical radius above the confidence floor bounds the
instrument-averaged squared Hellinger error by that constant times its square with
probability at least one minus the failure probability.

The paper proves this density-only rate target locally from likelihood optimality and
localized concentration. -/
noncomputable def ConditionalMLEHellingerRate : Sort 0 :=
  ∀ (mu : Measure 𝒳) (G : Set (𝒳 → 𝒵 → ℝ)) (g₀ : 𝒳 → 𝒵 → ℝ)
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ)
    (support : Set (𝒳 × 𝒵)) (c₀ CG : ℝ),
    RDIVSetting V mu g₀ → DensityRealizable V mu G g₀ → DensityBounds G g₀ support c₀ CG →
    MLEMaximizerSelected V P sample split G gHat → RDIVClassesMeasurable V P sample split mu G g₀ gHat →
    ∃ C > 0, ∀ (n : ℕ) (ξ r : ℝ), 0 < n → ξ ∈ Set.Ioo (0 : ℝ) 1 →
      confidenceFloor n ξ ≤ r →
      IsCriticalRadiusBound (V.law.map fun w => (V.xOf w, V.zOf w))
        (likelihoodTransformClass G g₀) n r →
      1 - ξ ≤ P.real {ω | (∫ z,
        hellingerSqDensity mu (fun x => gHat n ω x z) (fun x => g₀ x z)
          ∂V.law.map V.zOf) ≤ C * r ^ 2}

-- @node: lem:rdiv-localized-concentration-lemma-14
/-- For [an IV model](hyp:V), [a sampling law](hyp:P), [observations](hyp:sample), and
[a sample split](hyp:split), the [localized concentration condition for the two RDIV
coordinates](goal) asserts the following under probability sampling, the RDIV setting,
the range condition, membership of the minimum-norm solution in the hypothesis class,
density realizability and bounds, bounded outcomes and hypotheses, measurable likelihood
maximization, class measurability, and a measurable fitting supremum: one positive constant
bounds the error between conditional and empirical penalized risk differences relative to
the minimum-norm solution, simultaneously over all hypotheses, by the radius times the
sum of the density-induced prediction L2 distance and hypothesis norm distance, plus the
squared radius, all multiplied by that constant. For almost every preliminary sample,
the bound holds with fitting-sample probability at least one minus the failure probability,
for every positive sample size, failure probability strictly between zero and one, grid
penalty in `(0, 2]`, and radius above the confidence floor satisfying the hypothesis and
all candidate-density prediction critical-radius bounds.

Foster and Syrgkanis (2023), Orthogonal statistical learning,
DOI:10.1214/23-AOS2258, Lemma 14, `foster2023orthogonal`, as applied in
appendices.tex:197–235. This cited input is restricted to the two coordinates
(T-hat h(Z), h(X)), comparator h0, and phi_lambda(y,u,v)=(y-u)^2+lambda*v^2.
For almost every preliminary sample the fitted density is held fixed, and the
probability below is over the independent fitting sample. The two population
coordinate norms are retained separately, before the local density/Jensen reduction.
The retained source's positive-constant negative tails in lem:prob_localized
and the full lem:peeling proof support confidence conversion and fixed radius
inflation; no sign is assigned to the unsigned Lemma-14 display's c6.
No arbitrary vector class, dimension, loss, or population law is assumed here. -/
noncomputable def LipschitzVectorLocalizedConcentration
    (V : IVWorld 𝒲 𝒳 𝒵) (P : Measure Ω)
    (sample : AnalysisSample V P) (split : SampleSplit) : Sort 0 :=
  IsProbabilityMeasure P →
  ∀ (mu : Measure 𝒳) (G : Set (𝒳 → 𝒵 → ℝ)) (g₀ : 𝒳 → 𝒵 → ℝ)
    (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) (support : Set (𝒳 × 𝒵))
    (B c₀ CG ρ : ℝ),
    RDIVSetting V mu g₀ → RangeCondition V → H0MemHypothesisClass V →
    DensityRealizable V mu G g₀ → DensityBounds G g₀ support c₀ CG →
    OutcomeBounded V B → HypothesisClassBounded V support B →
    MLEMaximizerSelected V P sample split G gHat →
    RDIVClassesMeasurable V P sample split mu G g₀ gHat →
    RDIVFittingSupremumVersion V P sample split mu gHat ρ →
    ∃ C > 0, ∀ (n : ℕ) (ζ r lam : ℝ), 0 < n →
      ζ ∈ Set.Ioo (0 : ℝ) 1 → lam ∈ regGrid ρ n → lam ∈ Set.Ioc (0 : ℝ) 2 →
      confidenceFloor n ζ ≤ r →
      IsCriticalRadiusBound (V.law.map V.xOf) (primalVersion V '' V.H) n r →
      (∀ g ∈ G, IsCriticalRadiusBound (V.law.map V.zOf)
        (densityOperator mu g '' (primalVersion V '' V.H)) n r) →
      ∀ᵐ preliminary ∂P,
        1 - ζ ≤ P.real {ω | ∀ h ∈ V.H,
          |(conditionalRisk V mu gHat n preliminary lam h -
              conditionalRisk V mu gHat n preliminary lam (minNormSolution V)) -
            (empiricalRisk V P sample split mu (fun _ _ => gHat n preliminary) n ω lam h -
              empiricalRisk V P sample split mu (fun _ _ => gHat n preliminary) n ω lam
                (minNormSolution V))| ≤
          C * (r * inputL2Norm (V.law.map V.zOf)
            (densityOperator mu (gHat n preliminary)
              (primalVersion V h - primalVersion V (minNormSolution V))) +
            r * ‖h - minNormSolution V‖ + r ^ 2)}

-- @node: ass:pin-153
/-- The [pinned RDIV measurability condition](goal) is the full RDIV class measurability
condition, with all its model, sampling, density-class, and estimator arguments left open. -/
noncomputable def PinRDIVMeasurabilityReading := @RDIVClassesMeasurable

-- @node: ass:pin-155
/-- The [pinned RDIV minima condition](goal) is the attained-minima condition requiring
measurable empirical penalized-risk minimizers at every positive sample size and grid
penalty, with all its model, sampling, and estimator arguments left open. -/
noncomputable def PinRDIVMinimaReading := @RDIVMinimaAttained


variable (ρ ξ B β c₀ CG Cm c a b κδ κν required : ℝ) (w₀ : V.Hbar.toSubmodule)
  (δ ν baseδ baseν : ℕ → ℝ) (δG δH δr : ℕ → ℝ → ℝ)
  (κ₀ : ℝ → ℝ → ℝ → ℝ → ℝ × ℝ) (mu : Measure 𝒳)
  (G : Set (𝒳 → 𝒵 → ℝ)) (g₀ : 𝒳 → 𝒵 → ℝ) (support : Set (𝒳 × 𝒵))
  (gHat : ℕ → Ω → 𝒳 → 𝒵 → ℝ) (rHat : ℕ → Ω → 𝒵 → ℝ)
  (candidate : ℕ → ℝ → Ω → V.Hbar.toSubmodule)
  (iter : ℕ → ℕ → ℝ → Ω → V.Hbar.toSubmodule) (t : ℕ)


-- @node: rdivPopulationLoss_eq
/-- Under [the RDIV setting identifying the instrument space, conditional density, and
conditional outcome mean](hyp:hIV), [the range condition ensuring a minimum-norm solution](hyp:hRange),
and [a nonnegative almost-sure bound on the outcome](hyp:hY), [the population squared
prediction loss of any hypothesis equals the outcome noise plus the squared norm of the
projected difference between that hypothesis and the minimum-norm solution](goal). -/
lemma rdivPopulationLoss_eq (mu : Measure 𝒳) (g₀ : 𝒳 → 𝒵 → ℝ)
    (hIV : RDIVSetting V mu g₀) (hRange : RangeCondition V)
    (B : ℝ) (hY : OutcomeBounded V B) (h : V.Hbar.toSubmodule) :
    rdivPopulationLoss V h = outcomeNoise V +
      ‖projCondExpOp V (h - minNormSolution V)‖ ^ 2 := by
  have hYm : AEStronglyMeasurable V.Y V.law := V.measurable_Y.aestronglyMeasurable
  have hY2 : MemLp V.Y 2 V.law :=
    MemLp.of_bound hYm B (by simpa only [Real.norm_eq_abs] using hY.2)
  let y : Lp ℝ 2 V.law := hY2.toLp V.Y
  let r := momentRepresenter V
  let q := projCondExpOp V h
  have hr : (r : Lp ℝ 2 V.law) =
      (condExpL2 ℝ ℝ V.measurable_z.comap_le y : Lp ℝ 2 V.law) := by
    apply Lp.ext
    exact (V.dual_coherent r).symm.trans
      (hIV.2.2.trans (hY2.condExpL2_ae_eq_condExp (𝕜 := ℝ)
        V.measurable_z.comap_le).symm)
  have horth : inner ℝ (y - (r : Lp ℝ 2 V.law))
      ((r - q : V.Qbar.toSubmodule) : Lp ℝ 2 V.law) = 0 := by
    rw [inner_sub_left, hr,
      inner_condExpL2_eq_inner_fun V.measurable_z.comap_le y _
        (mem_lpMeas_iff_aestronglyMeasurable.mp (V.Qmeas (r - q).property)), sub_self]
  have hsquare (f : Lp ℝ 2 V.law) :
      (∫ w, f w ^ 2 ∂V.law) = ‖f‖ ^ 2 := by
    simpa only [L2.inner_def, RCLike.inner_apply, conj_trivial, pow_two] using
      real_inner_self_eq_norm_sq f
  have hloss (a : V.Qbar.toSubmodule) :
      (∫ w, (V.Y w - dualVersion V a (V.zOf w)) ^ 2 ∂V.law) =
        ‖y - (a : Lp ℝ 2 V.law)‖ ^ 2 := by
    rw [← hsquare]
    apply integral_congr_ae
    filter_upwards [hY2.coeFn_toLp, V.dual_coherent a,
      Lp.coeFn_sub y (a : Lp ℝ 2 V.law)] with w hy ha hsub
    dsimp only [y] at hsub ⊢
    change (V.Y w - V.dualRealization a (V.zOf w)) ^ 2 = _
    rw [hsub, Pi.sub_apply, hy, ha]
  rw [rdivPopulationLoss, hloss, outcomeNoise, hloss]
  have hdecomp : y - (q : Lp ℝ 2 V.law) =
      (y - (r : Lp ℝ 2 V.law)) +
        ((r - q : V.Qbar.toSubmodule) : Lp ℝ 2 V.law) := by
    change y - (q : Lp ℝ 2 V.law) = (y - r) + (r - q)
    abel
  change ‖y - (q : Lp ℝ 2 V.law)‖ ^ 2 = _
  rw [hdecomp, norm_add_sq_real, horth, mul_zero, add_zero]
  congr 1
  have heq : r - q = -projCondExpOp V (h - minNormSolution V) := by
    dsimp [r, q]
    rw [map_sub, (minNormSolution_spec V hRange).1]
    abel
  rw [heq]
  simp only [Submodule.coe_neg, norm_neg, Submodule.norm_coe]



variable (rawG rawH rawR : ℕ → ℝ → ℝ)

end Papers.TsAdaptiveEstimationInference