9.1. 4. Pair information from a positive quadratic form
Setting. Units and conventions are those of section 0 of the contact page: logarithms are natural and
I(P)=D(P\Vert P_X\otimes P_Y) as in (D2). Fix finite nonempty alphabets X,Y, a nonempty support
S\subseteq X\times Y with all rows and columns used, a feasible kernel w>0 on S as in (C1.1), and two distinct
positive contacts P,R of w as in (C1.2). Extend both laws by zero to the rectangle X\times Y; its cells outside
S are the holes. The fields f,g,U,V,A_0,B_0,s,J are those of (C1.3), and an unmarked expectation is under P.
Every marginal probability of a used symbol is positive, so f and g are positive and finite on every row and
column, every field below is finite on every cell of the rectangle, holes included, and both contacts have positive
marginals on every used symbol. Put
\begin{aligned}
z&=\frac{A_0-B_0}s,&v&=\frac{A_0B_0}{s^2}=\frac{1-z^2}4,&j&=\frac J{s^2},\\
\eta&=\frac{1+sj}4,&y&=1-s+sj,&t_0&=\frac12-j-\frac32z^2,
\end{aligned}
\qquad
D_X=E[V^2\mid X],\quad D_Y=E[U^2\mid Y].
\qquad \text{(PC4.1)}
Some letters are local to this page: z is an asymmetry and y a scalar, not a cell or a column symbol;
w_X,w_Y below are fields, not the kernel w; h below is a cross moment, not the seed entropy h; unadorned
D denotes the integrated variance, while D(\cdot\Vert\cdot) denotes relative entropy; u is a mixing parameter
and v a scalar, not the probability vectors of (C1.1) or the price bound u of the cap page;
j=J/s^2 is not the race price j(a); d_X,d_Y are fields, not the mismatch d; Q is a product law
and W a statistic, not the reference Q or the winner W of the race page; K(u) in the proof of Lemma PC4.5 is a
relative entropy, not the replica budget K, and \tau in its Lean note is a real parameter; F, F_l,
F_m, F_h in section 5 are scalar functions, not the cap F; M_l,M_m,M_h are polynomials, not the budget
M; and \beta,\gamma are the charge pair of section 0 of the contact page, while \alpha,\kappa,\lambda,k,c_0
are local coefficients.
Theorem9.1.1
✓L∃∀N
Associated Lean declarations
-
NaturalLatents.General.contact_moments[complete] -
NaturalLatents.General.contact_hessian[complete] -
NaturalLatents.General.pairCharge_contact_defect_X[complete] -
NaturalLatents.General.pairCharge_contact_defect_Y[complete] -
NaturalLatents.General.pairCharge_contact_defects_centered[complete] -
NaturalLatents.General.pairCharge_contact_gram_energy[complete] -
NaturalLatents.General.pairCharge_quarticRatio_bounds[complete] -
NaturalLatents.General.defect_bounds[complete] -
NaturalLatents.General.pairCharge_secant_mixed_moments[complete]
Lemma PC4.0 (the moment inputs). For every finite nonempty X,Y, every nonempty S with all rows and columns used,
every feasible w>0 on S, and every pair of distinct positive contacts P,R of w, the quantities (C1.3) and
(PC4.1) satisfy 0<A_0,B_0<1, 0<s<2, v\le1/4,
EU=-A_0,\quad EV=-B_0,\quad EU^2=2A_0-B_0,\quad EV^2=2B_0-A_0,\quad E[UV]=s\eta,\quad E[UV(U+V)]=-J,
\qquad \text{(PC4.M)}
and the centered conditionals 2E[V\mid X]+D_X=U and 2E[U\mid Y]+D_Y=V on used rows and columns. For every pair of
real marginal fields e_X on X and e_Y on Y with Ee_X=Ee_Y=0,
\mathcal Q(e):=Ee_X^2+Ee_Y^2-4E[e_Xe_Y]\ge0.
\qquad \text{(PC-H)}
The fields w_X=U+A_0, w_Y=V+B_0, d_X=D_X-(2B_0-A_0) and d_Y=D_Y-(2A_0-B_0) are centered and satisfy
d_X=w_X-2E[w_Y\mid X],\qquad d_Y=w_Y-2E[w_X\mid Y],
\qquad \text{(PC-C)}
and \mathcal Q(w)=s^2t_0, so that t_0\ge0, j\le1/2 and 1/16\le\eta^2\le j.
Lean code for Theorem9.1.1●9 theorems
Associated Lean declarations
-
NaturalLatents.General.contact_moments[complete]
-
NaturalLatents.General.contact_hessian[complete]
-
NaturalLatents.General.pairCharge_contact_defect_X[complete]
-
NaturalLatents.General.pairCharge_contact_defect_Y[complete]
-
NaturalLatents.General.pairCharge_contact_defects_centered[complete]
-
NaturalLatents.General.pairCharge_contact_gram_energy[complete]
-
NaturalLatents.General.pairCharge_quarticRatio_bounds[complete]
-
NaturalLatents.General.defect_bounds[complete]
-
NaturalLatents.General.pairCharge_secant_mixed_moments[complete]
Associated Lean declarations
-
NaturalLatents.General.contact_moments[complete] -
NaturalLatents.General.contact_hessian[complete] -
NaturalLatents.General.pairCharge_contact_defect_X[complete] -
NaturalLatents.General.pairCharge_contact_defect_Y[complete] -
NaturalLatents.General.pairCharge_contact_defects_centered[complete] -
NaturalLatents.General.pairCharge_contact_gram_energy[complete] -
NaturalLatents.General.pairCharge_quarticRatio_bounds[complete] -
NaturalLatents.General.defect_bounds[complete] -
NaturalLatents.General.pairCharge_secant_mixed_moments[complete]
-
theoremdefined in NaturalLatents/General/Contact.leancomplete
theorem NaturalLatents.General.contact_moments {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.ContactMoments S P R
theorem NaturalLatents.General.contact_moments {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.ContactMoments S P R
Two distinct positive contacts `P`, `R` of a common feasible kernel satisfy the moment relations of `ContactMoments`, in particular `quarticMoment P R ≤ separation P R ^ 2 / 2`.
-
theoremdefined in NaturalLatents/General/Contact.leancomplete
theorem NaturalLatents.General.contact_hessian {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P : NaturalLatents.General.Law X Y} (hw : stoch_to_det.Feasible S w) (hP : stoch_to_det.IsContact S w P) (F : X → ℝ) (G : Y → ℝ) (hF : (NaturalLatents.General.expect P fun z => F z.1) = 0) (hG : (NaturalLatents.General.expect P fun z => G z.2) = 0) : (4 * NaturalLatents.General.expect P fun z => F z.1 * G z.2) ≤ (NaturalLatents.General.expect P fun z => F z.1 ^ 2) + NaturalLatents.General.expect P fun z => G z.2 ^ 2
theorem NaturalLatents.General.contact_hessian {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P : NaturalLatents.General.Law X Y} (hw : stoch_to_det.Feasible S w) (hP : stoch_to_det.IsContact S w P) (F : X → ℝ) (G : Y → ℝ) (hF : (NaturalLatents.General.expect P fun z => F z.1) = 0) (hG : (NaturalLatents.General.expect P fun z => G z.2) = 0) : (4 * NaturalLatents.General.expect P fun z => F z.1 * G z.2) ≤ (NaturalLatents.General.expect P fun z => F z.1 ^ 2) + NaturalLatents.General.expect P fun z => G z.2 ^ 2
-
theoremdefined in NaturalLatents/General/PairCharge/Gram.leancomplete
theorem NaturalLatents.General.pairCharge_contact_defect_X {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) {x : X} (hx : x ∈ NaturalLatents.General.xSupport S) : (∑ y, P (x, y) * stoch_to_det.contactSecantY P R y ^ 2) / stoch_to_det.mX P x - (2 * NaturalLatents.General.defectY P R - NaturalLatents.General.defectX P R) = stoch_to_det.contactSecantX P R x + NaturalLatents.General.defectX P R - 2 * ((∑ y, P (x, y) * (stoch_to_det.contactSecantY P R y + NaturalLatents.General.defectY P R)) / stoch_to_det.mX P x)
theorem NaturalLatents.General.pairCharge_contact_defect_X {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) {x : X} (hx : x ∈ NaturalLatents.General.xSupport S) : (∑ y, P (x, y) * stoch_to_det.contactSecantY P R y ^ 2) / stoch_to_det.mX P x - (2 * NaturalLatents.General.defectY P R - NaturalLatents.General.defectX P R) = stoch_to_det.contactSecantX P R x + NaturalLatents.General.defectX P R - 2 * ((∑ y, P (x, y) * (stoch_to_det.contactSecantY P R y + NaturalLatents.General.defectY P R)) / stoch_to_det.mX P x)
-
theoremdefined in NaturalLatents/General/PairCharge/Gram.leancomplete
theorem NaturalLatents.General.pairCharge_contact_defect_Y {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) {y : Y} (hy : y ∈ NaturalLatents.General.ySupport S) : (∑ x, P (x, y) * stoch_to_det.contactSecantX P R x ^ 2) / stoch_to_det.mY P y - (2 * NaturalLatents.General.defectX P R - NaturalLatents.General.defectY P R) = stoch_to_det.contactSecantY P R y + NaturalLatents.General.defectY P R - 2 * ((∑ x, P (x, y) * (stoch_to_det.contactSecantX P R x + NaturalLatents.General.defectX P R)) / stoch_to_det.mY P y)
theorem NaturalLatents.General.pairCharge_contact_defect_Y {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) {y : Y} (hy : y ∈ NaturalLatents.General.ySupport S) : (∑ x, P (x, y) * stoch_to_det.contactSecantX P R x ^ 2) / stoch_to_det.mY P y - (2 * NaturalLatents.General.defectX P R - NaturalLatents.General.defectY P R) = stoch_to_det.contactSecantY P R y + NaturalLatents.General.defectY P R - 2 * ((∑ x, P (x, y) * (stoch_to_det.contactSecantX P R x + NaturalLatents.General.defectX P R)) / stoch_to_det.mY P y)
-
theoremdefined in NaturalLatents/General/PairCharge/Gram.leancomplete
theorem NaturalLatents.General.pairCharge_contact_defects_centered {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : (NaturalLatents.General.expect P fun z => (∑ y, P (z.1, y) * stoch_to_det.contactSecantY P R y ^ 2) / stoch_to_det.mX P z.1 - (2 * NaturalLatents.General.defectY P R - NaturalLatents.General.defectX P R)) = 0 ∧ (NaturalLatents.General.expect P fun z => (∑ x, P (x, z.2) * stoch_to_det.contactSecantX P R x ^ 2) / stoch_to_det.mY P z.2 - (2 * NaturalLatents.General.defectX P R - NaturalLatents.General.defectY P R)) = 0
theorem NaturalLatents.General.pairCharge_contact_defects_centered {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : (NaturalLatents.General.expect P fun z => (∑ y, P (z.1, y) * stoch_to_det.contactSecantY P R y ^ 2) / stoch_to_det.mX P z.1 - (2 * NaturalLatents.General.defectY P R - NaturalLatents.General.defectX P R)) = 0 ∧ (NaturalLatents.General.expect P fun z => (∑ x, P (x, z.2) * stoch_to_det.contactSecantX P R x ^ 2) / stoch_to_det.mY P z.2 - (2 * NaturalLatents.General.defectX P R - NaturalLatents.General.defectY P R)) = 0
-
theoremdefined in NaturalLatents/General/PairCharge/Gram.leancomplete
theorem NaturalLatents.General.pairCharge_contact_gram_energy {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : (((NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantX P R z.1 + NaturalLatents.General.defectX P R) ^ 2) + NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.defectY P R) ^ 2) - 4 * NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantX P R z.1 + NaturalLatents.General.defectX P R) * (stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.defectY P R)) = 6 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R - NaturalLatents.General.separation P R ^ 2 - NaturalLatents.General.quarticMoment P R
theorem NaturalLatents.General.pairCharge_contact_gram_energy {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : (((NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantX P R z.1 + NaturalLatents.General.defectX P R) ^ 2) + NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.defectY P R) ^ 2) - 4 * NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantX P R z.1 + NaturalLatents.General.defectX P R) * (stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.defectY P R)) = 6 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R - NaturalLatents.General.separation P R ^ 2 - NaturalLatents.General.quarticMoment P R
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_quarticRatio_bounds {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : 1 / 16 ≤ NaturalLatents.General.quarticRatio P R ∧ NaturalLatents.General.quarticRatio P R ≤ 1 / 2
theorem NaturalLatents.General.pairCharge_quarticRatio_bounds {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : 1 / 16 ≤ NaturalLatents.General.quarticRatio P R ∧ NaturalLatents.General.quarticRatio P R ≤ 1 / 2
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.defect_bounds {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : 2 / 9 ≤ NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / NaturalLatents.General.separation P R ^ 2 ∧ NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / NaturalLatents.General.separation P R ^ 2 ≤ 1 / 4
theorem NaturalLatents.General.defect_bounds {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : 2 / 9 ≤ NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / NaturalLatents.General.separation P R ^ 2 ∧ NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / NaturalLatents.General.separation P R ^ 2 ≤ 1 / 4
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_secant_mixed_moments {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : (NaturalLatents.General.expect P fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2 ^ 2) = (3 * (NaturalLatents.General.defectX P R - NaturalLatents.General.defectY P R) - NaturalLatents.General.quarticMoment P R) / 2 ∧ (NaturalLatents.General.expect P fun z => stoch_to_det.contactSecantX P R z.1 ^ 2 * stoch_to_det.contactSecantY P R z.2) = (-3 * (NaturalLatents.General.defectX P R - NaturalLatents.General.defectY P R) - NaturalLatents.General.quarticMoment P R) / 2
theorem NaturalLatents.General.pairCharge_secant_mixed_moments {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : (NaturalLatents.General.expect P fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2 ^ 2) = (3 * (NaturalLatents.General.defectX P R - NaturalLatents.General.defectY P R) - NaturalLatents.General.quarticMoment P R) / 2 ∧ (NaturalLatents.General.expect P fun z => stoch_to_det.contactSecantX P R z.1 ^ 2 * stoch_to_det.contactSecantY P R z.2) = (-3 * (NaturalLatents.General.defectX P R - NaturalLatents.General.defectY P R) - NaturalLatents.General.quarticMoment P R) / 2
Proof for Theorem 9.1.1
uses 0
Lean proves: the ContactMoments identities and bounds, the Hessian inequality (PC-H), the centered defect identities (PC-C), \mathcal Q(w)=6A_0B_0-s^2-J, 1/16\le j\le1/2, 2/9\le v\le1/4, and the two mixed moments whose sum is E[UV(U+V)]=-J.
Combine the contact moments and Hessian test with centering, conditional expansions, and Cauchy-Schwarz. See the page section.
Lean: contact_moments (NaturalLatents/General/Contact.lean) supplies the conditional and moment identities of
(C1.4), the energy and quartic identities, 0<s<2 and J\le6A_0B_0-s^2; the Hessian test (PC-H) is contact_hessian
(same file); the identities (PC-C) are
pairCharge_contact_defect_X and pairCharge_contact_defect_Y, the centering of d_X,d_Y is
pairCharge_contact_defects_centered, and \mathcal Q(w)=6A_0B_0-s^2-J is pairCharge_contact_gram_energy, all in
NaturalLatents/General/PairCharge/Gram.lean; the bounds on j and v are pairCharge_quarticRatio_bounds and
defect_bounds (NaturalLatents/General/PairCharge/MomentBounds.lean). The identity E[UV(U+V)]=-J is the sum of the
two parts of pairCharge_secant_mixed_moments (MomentBounds.lean), which states E[UV^2] and E[U^2V] separately; (PC-C) is stated at used rows and columns, with conditional expectations written as quotients of sums;
and defect_bounds also proves v\ge2/9, which this page does not use.
9.1.1. 4.1 Reversal and a corrected statistic
The reversed orientation takes R as reference and P as the second contact; its quantities carry a prime. In each
orientation, Q is the product of the reference marginals, positive on every cell of the rectangle, and
P_u=(1-u)Q+uP (with R in place of P for the reversed orientation). An overbar averages a quantity over the
two orientations with weight one half; in the reversed orientation E_P becomes E_R and E_Q becomes the
expectation under R_X\otimes R_Y. Define
\begin{aligned}
W&=\frac{(U+s/5)(V+s/5)}s,&\Theta&=\frac{D_X+D_Y}s-1,\\
\lambda&=\frac{27-55s}{40},\quad k=13\lambda+2s,\quad c_0=\frac32-\frac s2,&W_u&=W-\lambda u\Theta,\\
\mathrm{Res}&=\overline{\int_0^1(1-u)\mathrm{Var}_{P_u}W_u\,du}.
\end{aligned}
\qquad \text{(PC4.2)}
The correction leaves the expectation gap between the contact and the product law unchanged: \Theta has zero mean
under both P and Q (PC4.B), so E_PW_u-E_QW_u=E_PW-E_QW for every u. On 0<s\le1 the Hessian test
(PC-H) then bounds the integrated variance \mathrm{Res} by \mathrm{Den}(s,j)/192 (Lemma PC4.4), and
Cauchy–Schwarz turns the gap into the information floor (PC-FLOOR) of Lemma PC4.5.
Theorem9.1.1.1
✓L∃∀N
Associated Lean declarations
-
NaturalLatents.General.pairCharge_mean_losses_reverse[complete] -
NaturalLatents.General.pairCharge_separation_reverse[complete] -
NaturalLatents.General.pairCharge_quarticMoment_reverse[complete] -
NaturalLatents.General.pairCharge_quarticRatio_reverse[complete] -
NaturalLatents.General.pairCharge_defectProductRatio_reverse[complete] -
NaturalLatents.General.pairCharge_pair_reverse[complete] -
NaturalLatents.General.pairCharge_cond_defect_X_reverse[complete] -
NaturalLatents.General.pairCharge_cond_defect_Y_reverse[complete] -
NaturalLatents.General.pairCharge_fixed_coefficient_data[complete] -
NaturalLatents.General.pairCharge_fixed_endpoint_table[complete]
Lemma PC4.1 (reversal and raw moments). Under the hypotheses of Lemma PC4.0,
U'=-\frac Uf,\quad V'=-\frac Vg,\quad D_X'=\frac{D_X}f,\quad D_Y'=\frac{D_Y}g,\quad J'=J,\quad A_0'=B_0,\quad B_0'=A_0,
so s,j,z^2,v,t_0,\eta,y are common to both orientations. With \mu_Q=E_QW and \mu_P=E_PW,
\begin{aligned}
\mu_Q&=s\left(v-\frac4{25}\right),\qquad \mu_P=\eta-\frac{4s}{25},\\
E_QW^2&=\frac{[(2A_0-B_0)-2sA_0/5+s^2/25][(2B_0-A_0)-2sB_0/5+s^2/25]}{s^2},\\
E_PW^2&=\frac{J+(2s/5)(-J)+(s^2/25)(s+4s\eta)-2s^4/125+s^4/625}{s^2},
\end{aligned}
\qquad \text{(PC-W)}
and in terms of s,j,z these read
\mu_Q=\frac{s(1-z^2)}4-\frac{4s}{25},\quad \mu_P=\frac{1+sj}4-\frac{4s}{25},\quad
E_QW^2=\left(\frac12-\frac{4s}{25}\right)^2-z^2\left(\frac32-\frac s5\right)^2,\quad
E_PW^2=j\left(1-\frac s5\right)^2+\frac{2s}{25}-\frac{9s^2}{625}.
All four are invariant under reversal.
Lean code for Theorem9.1.1.1●10 theorems
Associated Lean declarations
-
NaturalLatents.General.pairCharge_mean_losses_reverse[complete]
-
NaturalLatents.General.pairCharge_separation_reverse[complete]
-
NaturalLatents.General.pairCharge_quarticMoment_reverse[complete]
-
NaturalLatents.General.pairCharge_quarticRatio_reverse[complete]
-
NaturalLatents.General.pairCharge_defectProductRatio_reverse[complete]
-
NaturalLatents.General.pairCharge_pair_reverse[complete]
-
NaturalLatents.General.pairCharge_cond_defect_X_reverse[complete]
-
NaturalLatents.General.pairCharge_cond_defect_Y_reverse[complete]
-
NaturalLatents.General.pairCharge_fixed_coefficient_data[complete]
-
NaturalLatents.General.pairCharge_fixed_endpoint_table[complete]
Associated Lean declarations
-
NaturalLatents.General.pairCharge_mean_losses_reverse[complete] -
NaturalLatents.General.pairCharge_separation_reverse[complete] -
NaturalLatents.General.pairCharge_quarticMoment_reverse[complete] -
NaturalLatents.General.pairCharge_quarticRatio_reverse[complete] -
NaturalLatents.General.pairCharge_defectProductRatio_reverse[complete] -
NaturalLatents.General.pairCharge_pair_reverse[complete] -
NaturalLatents.General.pairCharge_cond_defect_X_reverse[complete] -
NaturalLatents.General.pairCharge_cond_defect_Y_reverse[complete] -
NaturalLatents.General.pairCharge_fixed_coefficient_data[complete] -
NaturalLatents.General.pairCharge_fixed_endpoint_table[complete]
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_mean_losses_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.defectX R P = NaturalLatents.General.defectY P R ∧ NaturalLatents.General.defectY R P = NaturalLatents.General.defectX P R
theorem NaturalLatents.General.pairCharge_mean_losses_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.defectX R P = NaturalLatents.General.defectY P R ∧ NaturalLatents.General.defectY R P = NaturalLatents.General.defectX P R
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_separation_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.separation R P = NaturalLatents.General.separation P R
theorem NaturalLatents.General.pairCharge_separation_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.separation R P = NaturalLatents.General.separation P R
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_quarticMoment_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.quarticMoment R P = NaturalLatents.General.quarticMoment P R
theorem NaturalLatents.General.pairCharge_quarticMoment_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.quarticMoment R P = NaturalLatents.General.quarticMoment P R
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_quarticRatio_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.quarticRatio R P = NaturalLatents.General.quarticRatio P R
theorem NaturalLatents.General.pairCharge_quarticRatio_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.quarticRatio R P = NaturalLatents.General.quarticRatio P R
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_defectProductRatio_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.defectX R P * NaturalLatents.General.defectY R P / NaturalLatents.General.separation R P ^ 2 = NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / NaturalLatents.General.separation P R ^ 2
theorem NaturalLatents.General.pairCharge_defectProductRatio_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.defectX R P * NaturalLatents.General.defectY R P / NaturalLatents.General.separation R P ^ 2 = NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / NaturalLatents.General.separation P R ^ 2
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_pair_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.CommonSupportPair S w R P
theorem NaturalLatents.General.pairCharge_pair_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.CommonSupportPair S w R P
-
theoremdefined in NaturalLatents/General/PairCharge/Features.leancomplete
theorem NaturalLatents.General.pairCharge_cond_defect_X_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) {x : X} (hx : x ∈ NaturalLatents.General.xSupport S) : NaturalLatents.General.rootRatioX P R x * ((∑ y, R (x, y) * stoch_to_det.contactSecantY R P y ^ 2) / stoch_to_det.mX R x) = (∑ y, P (x, y) * stoch_to_det.contactSecantY P R y ^ 2) / stoch_to_det.mX P x
theorem NaturalLatents.General.pairCharge_cond_defect_X_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) {x : X} (hx : x ∈ NaturalLatents.General.xSupport S) : NaturalLatents.General.rootRatioX P R x * ((∑ y, R (x, y) * stoch_to_det.contactSecantY R P y ^ 2) / stoch_to_det.mX R x) = (∑ y, P (x, y) * stoch_to_det.contactSecantY P R y ^ 2) / stoch_to_det.mX P x
-
theoremdefined in NaturalLatents/General/PairCharge/Features.leancomplete
theorem NaturalLatents.General.pairCharge_cond_defect_Y_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) {y : Y} (hy : y ∈ NaturalLatents.General.ySupport S) : NaturalLatents.General.rootRatioY P R y * ((∑ x, R (x, y) * stoch_to_det.contactSecantX R P x ^ 2) / stoch_to_det.mY R y) = (∑ x, P (x, y) * stoch_to_det.contactSecantX P R x ^ 2) / stoch_to_det.mY P y
theorem NaturalLatents.General.pairCharge_cond_defect_Y_reverse {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) {y : Y} (hy : y ∈ NaturalLatents.General.ySupport S) : NaturalLatents.General.rootRatioY P R y * ((∑ x, R (x, y) * stoch_to_det.contactSecantX R P x ^ 2) / stoch_to_det.mY R y) = (∑ x, P (x, y) * stoch_to_det.contactSecantX P R x ^ 2) / stoch_to_det.mY P y
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_fixed_coefficient_data {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (c : ℝ) : have t := NaturalLatents.General.separation P R; have jj := NaturalLatents.General.quarticRatio P R; have vv := NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / t ^ 2; have hh := (1 + t * jj) / 4; have F := fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2 / t + c * (stoch_to_det.contactSecantX P R z.1 + stoch_to_det.contactSecantY P R z.2 + t); NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F = hh - t * vv ∧ (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => (F z - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F) ^ 2) / 3 + (NaturalLatents.General.expect P fun z => (F z - NaturalLatents.General.expect P F) ^ 2) / 6 + (NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F) ^ 2 / 12 = (9 * vv - 2) / 3 + jj / 6 - t ^ 2 * vv ^ 2 / 4 - t * vv * hh / 6 - hh ^ 2 / 12 + 2 * c * t * (3 / 8 - 2 * vv - jj / 6 + t * (vv / 3 + jj / 24)) + c ^ 2 * t * (7 / 12 - t / 2 + 2 * t * vv / 3 + t * jj / 12)
theorem NaturalLatents.General.pairCharge_fixed_coefficient_data {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (c : ℝ) : have t := NaturalLatents.General.separation P R; have jj := NaturalLatents.General.quarticRatio P R; have vv := NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / t ^ 2; have hh := (1 + t * jj) / 4; have F := fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2 / t + c * (stoch_to_det.contactSecantX P R z.1 + stoch_to_det.contactSecantY P R z.2 + t); NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F = hh - t * vv ∧ (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => (F z - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F) ^ 2) / 3 + (NaturalLatents.General.expect P fun z => (F z - NaturalLatents.General.expect P F) ^ 2) / 6 + (NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F) ^ 2 / 12 = (9 * vv - 2) / 3 + jj / 6 - t ^ 2 * vv ^ 2 / 4 - t * vv * hh / 6 - hh ^ 2 / 12 + 2 * c * t * (3 / 8 - 2 * vv - jj / 6 + t * (vv / 3 + jj / 24)) + c ^ 2 * t * (7 / 12 - t / 2 + 2 * t * vv / 3 + t * jj / 12)
Exact variance for any fixed additive correction.
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_fixed_endpoint_table {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : have H := fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2; have L := fun z => stoch_to_det.contactSecantX P R z.1 + stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.separation P R; NaturalLatents.General.expect P H = (NaturalLatents.General.separation P R + NaturalLatents.General.quarticMoment P R) / 4 ∧ NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) H = NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R ∧ NaturalLatents.General.expect P L = 0 ∧ NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) L = 0 ∧ (NaturalLatents.General.expect P fun z => H z ^ 2) = NaturalLatents.General.quarticMoment P R ∧ (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => H z ^ 2) = 9 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R - 2 * NaturalLatents.General.separation P R ^ 2 ∧ (NaturalLatents.General.expect P fun z => L z ^ 2) = 3 * NaturalLatents.General.separation P R / 2 - NaturalLatents.General.separation P R ^ 2 + NaturalLatents.General.quarticMoment P R / 2 ∧ (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => L z ^ 2) = NaturalLatents.General.separation P R - NaturalLatents.General.separation P R ^ 2 + 2 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R ∧ (NaturalLatents.General.expect P fun z => H z * L z) = -NaturalLatents.General.quarticMoment P R + NaturalLatents.General.separation P R * (NaturalLatents.General.separation P R + NaturalLatents.General.quarticMoment P R) / 4 ∧ (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => H z * L z) = NaturalLatents.General.separation P R ^ 2 - 6 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R + NaturalLatents.General.separation P R * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R
theorem NaturalLatents.General.pairCharge_fixed_endpoint_table {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : have H := fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2; have L := fun z => stoch_to_det.contactSecantX P R z.1 + stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.separation P R; NaturalLatents.General.expect P H = (NaturalLatents.General.separation P R + NaturalLatents.General.quarticMoment P R) / 4 ∧ NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) H = NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R ∧ NaturalLatents.General.expect P L = 0 ∧ NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) L = 0 ∧ (NaturalLatents.General.expect P fun z => H z ^ 2) = NaturalLatents.General.quarticMoment P R ∧ (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => H z ^ 2) = 9 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R - 2 * NaturalLatents.General.separation P R ^ 2 ∧ (NaturalLatents.General.expect P fun z => L z ^ 2) = 3 * NaturalLatents.General.separation P R / 2 - NaturalLatents.General.separation P R ^ 2 + NaturalLatents.General.quarticMoment P R / 2 ∧ (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => L z ^ 2) = NaturalLatents.General.separation P R - NaturalLatents.General.separation P R ^ 2 + 2 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R ∧ (NaturalLatents.General.expect P fun z => H z * L z) = -NaturalLatents.General.quarticMoment P R + NaturalLatents.General.separation P R * (NaturalLatents.General.separation P R + NaturalLatents.General.quarticMoment P R) / 4 ∧ (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => H z * L z) = NaturalLatents.General.separation P R ^ 2 - 6 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R + NaturalLatents.General.separation P R * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R
The exact endpoint table for the fixed quarter correction.
Proof for Theorem 9.1.1.1
uses 0
Lean proves: reversal of A_0,B_0,s,J,j,v and the conditional defects, the endpoint moments of UV and U+V+s, and the mean gap and collected algebraic variance of the statistic W+4s/25.
Change measure under contact reversal and expand the first and second moments under the contact and product laws. See the page section.
Lean: pairCharge_mean_losses_reverse, pairCharge_separation_reverse, pairCharge_quarticMoment_reverse, pairCharge_quarticRatio_reverse,
pairCharge_defectProductRatio_reverse and pairCharge_pair_reverse (NaturalLatents/General/PairCharge/MomentBounds.lean) and
pairCharge_cond_defect_X_reverse, pairCharge_cond_defect_Y_reverse
(NaturalLatents/General/PairCharge/Features.lean); pairCharge_fixed_coefficient_data (MomentBounds.lean) at
coefficient 1/5 gives the mean gap and the integrated variance D of Lemma PC4.3, from the component moments of
UV and U+V+s under P and Q in pairCharge_fixed_endpoint_table (MomentBounds.lean). Lean does not state
the four raw moments (PC-W) themselves, but states D directly in a collected form in s,j,v, and its statistic is
UV/s+(U+V+s)/5=W+4s/25, a constant shift that changes no gap, variance or product with \Theta.
9.1.2. 4.2 Correction products
In one orientation put
\rho=Ed_X^2+Ed_Y^2,\qquad h=E[d_Xd_Y],\qquad H_0=\frac{UV}s.
Since d_X+d_Y=D_X+D_Y-s, the correction field is \Theta=(d_X+d_Y)/s.
Theorem9.1.2.1
used by 1✓L∃∀N
Associated Lean declarations
-
NaturalLatents.General.pairCharge_correction_eq[complete] -
NaturalLatents.General.pairCharge_correction_means[complete] -
NaturalLatents.General.pairCharge_defect_products[complete] -
NaturalLatents.General.pairCharge_correction_second_moments[complete] -
NaturalLatents.General.pairCharge_linear_correction[complete] -
NaturalLatents.General.pairCharge_statistic_correction_average[complete] -
NaturalLatents.General.pairCharge_secantStatistic_correction_product[complete] -
NaturalLatents.General.pairCharge_secantStatistic_correction_joint[complete]
Lemma PC4.2 (correction products). Under the hypotheses of Lemma PC4.0, in each orientation,
\begin{aligned}
E[w_Xd_X+w_Yd_Y]&=s^2t_0,\qquad E[w_Xd_Y+w_Yd_X]=\frac{s^2t_0-\rho}2,
&&\text{(PC4.D)}\\
E_P\Theta&=E_Q\Theta=0,\qquad E_Q\Theta^2=\frac\rho{s^2},\qquad E_P\Theta^2=\frac{\rho+2h}{s^2},
&&\text{(PC4.B)}\\
E_Q[(w_X+w_Y)\Theta]+E_P[(w_X+w_Y)\Theta]&=\frac{5s^2t_0-\rho}{2s},
&&\text{(PC4.L)}
\end{aligned}
and, averaged over the two orientations,
\overline{E_Q(W\Theta)+E_P(W\Theta)}=j\left(1-\frac s4\right)-\frac14+c_0z^2-\frac{\bar\rho}{10s}.
\qquad \text{(PC-X)}
Lean code for Theorem9.1.2.1●8 theorems
Associated Lean declarations
-
NaturalLatents.General.pairCharge_correction_eq[complete]
-
NaturalLatents.General.pairCharge_correction_means[complete]
-
NaturalLatents.General.pairCharge_defect_products[complete]
-
NaturalLatents.General.pairCharge_correction_second_moments[complete]
-
NaturalLatents.General.pairCharge_linear_correction[complete]
-
NaturalLatents.General.pairCharge_statistic_correction_average[complete]
-
NaturalLatents.General.pairCharge_secantStatistic_correction_product[complete]
-
NaturalLatents.General.pairCharge_secantStatistic_correction_joint[complete]
Associated Lean declarations
-
NaturalLatents.General.pairCharge_correction_eq[complete] -
NaturalLatents.General.pairCharge_correction_means[complete] -
NaturalLatents.General.pairCharge_defect_products[complete] -
NaturalLatents.General.pairCharge_correction_second_moments[complete] -
NaturalLatents.General.pairCharge_linear_correction[complete] -
NaturalLatents.General.pairCharge_statistic_correction_average[complete] -
NaturalLatents.General.pairCharge_secantStatistic_correction_product[complete] -
NaturalLatents.General.pairCharge_secantStatistic_correction_joint[complete]
-
theoremdefined in NaturalLatents/General/PairCharge/Correction.leancomplete
theorem NaturalLatents.General.pairCharge_correction_eq {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] (P R : NaturalLatents.General.Law X Y) (hs : NaturalLatents.General.separation P R ≠ 0) (z : X × Y) : NaturalLatents.General.pairCharge_correction P R z = (NaturalLatents.General.pairCharge_defectX P R z.1 + NaturalLatents.General.pairCharge_defectY P R z.2) / NaturalLatents.General.separation P R
theorem NaturalLatents.General.pairCharge_correction_eq {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] (P R : NaturalLatents.General.Law X Y) (hs : NaturalLatents.General.separation P R ≠ 0) (z : X × Y) : NaturalLatents.General.pairCharge_correction P R z = (NaturalLatents.General.pairCharge_defectX P R z.1 + NaturalLatents.General.pairCharge_defectY P R z.2) / NaturalLatents.General.separation P R
The correction is the sum of the centered defects divided by separation.
-
theoremdefined in NaturalLatents/General/PairCharge/Correction.leancomplete
theorem NaturalLatents.General.pairCharge_correction_means {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.expect P (NaturalLatents.General.pairCharge_correction P R) = 0 ∧ NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) (NaturalLatents.General.pairCharge_correction P R) = 0
theorem NaturalLatents.General.pairCharge_correction_means {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : NaturalLatents.General.expect P (NaturalLatents.General.pairCharge_correction P R) = 0 ∧ NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) (NaturalLatents.General.pairCharge_correction P R) = 0
The correction has zero mean under the contact and its product law.
-
theoremdefined in NaturalLatents/General/PairCharge/Correction.leancomplete
theorem NaturalLatents.General.pairCharge_defect_products {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : ((NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantX P R z.1 + NaturalLatents.General.defectX P R) * NaturalLatents.General.pairCharge_defectX P R z.1) + NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.defectY P R) * NaturalLatents.General.pairCharge_defectY P R z.2) = 6 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R - NaturalLatents.General.separation P R ^ 2 - NaturalLatents.General.quarticMoment P R ∧ ((NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantX P R z.1 + NaturalLatents.General.defectX P R) * NaturalLatents.General.pairCharge_defectY P R z.2) + NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.defectY P R) * NaturalLatents.General.pairCharge_defectX P R z.1) = (6 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R - NaturalLatents.General.separation P R ^ 2 - NaturalLatents.General.quarticMoment P R - NaturalLatents.General.pairCharge_defectNorm P R) / 2
theorem NaturalLatents.General.pairCharge_defect_products {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : ((NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantX P R z.1 + NaturalLatents.General.defectX P R) * NaturalLatents.General.pairCharge_defectX P R z.1) + NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.defectY P R) * NaturalLatents.General.pairCharge_defectY P R z.2) = 6 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R - NaturalLatents.General.separation P R ^ 2 - NaturalLatents.General.quarticMoment P R ∧ ((NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantX P R z.1 + NaturalLatents.General.defectX P R) * NaturalLatents.General.pairCharge_defectY P R z.2) + NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.defectY P R) * NaturalLatents.General.pairCharge_defectX P R z.1) = (6 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R - NaturalLatents.General.separation P R ^ 2 - NaturalLatents.General.quarticMoment P R - NaturalLatents.General.pairCharge_defectNorm P R) / 2
The diagonal and off-diagonal products of shifted features with defects.
-
theoremdefined in NaturalLatents/General/PairCharge/Correction.leancomplete
theorem NaturalLatents.General.pairCharge_correction_second_moments {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => NaturalLatents.General.pairCharge_correction P R z ^ 2) = NaturalLatents.General.pairCharge_defectNorm P R / NaturalLatents.General.separation P R ^ 2 ∧ (NaturalLatents.General.expect P fun z => NaturalLatents.General.pairCharge_correction P R z ^ 2) = (NaturalLatents.General.pairCharge_defectNorm P R + 2 * NaturalLatents.General.pairCharge_defectCross P R) / NaturalLatents.General.separation P R ^ 2
theorem NaturalLatents.General.pairCharge_correction_second_moments {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => NaturalLatents.General.pairCharge_correction P R z ^ 2) = NaturalLatents.General.pairCharge_defectNorm P R / NaturalLatents.General.separation P R ^ 2 ∧ (NaturalLatents.General.expect P fun z => NaturalLatents.General.pairCharge_correction P R z ^ 2) = (NaturalLatents.General.pairCharge_defectNorm P R + 2 * NaturalLatents.General.pairCharge_defectCross P R) / NaturalLatents.General.separation P R ^ 2
The exact correction second moments under the two endpoint laws.
-
theoremdefined in NaturalLatents/General/PairCharge/Correction.leancomplete
theorem NaturalLatents.General.pairCharge_linear_correction {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : ((NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => (stoch_to_det.contactSecantX P R z.1 + stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.separation P R) * NaturalLatents.General.pairCharge_correction P R z) + NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantX P R z.1 + stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.separation P R) * NaturalLatents.General.pairCharge_correction P R z) = (5 * (6 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R - NaturalLatents.General.separation P R ^ 2 - NaturalLatents.General.quarticMoment P R) - NaturalLatents.General.pairCharge_defectNorm P R) / (2 * NaturalLatents.General.separation P R)
theorem NaturalLatents.General.pairCharge_linear_correction {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : ((NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => (stoch_to_det.contactSecantX P R z.1 + stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.separation P R) * NaturalLatents.General.pairCharge_correction P R z) + NaturalLatents.General.expect P fun z => (stoch_to_det.contactSecantX P R z.1 + stoch_to_det.contactSecantY P R z.2 + NaturalLatents.General.separation P R) * NaturalLatents.General.pairCharge_correction P R z) = (5 * (6 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R - NaturalLatents.General.separation P R ^ 2 - NaturalLatents.General.quarticMoment P R) - NaturalLatents.General.pairCharge_defectNorm P R) / (2 * NaturalLatents.General.separation P R)
The sum of the two endpoint products of the additive statistic and correction.
-
theoremdefined in NaturalLatents/General/PairCharge.leancomplete
theorem NaturalLatents.General.pairCharge_statistic_correction_average {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : (((NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => NaturalLatents.General.pairCharge_statistic P R z * NaturalLatents.General.pairCharge_correction P R z) + NaturalLatents.General.expect P fun z => NaturalLatents.General.pairCharge_statistic P R z * NaturalLatents.General.pairCharge_correction P R z) + ((NaturalLatents.General.expect (NaturalLatents.General.marginalProduct R) fun z => NaturalLatents.General.pairCharge_statistic R P z * NaturalLatents.General.pairCharge_correction R P z) + NaturalLatents.General.expect R fun z => NaturalLatents.General.pairCharge_statistic R P z * NaturalLatents.General.pairCharge_correction R P z)) / 2 = NaturalLatents.General.quarticRatio P R * (1 - NaturalLatents.General.separation P R / 4) - 1 / 4 + (3 / 2 - NaturalLatents.General.separation P R / 2) * (1 - 4 * (NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / NaturalLatents.General.separation P R ^ 2)) - (NaturalLatents.General.pairCharge_defectNorm P R + NaturalLatents.General.pairCharge_defectNorm R P) / (20 * NaturalLatents.General.separation P R)
theorem NaturalLatents.General.pairCharge_statistic_correction_average {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) : (((NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => NaturalLatents.General.pairCharge_statistic P R z * NaturalLatents.General.pairCharge_correction P R z) + NaturalLatents.General.expect P fun z => NaturalLatents.General.pairCharge_statistic P R z * NaturalLatents.General.pairCharge_correction P R z) + ((NaturalLatents.General.expect (NaturalLatents.General.marginalProduct R) fun z => NaturalLatents.General.pairCharge_statistic R P z * NaturalLatents.General.pairCharge_correction R P z) + NaturalLatents.General.expect R fun z => NaturalLatents.General.pairCharge_statistic R P z * NaturalLatents.General.pairCharge_correction R P z)) / 2 = NaturalLatents.General.quarticRatio P R * (1 - NaturalLatents.General.separation P R / 4) - 1 / 4 + (3 / 2 - NaturalLatents.General.separation P R / 2) * (1 - 4 * (NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / NaturalLatents.General.separation P R ^ 2)) - (NaturalLatents.General.pairCharge_defectNorm P R + NaturalLatents.General.pairCharge_defectNorm R P) / (20 * NaturalLatents.General.separation P R)
The paired change of measure gives the averaged statistic-correction product.
-
theoremdefined in NaturalLatents/General/PairCharge/Features.leancomplete
theorem NaturalLatents.General.pairCharge_secantStatistic_correction_product {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (DX : X → ℝ) (DY : Y → ℝ) (hDX : ∀ (x : X), DX x = (∑ y, P (x, y) * stoch_to_det.contactSecantY P R y ^ 2) / stoch_to_det.mX P x) (hDY : ∀ (y : Y), DY y = (∑ x, P (x, y) * stoch_to_det.contactSecantX P R x ^ 2) / stoch_to_det.mY P y) : (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2 / NaturalLatents.General.separation P R * ((DX z.1 + DY z.2) / NaturalLatents.General.separation P R - 1)) = 3 / 2 * ((NaturalLatents.General.defectX P R - NaturalLatents.General.defectY P R) / NaturalLatents.General.separation P R) ^ 2 + NaturalLatents.General.quarticMoment P R / (2 * NaturalLatents.General.separation P R) - NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / NaturalLatents.General.separation P R
theorem NaturalLatents.General.pairCharge_secantStatistic_correction_product {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (DX : X → ℝ) (DY : Y → ℝ) (hDX : ∀ (x : X), DX x = (∑ y, P (x, y) * stoch_to_det.contactSecantY P R y ^ 2) / stoch_to_det.mX P x) (hDY : ∀ (y : Y), DY y = (∑ x, P (x, y) * stoch_to_det.contactSecantX P R x ^ 2) / stoch_to_det.mY P y) : (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2 / NaturalLatents.General.separation P R * ((DX z.1 + DY z.2) / NaturalLatents.General.separation P R - 1)) = 3 / 2 * ((NaturalLatents.General.defectX P R - NaturalLatents.General.defectY P R) / NaturalLatents.General.separation P R) ^ 2 + NaturalLatents.General.quarticMoment P R / (2 * NaturalLatents.General.separation P R) - NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / NaturalLatents.General.separation P R
The product endpoint for `H` and `defectY`.
-
theoremdefined in NaturalLatents/General/PairCharge/Features.leancomplete
theorem NaturalLatents.General.pairCharge_secantStatistic_correction_joint {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (DX : X → ℝ) (DY : Y → ℝ) (hDX : ∀ (x : X), DX x = (∑ y, P (x, y) * stoch_to_det.contactSecantY P R y ^ 2) / stoch_to_det.mX P x) (hDY : ∀ (y : Y), DY y = (∑ x, P (x, y) * stoch_to_det.contactSecantX P R x ^ 2) / stoch_to_det.mY P y) : (NaturalLatents.General.expect P fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2 / NaturalLatents.General.separation P R * ((DX z.1 + DY z.2) / NaturalLatents.General.separation P R - 1)) = NaturalLatents.General.quarticMoment P R / NaturalLatents.General.separation P R ^ 2 - (NaturalLatents.General.expect P fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2) / NaturalLatents.General.separation P R - ((NaturalLatents.General.expect P fun z => stoch_to_det.contactSecantX P R z.1 * DX z.1 ^ 2) + NaturalLatents.General.expect P fun z => stoch_to_det.contactSecantY P R z.2 * DY z.2 ^ 2) / (2 * NaturalLatents.General.separation P R ^ 2)
theorem NaturalLatents.General.pairCharge_secantStatistic_correction_joint {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (DX : X → ℝ) (DY : Y → ℝ) (hDX : ∀ (x : X), DX x = (∑ y, P (x, y) * stoch_to_det.contactSecantY P R y ^ 2) / stoch_to_det.mX P x) (hDY : ∀ (y : Y), DY y = (∑ x, P (x, y) * stoch_to_det.contactSecantX P R x ^ 2) / stoch_to_det.mY P y) : (NaturalLatents.General.expect P fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2 / NaturalLatents.General.separation P R * ((DX z.1 + DY z.2) / NaturalLatents.General.separation P R - 1)) = NaturalLatents.General.quarticMoment P R / NaturalLatents.General.separation P R ^ 2 - (NaturalLatents.General.expect P fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2) / NaturalLatents.General.separation P R - ((NaturalLatents.General.expect P fun z => stoch_to_det.contactSecantX P R z.1 * DX z.1 ^ 2) + NaturalLatents.General.expect P fun z => stoch_to_det.contactSecantY P R z.2 * DY z.2 ^ 2) / (2 * NaturalLatents.General.separation P R ^ 2)
The unaveraged contact endpoint for `H` and `defectY`.
Proof for Theorem 9.1.2.1
uses 0
Use centered conditional defects for the linear products and a paired change of measure for the nonlinear correction product. See the page section.
Lean: pairCharge_correction_eq and pairCharge_correction_means (the form and means of \Theta),
pairCharge_defect_products (PC4.D), pairCharge_correction_second_moments (PC4.B) and pairCharge_linear_correction
(PC4.L), all in NaturalLatents/General/PairCharge/Correction.lean, which write s^2t_0 as 6A_0B_0-s^2-J; and
pairCharge_statistic_correction_average (PC-X) (NaturalLatents/General/PairCharge.lean), with the statistic
W+4s/25 and \bar\rho/(10s) written as (\rho+\rho')/(20s). Its proof uses
pairCharge_secantStatistic_correction_product (NaturalLatents/General/PairCharge/Features.lean), which states E_Q[H_0\Theta] in the
equivalent form 3z^2/2+J/(2s)-A_0B_0/s, and pairCharge_secantStatistic_correction_joint (same file), which states the
one-orientation product E_P[H_0\Theta] in a form that keeps the terms E[UD_X^2] and E[VD_Y^2].
9.1.3. 4.3 Integrated residual
Let
D=\frac{2E_QW^2+E_PW^2}6-\frac{3\mu_Q^2+2\mu_Q\mu_P+\mu_P^2}{12}.
Theorem9.1.3.1
✓L∃∀N
Associated Lean declarations
Lemma PC4.3 (the integrated residual). Under the hypotheses of Lemma PC4.0, with the definitions (PC4.2),
\mathrm{Res}=D-\frac\lambda6\overline{E_Q(W\Theta)+E_P(W\Theta)}+\frac{\lambda^2}{60s^2}\overline{5\rho+6h}.
\qquad \text{(PC-R1)}
The fields e_X=6\lambda d_X-kw_X and e_Y=6\lambda d_Y-kw_Y are centered, and
\mathcal Q(e)=36\lambda^2(\rho-4h)-12\lambda k\rho+k^2s^2t_0.
\qquad \text{(PC-R2)}
Consequently
192\,\mathrm{Res}=192D-32\lambda\left[j\left(1-\frac s4\right)-\frac14+c_0z^2\right]+\frac2{15}k^2t_0
-\frac2{15s^2}\overline{\mathcal Q(e)}.
\qquad \text{(PC-R3)}
(PC-R1) to (PC-R3) are exact identities; their proof divides only by s, never by \lambda, \rho or h.
Lean code for Theorem9.1.3.1●4 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in NaturalLatents/General/PairCharge.leancomplete
theorem NaturalLatents.General.pairCharge_residual_information {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {P : NaturalLatents.General.Law X Y} (hP : stoch_to_det.IsPMF P) (F C : X × Y → ℝ) (hCP : NaturalLatents.General.expect P C = 0) (hCQ : NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) C = 0) (hg : NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F ≠ 0) (lam : ℝ) : have gap := NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F; have D := (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => (F z - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F) ^ 2) / 3 + (NaturalLatents.General.expect P fun z => (F z - NaturalLatents.General.expect P F) ^ 2) / 6 + gap ^ 2 / 12; have N := ((NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => F z * C z) + NaturalLatents.General.expect P fun z => F z * C z) / 12; have W := (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => C z ^ 2) / 30 + (NaturalLatents.General.expect P fun z => C z ^ 2) / 20; 0 < D - 2 * lam * N + lam ^ 2 * W ∧ gap ^ 2 / (4 * (D - 2 * lam * N + lam ^ 2 * W)) ≤ stoch_to_det.Knat P
theorem NaturalLatents.General.pairCharge_residual_information {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {P : NaturalLatents.General.Law X Y} (hP : stoch_to_det.IsPMF P) (F C : X × Y → ℝ) (hCP : NaturalLatents.General.expect P C = 0) (hCQ : NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) C = 0) (hg : NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F ≠ 0) (lam : ℝ) : have gap := NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F; have D := (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => (F z - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F) ^ 2) / 3 + (NaturalLatents.General.expect P fun z => (F z - NaturalLatents.General.expect P F) ^ 2) / 6 + gap ^ 2 / 12; have N := ((NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => F z * C z) + NaturalLatents.General.expect P fun z => F z * C z) / 12; have W := (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => C z ^ 2) / 30 + (NaturalLatents.General.expect P fun z => C z ^ 2) / 20; 0 < D - 2 * lam * N + lam ^ 2 * W ∧ gap ^ 2 / (4 * (D - 2 * lam * N + lam ^ 2 * W)) ≤ stoch_to_det.Knat P
KL payment for `F - λ u C`, with both endpoint means of `C` zero.
-
theoremdefined in NaturalLatents/General/PairCharge/Correction.leancomplete
theorem NaturalLatents.General.pairCharge_correction_hessian {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (lam k : ℝ) : 0 ≤ 36 * lam ^ 2 * (NaturalLatents.General.pairCharge_defectNorm P R - 4 * NaturalLatents.General.pairCharge_defectCross P R) - 12 * lam * k * NaturalLatents.General.pairCharge_defectNorm P R + k ^ 2 * (6 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R - NaturalLatents.General.separation P R ^ 2 - NaturalLatents.General.quarticMoment P R)
theorem NaturalLatents.General.pairCharge_correction_hessian {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (lam k : ℝ) : 0 ≤ 36 * lam ^ 2 * (NaturalLatents.General.pairCharge_defectNorm P R - 4 * NaturalLatents.General.pairCharge_defectCross P R) - 12 * lam * k * NaturalLatents.General.pairCharge_defectNorm P R + k ^ 2 * (6 * NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R - NaturalLatents.General.separation P R ^ 2 - NaturalLatents.General.quarticMoment P R)
The feasibility Hessian evaluated on `6 * lam * defect - k * shifted feature`.
-
theoremdefined in NaturalLatents/General/PairCharge/Certificate.leancomplete
theorem NaturalLatents.General.pairCharge_residual_identity (s j v rho h D Xc : ℝ) (hs : s ≠ 0) (hD : D = (9 * v - 2) / 3 + j / 6 - s ^ 2 * v ^ 2 / 4 - s * v * ((1 + s * j) / 4) / 6 - ((1 + s * j) / 4) ^ 2 / 12 + 2 * (1 / 5) * s * (3 / 8 - 2 * v - j / 6 + s * (v / 3 + j / 24)) + (1 / 5) ^ 2 * s * (7 / 12 - s / 2 + 2 * s * v / 3 + s * j / 12)) (hX : Xc = j * (1 - s / 4) - 1 / 4 + (3 / 2 - s / 2) * (1 - 4 * v) - rho / (10 * s)) : 192 * (D - NaturalLatents.General.pairChargeSlope s / 6 * Xc + NaturalLatents.General.pairChargeSlope s ^ 2 * (5 * rho + 6 * h) / (60 * s ^ 2)) = NaturalLatents.General.pairChargeDenominator s j - (1 - 4 * v) * (48 * (3 - 101 * s / 120 + (7 / 200 - j / 24) * s ^ 2 + s ^ 2 * (1 - 4 * v) / 16) + 32 * NaturalLatents.General.pairChargeSlope s * (3 / 2 - s / 2) + NaturalLatents.General.pairChargeWeight s ^ 2 / 5) - 2 / (15 * s ^ 2) * (36 * NaturalLatents.General.pairChargeSlope s ^ 2 * (rho - 4 * h) - 12 * NaturalLatents.General.pairChargeSlope s * NaturalLatents.General.pairChargeWeight s * rho + NaturalLatents.General.pairChargeWeight s ^ 2 * (s ^ 2 * (6 * v - 1 - j)))
theorem NaturalLatents.General.pairCharge_residual_identity (s j v rho h D Xc : ℝ) (hs : s ≠ 0) (hD : D = (9 * v - 2) / 3 + j / 6 - s ^ 2 * v ^ 2 / 4 - s * v * ((1 + s * j) / 4) / 6 - ((1 + s * j) / 4) ^ 2 / 12 + 2 * (1 / 5) * s * (3 / 8 - 2 * v - j / 6 + s * (v / 3 + j / 24)) + (1 / 5) ^ 2 * s * (7 / 12 - s / 2 + 2 * s * v / 3 + s * j / 12)) (hX : Xc = j * (1 - s / 4) - 1 / 4 + (3 / 2 - s / 2) * (1 - 4 * v) - rho / (10 * s)) : 192 * (D - NaturalLatents.General.pairChargeSlope s / 6 * Xc + NaturalLatents.General.pairChargeSlope s ^ 2 * (5 * rho + 6 * h) / (60 * s ^ 2)) = NaturalLatents.General.pairChargeDenominator s j - (1 - 4 * v) * (48 * (3 - 101 * s / 120 + (7 / 200 - j / 24) * s ^ 2 + s ^ 2 * (1 - 4 * v) / 16) + 32 * NaturalLatents.General.pairChargeSlope s * (3 / 2 - s / 2) + NaturalLatents.General.pairChargeWeight s ^ 2 / 5) - 2 / (15 * s ^ 2) * (36 * NaturalLatents.General.pairChargeSlope s ^ 2 * (rho - 4 * h) - 12 * NaturalLatents.General.pairChargeSlope s * NaturalLatents.General.pairChargeWeight s * rho + NaturalLatents.General.pairChargeWeight s ^ 2 * (s ^ 2 * (6 * v - 1 - j)))
C5-C6, (R3)/(R4) as one exact identity. `D` is the integrated variance of the statistic in the form of `pairCharge_fixed_coefficient_data` at `c = 1/5`; `Xc` is the averaged correction product (X); `rho`, `h` are the averaged defect norm and cross moment; `v = a b / s^2`, so `z^2 = 1 - 4 v`.
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_fixed_coefficient_data {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (c : ℝ) : have t := NaturalLatents.General.separation P R; have jj := NaturalLatents.General.quarticRatio P R; have vv := NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / t ^ 2; have hh := (1 + t * jj) / 4; have F := fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2 / t + c * (stoch_to_det.contactSecantX P R z.1 + stoch_to_det.contactSecantY P R z.2 + t); NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F = hh - t * vv ∧ (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => (F z - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F) ^ 2) / 3 + (NaturalLatents.General.expect P fun z => (F z - NaturalLatents.General.expect P F) ^ 2) / 6 + (NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F) ^ 2 / 12 = (9 * vv - 2) / 3 + jj / 6 - t ^ 2 * vv ^ 2 / 4 - t * vv * hh / 6 - hh ^ 2 / 12 + 2 * c * t * (3 / 8 - 2 * vv - jj / 6 + t * (vv / 3 + jj / 24)) + c ^ 2 * t * (7 / 12 - t / 2 + 2 * t * vv / 3 + t * jj / 12)
theorem NaturalLatents.General.pairCharge_fixed_coefficient_data {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (c : ℝ) : have t := NaturalLatents.General.separation P R; have jj := NaturalLatents.General.quarticRatio P R; have vv := NaturalLatents.General.defectX P R * NaturalLatents.General.defectY P R / t ^ 2; have hh := (1 + t * jj) / 4; have F := fun z => stoch_to_det.contactSecantX P R z.1 * stoch_to_det.contactSecantY P R z.2 / t + c * (stoch_to_det.contactSecantX P R z.1 + stoch_to_det.contactSecantY P R z.2 + t); NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F = hh - t * vv ∧ (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => (F z - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F) ^ 2) / 3 + (NaturalLatents.General.expect P fun z => (F z - NaturalLatents.General.expect P F) ^ 2) / 6 + (NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F) ^ 2 / 12 = (9 * vv - 2) / 3 + jj / 6 - t ^ 2 * vv ^ 2 / 4 - t * vv * hh / 6 - hh ^ 2 / 12 + 2 * c * t * (3 / 8 - 2 * vv - jj / 6 + t * (vv / 3 + jj / 24)) + c ^ 2 * t * (7 / 12 - t / 2 + 2 * t * vv / 3 + t * jj / 12)
Exact variance for any fixed additive correction.
Proof for Theorem 9.1.3.1
uses 0
Lean proves: positivity and the information bound for the algebraic one-orientation residual, 0\le36\lambda^2(\rho-4h)-12\lambda k\rho+k^2s^2t_0, and the scalar collected residual identity pairCharge_residual_identity.
Integrate the corrected variance polynomial and complete the Hessian quadratic form using the defect products. See the page section.
Lean: the one-orientation shape of (PC-R1) is the residual in the conclusion of pairCharge_residual_information
(NaturalLatents/General/PairCharge.lean), with the statistic W+4s/25 and correction \Theta; the nonnegativity
consequence of (PC-R2) and (PC-H), 0\le36\lambda^2(\rho-4h)-12\lambda k\rho+k^2s^2t_0 for all real \lambda,k, is
pairCharge_correction_hessian (NaturalLatents/General/PairCharge/Correction.lean), which does not state the
equality (PC-R2) itself. (PC-R1) with (PC-X)
substituted, (PC-R3) and (PC-R4) below are one statement, pairCharge_residual_identity
(NaturalLatents/General/PairCharge/Certificate.lean), in the scalars s,j,v,\rho,h with z^2=1-4v, taking D
in the collected form of pairCharge_fixed_coefficient_data at coefficient 1/5, which equals (PC-D-RAW)
divided by 192.
9.1.4. 4.4 A direct residual bound
Define
\begin{aligned}
\mathrm{Den}(s,j)&=15+32j-\left(\frac{178}{25}+\frac{74j}5\right)s+\left(\frac{21}{25}+\frac{46j}{25}-j^2\right)s^2
-32\lambda\left[j\left(1-\frac s4\right)-\frac14\right]+\frac2{15}k^2\left(\frac12-j\right),\\
\Xi&=3-\frac{101}{120}s+\left(\frac7{200}-\frac j{24}\right)s^2+\frac{s^2z^2}{16}.
\end{aligned}
\qquad \text{(PC-DEN)}
Theorem9.1.4.1
Lemma PC4.4 (the residual bound). Under the hypotheses of Lemma PC4.0,
192D=15+32j-\left(\frac{178}{25}+\frac{74j}5\right)s+\left(\frac{21}{25}+\frac{46j}{25}-j^2\right)s^2-48z^2\Xi,
\qquad \text{(PC-D-RAW)}
192\,\mathrm{Res}=\mathrm{Den}(s,j)-z^2\left[48\Xi+32\lambda c_0+\frac{k^2}5\right]-\frac2{15s^2}\overline{\mathcal Q(e)},
\qquad \text{(PC-R4)}
and if 0<s\le1, then 192\,\mathrm{Res}\le \mathrm{Den}(s,j).
Lean code for Theorem9.1.4.1●4 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in NaturalLatents/General/PairCharge/Certificate.leancomplete
theorem NaturalLatents.General.pairCharge_residual_identity (s j v rho h D Xc : ℝ) (hs : s ≠ 0) (hD : D = (9 * v - 2) / 3 + j / 6 - s ^ 2 * v ^ 2 / 4 - s * v * ((1 + s * j) / 4) / 6 - ((1 + s * j) / 4) ^ 2 / 12 + 2 * (1 / 5) * s * (3 / 8 - 2 * v - j / 6 + s * (v / 3 + j / 24)) + (1 / 5) ^ 2 * s * (7 / 12 - s / 2 + 2 * s * v / 3 + s * j / 12)) (hX : Xc = j * (1 - s / 4) - 1 / 4 + (3 / 2 - s / 2) * (1 - 4 * v) - rho / (10 * s)) : 192 * (D - NaturalLatents.General.pairChargeSlope s / 6 * Xc + NaturalLatents.General.pairChargeSlope s ^ 2 * (5 * rho + 6 * h) / (60 * s ^ 2)) = NaturalLatents.General.pairChargeDenominator s j - (1 - 4 * v) * (48 * (3 - 101 * s / 120 + (7 / 200 - j / 24) * s ^ 2 + s ^ 2 * (1 - 4 * v) / 16) + 32 * NaturalLatents.General.pairChargeSlope s * (3 / 2 - s / 2) + NaturalLatents.General.pairChargeWeight s ^ 2 / 5) - 2 / (15 * s ^ 2) * (36 * NaturalLatents.General.pairChargeSlope s ^ 2 * (rho - 4 * h) - 12 * NaturalLatents.General.pairChargeSlope s * NaturalLatents.General.pairChargeWeight s * rho + NaturalLatents.General.pairChargeWeight s ^ 2 * (s ^ 2 * (6 * v - 1 - j)))
theorem NaturalLatents.General.pairCharge_residual_identity (s j v rho h D Xc : ℝ) (hs : s ≠ 0) (hD : D = (9 * v - 2) / 3 + j / 6 - s ^ 2 * v ^ 2 / 4 - s * v * ((1 + s * j) / 4) / 6 - ((1 + s * j) / 4) ^ 2 / 12 + 2 * (1 / 5) * s * (3 / 8 - 2 * v - j / 6 + s * (v / 3 + j / 24)) + (1 / 5) ^ 2 * s * (7 / 12 - s / 2 + 2 * s * v / 3 + s * j / 12)) (hX : Xc = j * (1 - s / 4) - 1 / 4 + (3 / 2 - s / 2) * (1 - 4 * v) - rho / (10 * s)) : 192 * (D - NaturalLatents.General.pairChargeSlope s / 6 * Xc + NaturalLatents.General.pairChargeSlope s ^ 2 * (5 * rho + 6 * h) / (60 * s ^ 2)) = NaturalLatents.General.pairChargeDenominator s j - (1 - 4 * v) * (48 * (3 - 101 * s / 120 + (7 / 200 - j / 24) * s ^ 2 + s ^ 2 * (1 - 4 * v) / 16) + 32 * NaturalLatents.General.pairChargeSlope s * (3 / 2 - s / 2) + NaturalLatents.General.pairChargeWeight s ^ 2 / 5) - 2 / (15 * s ^ 2) * (36 * NaturalLatents.General.pairChargeSlope s ^ 2 * (rho - 4 * h) - 12 * NaturalLatents.General.pairChargeSlope s * NaturalLatents.General.pairChargeWeight s * rho + NaturalLatents.General.pairChargeWeight s ^ 2 * (s ^ 2 * (6 * v - 1 - j)))
C5-C6, (R3)/(R4) as one exact identity. `D` is the integrated variance of the statistic in the form of `pairCharge_fixed_coefficient_data` at `c = 1/5`; `Xc` is the averaged correction product (X); `rho`, `h` are the averaged defect norm and cross moment; `v = a b / s^2`, so `z^2 = 1 - 4 v`.
-
theoremdefined in NaturalLatents/General/PairCharge/Certificate.leancomplete
theorem NaturalLatents.General.pairCharge_asymmetry_bracket {s j w : ℝ} (hs : 0 ≤ s) (hs1 : s ≤ 1) (hj : j ≤ 1 / 2) (hw : 0 ≤ w) : 70 ≤ 48 * (3 - 101 * s / 120 + (7 / 200 - j / 24) * s ^ 2 + s ^ 2 * w / 16) + 32 * NaturalLatents.General.pairChargeSlope s * (3 / 2 - s / 2) + NaturalLatents.General.pairChargeWeight s ^ 2 / 5
theorem NaturalLatents.General.pairCharge_asymmetry_bracket {s j w : ℝ} (hs : 0 ≤ s) (hs1 : s ≤ 1) (hj : j ≤ 1 / 2) (hw : 0 ≤ w) : 70 ≤ 48 * (3 - 101 * s / 120 + (7 / 200 - j / 24) * s ^ 2 + s ^ 2 * w / 16) + 32 * NaturalLatents.General.pairChargeSlope s * (3 / 2 - s / 2) + NaturalLatents.General.pairChargeWeight s ^ 2 / 5
C6, the asymmetry bracket of (R4): at least `70` (hence nonnegative) on `0 ≤ s ≤ 1`, `j ≤ 1/2`, for every `w = z^2 ≥ 0`.
-
theoremdefined in NaturalLatents/General/PairCharge/Certificate.leancomplete
theorem NaturalLatents.General.pairCharge_residual_le_denominator (s j v rho h D Xc : ℝ) (hs : 0 < s) (hs1 : s ≤ 1) (hj : j ≤ 1 / 2) (hv : v ≤ 1 / 4) (hD : D = (9 * v - 2) / 3 + j / 6 - s ^ 2 * v ^ 2 / 4 - s * v * ((1 + s * j) / 4) / 6 - ((1 + s * j) / 4) ^ 2 / 12 + 2 * (1 / 5) * s * (3 / 8 - 2 * v - j / 6 + s * (v / 3 + j / 24)) + (1 / 5) ^ 2 * s * (7 / 12 - s / 2 + 2 * s * v / 3 + s * j / 12)) (hX : Xc = j * (1 - s / 4) - 1 / 4 + (3 / 2 - s / 2) * (1 - 4 * v) - rho / (10 * s)) (hQ : 0 ≤ 36 * NaturalLatents.General.pairChargeSlope s ^ 2 * (rho - 4 * h) - 12 * NaturalLatents.General.pairChargeSlope s * NaturalLatents.General.pairChargeWeight s * rho + NaturalLatents.General.pairChargeWeight s ^ 2 * (s ^ 2 * (6 * v - 1 - j))) : 192 * (D - NaturalLatents.General.pairChargeSlope s / 6 * Xc + NaturalLatents.General.pairChargeSlope s ^ 2 * (5 * rho + 6 * h) / (60 * s ^ 2)) ≤ NaturalLatents.General.pairChargeDenominator s j
theorem NaturalLatents.General.pairCharge_residual_le_denominator (s j v rho h D Xc : ℝ) (hs : 0 < s) (hs1 : s ≤ 1) (hj : j ≤ 1 / 2) (hv : v ≤ 1 / 4) (hD : D = (9 * v - 2) / 3 + j / 6 - s ^ 2 * v ^ 2 / 4 - s * v * ((1 + s * j) / 4) / 6 - ((1 + s * j) / 4) ^ 2 / 12 + 2 * (1 / 5) * s * (3 / 8 - 2 * v - j / 6 + s * (v / 3 + j / 24)) + (1 / 5) ^ 2 * s * (7 / 12 - s / 2 + 2 * s * v / 3 + s * j / 12)) (hX : Xc = j * (1 - s / 4) - 1 / 4 + (3 / 2 - s / 2) * (1 - 4 * v) - rho / (10 * s)) (hQ : 0 ≤ 36 * NaturalLatents.General.pairChargeSlope s ^ 2 * (rho - 4 * h) - 12 * NaturalLatents.General.pairChargeSlope s * NaturalLatents.General.pairChargeWeight s * rho + NaturalLatents.General.pairChargeWeight s ^ 2 * (s ^ 2 * (6 * v - 1 - j))) : 192 * (D - NaturalLatents.General.pairChargeSlope s / 6 * Xc + NaturalLatents.General.pairChargeSlope s ^ 2 * (5 * rho + 6 * h) / (60 * s ^ 2)) ≤ NaturalLatents.General.pairChargeDenominator s j
C6, the direct residual bound `192 Res ≤ B(s, j)` in scalar form.
-
theoremdefined in NaturalLatents/General/PairCharge.leancomplete
theorem NaturalLatents.General.pairCharge_residual_bound {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (hs1 : NaturalLatents.General.separation P R ≤ 1) : 192 * ((NaturalLatents.General.pairCharge_residual P R (NaturalLatents.General.pairChargeSlope (NaturalLatents.General.separation P R)) + NaturalLatents.General.pairCharge_residual R P (NaturalLatents.General.pairChargeSlope (NaturalLatents.General.separation P R))) / 2) ≤ NaturalLatents.General.pairChargeDenominator (NaturalLatents.General.separation P R) (NaturalLatents.General.quarticRatio P R)
theorem NaturalLatents.General.pairCharge_residual_bound {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (hs1 : NaturalLatents.General.separation P R ≤ 1) : 192 * ((NaturalLatents.General.pairCharge_residual P R (NaturalLatents.General.pairChargeSlope (NaturalLatents.General.separation P R)) + NaturalLatents.General.pairCharge_residual R P (NaturalLatents.General.pairChargeSlope (NaturalLatents.General.separation P R))) / 2) ≤ NaturalLatents.General.pairChargeDenominator (NaturalLatents.General.separation P R) (NaturalLatents.General.quarticRatio P R)
The averaged residual is bounded by the scalar denominator divided by `192`.
Proof for Theorem 9.1.4.1
uses 0
Lean proves: the scalar collected residual identity pairCharge_residual_identity, the asymmetry-bracket lower bound 70, and 192\,\overline{\mathrm{pairCharge\_residual}}\le\mathrm{Den}(s,j) for 0<s\le1, with the residual defined algebraically.
Expand the scalar residual identity and discard the nonnegative asymmetry and Hessian terms after bounding their coefficients. See the page section.
Lean: pairCharge_residual_identity ((PC-R1) with (PC-X) substituted, (PC-R3) and (PC-R4) as one identity, with D in the
collected form of pairCharge_fixed_coefficient_data, equal to (PC-D-RAW) divided by 192),
pairCharge_asymmetry_bracket (the bound 70) and pairCharge_residual_le_denominator (the scalar form of the bound),
all in NaturalLatents/General/PairCharge/Certificate.lean; the bound for a contact pair is
pairCharge_residual_bound (NaturalLatents/General/PairCharge.lean), for s\le1.
9.1.5. 4.5 Information, support holes and positivity
Theorem9.1.5.1
used by 1✓L∃∀N
Associated Lean declarations
-
NaturalLatents.General.pairCharge_residual_information[complete] -
NaturalLatents.General.pairCharge_entropy_linear_field_affine[complete] -
NaturalLatents.General.pairCharge_entropy_path_payment[complete] -
stoch_to_det.joint_absCont_product[complete] -
NaturalLatents.General.pairCharge_fixed_floor_gap[complete] -
NaturalLatents.General.pairCharge_average_KL_separate[complete] -
NaturalLatents.General.pairCharge_projection_information[complete] -
NaturalLatents.General.pairCharge_information_floor[complete]
Lemma PC4.5 (the information floor). Under the hypotheses of Lemma PC4.0, if 0<s\le1, then \mathrm{Res}>0,
\mathrm{Den}(s,j)>0, and the averaged information \bar I=(I(P)+I(R))/2 satisfies
\bar I\ge\frac{3y^2}{\mathrm{Den}(s,j)}.
\qquad \text{(PC-FLOOR)}
Lean code for Theorem9.1.5.1●8 theorems
Associated Lean declarations
-
NaturalLatents.General.pairCharge_residual_information[complete]
-
NaturalLatents.General.pairCharge_entropy_linear_field_affine[complete]
-
NaturalLatents.General.pairCharge_entropy_path_payment[complete]
-
stoch_to_det.joint_absCont_product[complete]
-
NaturalLatents.General.pairCharge_fixed_floor_gap[complete]
-
NaturalLatents.General.pairCharge_average_KL_separate[complete]
-
NaturalLatents.General.pairCharge_projection_information[complete]
-
NaturalLatents.General.pairCharge_information_floor[complete]
Associated Lean declarations
-
NaturalLatents.General.pairCharge_residual_information[complete] -
NaturalLatents.General.pairCharge_entropy_linear_field_affine[complete] -
NaturalLatents.General.pairCharge_entropy_path_payment[complete] -
stoch_to_det.joint_absCont_product[complete] -
NaturalLatents.General.pairCharge_fixed_floor_gap[complete] -
NaturalLatents.General.pairCharge_average_KL_separate[complete] -
NaturalLatents.General.pairCharge_projection_information[complete] -
NaturalLatents.General.pairCharge_information_floor[complete]
-
theoremdefined in NaturalLatents/General/PairCharge.leancomplete
theorem NaturalLatents.General.pairCharge_residual_information {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {P : NaturalLatents.General.Law X Y} (hP : stoch_to_det.IsPMF P) (F C : X × Y → ℝ) (hCP : NaturalLatents.General.expect P C = 0) (hCQ : NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) C = 0) (hg : NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F ≠ 0) (lam : ℝ) : have gap := NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F; have D := (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => (F z - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F) ^ 2) / 3 + (NaturalLatents.General.expect P fun z => (F z - NaturalLatents.General.expect P F) ^ 2) / 6 + gap ^ 2 / 12; have N := ((NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => F z * C z) + NaturalLatents.General.expect P fun z => F z * C z) / 12; have W := (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => C z ^ 2) / 30 + (NaturalLatents.General.expect P fun z => C z ^ 2) / 20; 0 < D - 2 * lam * N + lam ^ 2 * W ∧ gap ^ 2 / (4 * (D - 2 * lam * N + lam ^ 2 * W)) ≤ stoch_to_det.Knat P
theorem NaturalLatents.General.pairCharge_residual_information {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {P : NaturalLatents.General.Law X Y} (hP : stoch_to_det.IsPMF P) (F C : X × Y → ℝ) (hCP : NaturalLatents.General.expect P C = 0) (hCQ : NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) C = 0) (hg : NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F ≠ 0) (lam : ℝ) : have gap := NaturalLatents.General.expect P F - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F; have D := (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => (F z - NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) F) ^ 2) / 3 + (NaturalLatents.General.expect P fun z => (F z - NaturalLatents.General.expect P F) ^ 2) / 6 + gap ^ 2 / 12; have N := ((NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => F z * C z) + NaturalLatents.General.expect P fun z => F z * C z) / 12; have W := (NaturalLatents.General.expect (NaturalLatents.General.marginalProduct P) fun z => C z ^ 2) / 30 + (NaturalLatents.General.expect P fun z => C z ^ 2) / 20; 0 < D - 2 * lam * N + lam ^ 2 * W ∧ gap ^ 2 / (4 * (D - 2 * lam * N + lam ^ 2 * W)) ≤ stoch_to_det.Knat P
KL payment for `F - λ u C`, with both endpoint means of `C` zero.
-
theoremdefined in NaturalLatents/General/PairCharge/Information.leancomplete
theorem NaturalLatents.General.pairCharge_entropy_linear_field_affine.{u_1} {Ω : Type u_1} [Fintype Ω] (P Q A B : Ω → ℝ) (hP : ∀ (i : Ω), 0 ≤ P i) (hQ : ∀ (i : Ω), 0 ≤ Q i) (hzero : ∀ (i : Ω), Q i = 0 → P i = 0) (hPt : ∑ i, P i = 1) (hQt : ∑ i, Q i = 1) (hB : ∑ i, (P i - Q i) * B i = 0) (τ : ℝ) : have Δ := ∑ i, (P i - Q i) * A i; have VQA := ∑ i, Q i * (A i - ∑ j, Q j * A j) ^ 2; have VPA := ∑ i, P i * (A i - ∑ j, P j * A j) ^ 2; have VQB := ∑ i, Q i * (B i - ∑ j, Q j * B j) ^ 2; have VPB := ∑ i, P i * (B i - ∑ j, P j * B j) ^ 2; have CQ := ∑ i, Q i * (A i - ∑ j, Q j * A j) * (B i - ∑ j, Q j * B j); have CP := ∑ i, P i * (A i - ∑ j, P j * A j) * (B i - ∑ j, P j * B j); τ * Δ ≤ ∑ i, Q i * stoch_to_det.phi (P i / Q i) + τ ^ 2 * (VQA / 3 + VPA / 6 + Δ ^ 2 / 12 + CQ / 6 + CP / 6 + VQB / 30 + VPB / 20)
theorem NaturalLatents.General.pairCharge_entropy_linear_field_affine.{u_1} {Ω : Type u_1} [Fintype Ω] (P Q A B : Ω → ℝ) (hP : ∀ (i : Ω), 0 ≤ P i) (hQ : ∀ (i : Ω), 0 ≤ Q i) (hzero : ∀ (i : Ω), Q i = 0 → P i = 0) (hPt : ∑ i, P i = 1) (hQt : ∑ i, Q i = 1) (hB : ∑ i, (P i - Q i) * B i = 0) (τ : ℝ) : have Δ := ∑ i, (P i - Q i) * A i; have VQA := ∑ i, Q i * (A i - ∑ j, Q j * A j) ^ 2; have VPA := ∑ i, P i * (A i - ∑ j, P j * A j) ^ 2; have VQB := ∑ i, Q i * (B i - ∑ j, Q j * B j) ^ 2; have VPB := ∑ i, P i * (B i - ∑ j, P j * B j) ^ 2; have CQ := ∑ i, Q i * (A i - ∑ j, Q j * A j) * (B i - ∑ j, Q j * B j); have CP := ∑ i, P i * (A i - ∑ j, P j * A j) * (B i - ∑ j, P j * B j); τ * Δ ≤ ∑ i, Q i * stoch_to_det.phi (P i / Q i) + τ ^ 2 * (VQA / 3 + VPA / 6 + Δ ^ 2 / 12 + CQ / 6 + CP / 6 + VQB / 30 + VPB / 20)
The entropy payment for an affine field of constant gap, with the exact covariance and variance weights.
-
theoremdefined in NaturalLatents/General/PairCharge/Information.leancomplete
theorem NaturalLatents.General.pairCharge_entropy_path_payment.{u_1} {Ω : Type u_1} [Fintype Ω] (P Q : Ω → ℝ) (hP : ∀ (i : Ω), 0 ≤ P i) (hQ : ∀ (i : Ω), 0 ≤ Q i) (hzero : ∀ (i : Ω), Q i = 0 → P i = 0) (hPt : ∑ i, P i = 1) (hQt : ∑ i, Q i = 1) (A : ℝ → Ω → ℝ) (Δ : ℝ) (H H' : ℝ → ℝ) (hHcont : Continuous H) (hH0 : H 0 = 0) (hH'0 : H' 0 = 0) (hgap : ∀ u ∈ Set.Ico 0 1, ∑ i, (P i - Q i) * A u i = Δ) (hH : ∀ u ∈ Set.Ico 0 1, HasDerivAt H (H' u) u) (hH' : ∀ u ∈ Set.Ico 0 1, HasDerivAt H' (∑ i, (Q i + u * (P i - Q i)) * (A u i - ∑ j, (Q j + u * (P j - Q j)) * A u j) ^ 2) u) (τ : ℝ) : τ * Δ ≤ ∑ i, Q i * stoch_to_det.phi (P i / Q i) + τ ^ 2 * H 1
theorem NaturalLatents.General.pairCharge_entropy_path_payment.{u_1} {Ω : Type u_1} [Fintype Ω] (P Q : Ω → ℝ) (hP : ∀ (i : Ω), 0 ≤ P i) (hQ : ∀ (i : Ω), 0 ≤ Q i) (hzero : ∀ (i : Ω), Q i = 0 → P i = 0) (hPt : ∑ i, P i = 1) (hQt : ∑ i, Q i = 1) (A : ℝ → Ω → ℝ) (Δ : ℝ) (H H' : ℝ → ℝ) (hHcont : Continuous H) (hH0 : H 0 = 0) (hH'0 : H' 0 = 0) (hgap : ∀ u ∈ Set.Ico 0 1, ∑ i, (P i - Q i) * A u i = Δ) (hH : ∀ u ∈ Set.Ico 0 1, HasDerivAt H (H' u) u) (hH' : ∀ u ∈ Set.Ico 0 1, HasDerivAt H' (∑ i, (Q i + u * (P i - Q i)) * (A u i - ∑ j, (Q j + u * (P j - Q j)) * A u j) ^ 2) u) (τ : ℝ) : τ * Δ ≤ ∑ i, Q i * stoch_to_det.phi (P i / Q i) + τ ^ 2 * H 1
A variance primitive gives the entropy payment. Null reference cells are allowed when the first law also vanishes.
-
theoremdefined in NaturalLatents/Upstream/ContactInformation.leancomplete
theorem stoch_to_det.joint_absCont_product.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {q : α × β → ℝ} (hq : stoch_to_det.IsPMF q) : stoch_to_det.AbsCont q fun z => stoch_to_det.mX q z.1 * stoch_to_det.mY q z.2
theorem stoch_to_det.joint_absCont_product.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {q : α × β → ℝ} (hq : stoch_to_det.IsPMF q) : stoch_to_det.AbsCont q fun z => stoch_to_det.mX q z.1 * stoch_to_det.mY q z.2
The product of marginals dominates the joint support.
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_fixed_floor_gap (s j v h : ℝ) (hslo : 0 ≤ s) (hvhi : v ≤ 1 / 4) (hh : h = (1 + s * j) / 4) : (1 - s + s * j) / 4 ≤ h - s * v
theorem NaturalLatents.General.pairCharge_fixed_floor_gap (s j v h : ℝ) (hslo : 0 ≤ s) (hvhi : v ≤ 1 / 4) (hh : h = (1 + s * j) / 4) : (1 - s + s * j) / 4 ≤ h - s * v
The mean-gap comparison; the lower bound on `v` is unnecessary.
-
theoremdefined in NaturalLatents/General/PairCharge.leancomplete
theorem NaturalLatents.General.pairCharge_average_KL_separate (Ip Im Vp Vm gp gm y : ℝ) (hVp : 0 < Vp) (hVm : 0 < Vm) (hy : 0 ≤ y) (hgp : y / 4 ≤ gp) (hgm : y / 4 ≤ gm) (hIp : gp ^ 2 / (4 * Vp) ≤ Ip) (hIm : gm ^ 2 / (4 * Vm) ≤ Im) : y ^ 2 / (64 * ((Vp + Vm) / 2)) ≤ (Ip + Im) / 2
theorem NaturalLatents.General.pairCharge_average_KL_separate (Ip Im Vp Vm gp gm y : ℝ) (hVp : 0 < Vp) (hVm : 0 < Vm) (hy : 0 ≤ y) (hgp : y / 4 ≤ gp) (hgm : y / 4 ≤ gm) (hIp : gp ^ 2 / (4 * Vp) ≤ Ip) (hIm : gm ^ 2 / (4 * Vm) ≤ Im) : y ^ 2 / (64 * ((Vp + Vm) / 2)) ≤ (Ip + Im) / 2
The reciprocal mean step with separate positive mean gaps.
-
theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.leancomplete
theorem NaturalLatents.General.pairCharge_projection_information (ibar y residual Dstar : ℝ) (hr : 0 < residual) (hrD : residual ≤ Dstar) (hinfo : y ^ 2 / (64 * residual) ≤ ibar) : 0 < Dstar ∧ 3 * y ^ 2 / (192 * Dstar) ≤ ibar
theorem NaturalLatents.General.pairCharge_projection_information (ibar y residual Dstar : ℝ) (hr : 0 < residual) (hrD : residual ≤ Dstar) (hinfo : y ^ 2 / (64 * residual) ≤ ibar) : 0 < Dstar ∧ 3 * y ^ 2 / (192 * Dstar) ≤ ibar
The denominator comparison after the fixed coefficient. All analytic obligations are the supplied positive residual variance and one KL lower bound at that coefficient.
-
theoremdefined in NaturalLatents/General/PairCharge.leancomplete
theorem NaturalLatents.General.pairCharge_information_floor {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (hs1 : NaturalLatents.General.separation P R ≤ 1) : 0 < NaturalLatents.General.pairChargeDenominator (NaturalLatents.General.separation P R) (NaturalLatents.General.quarticRatio P R) ∧ 3 * (1 - NaturalLatents.General.separation P R + NaturalLatents.General.separation P R * NaturalLatents.General.quarticRatio P R) ^ 2 / NaturalLatents.General.pairChargeDenominator (NaturalLatents.General.separation P R) (NaturalLatents.General.quarticRatio P R) ≤ (stoch_to_det.Knat P + stoch_to_det.Knat R) / 2
theorem NaturalLatents.General.pairCharge_information_floor {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y} (hpair : NaturalLatents.General.CommonSupportPair S w P R) (hs1 : NaturalLatents.General.separation P R ≤ 1) : 0 < NaturalLatents.General.pairChargeDenominator (NaturalLatents.General.separation P R) (NaturalLatents.General.quarticRatio P R) ∧ 3 * (1 - NaturalLatents.General.separation P R + NaturalLatents.General.separation P R * NaturalLatents.General.quarticRatio P R) ^ 2 / NaturalLatents.General.pairChargeDenominator (NaturalLatents.General.separation P R) (NaturalLatents.General.quarticRatio P R) ≤ (stoch_to_det.Knat P + stoch_to_det.Knat R) / 2
The positive scalar denominator gives the averaged information floor.
Proof for Theorem 9.1.5.1
uses 0
Lean proves: positivity and \Delta^2/(4\,\mathrm{Res}_P)\le I(P) for the algebraic one-orientation residual with nonzero gap, and \mathrm{Den}(s,j)>0 with the information floor (PC-FLOOR) for 0<s\le1.
Compare the expectation gap with the integrated variance by Cauchy-Schwarz and obtain the entropy path integral by a monotone limit, including support holes. See the page section.
Lean: pairCharge_residual_information (NaturalLatents/General/PairCharge.lean) proves, in one orientation and for
any statistic and any correction with zero means under P and Q and a nonzero gap, that the residual
\mathrm{Res}_P of that orientation alone (the integral in (PC4.2) without the average) is positive and
\Delta^2/(4\,\mathrm{Res}_P)\le I(P), holes allowed; it rests on pairCharge_entropy_linear_field_affine and
pairCharge_entropy_path_payment (NaturalLatents/General/PairCharge/Information.lean), with
stoch_to_det.joint_absCont_product (NaturalLatents/Upstream/ContactInformation.lean) supplying that P vanishes
where Q does. The bound \Delta\ge y/4 is pairCharge_fixed_floor_gap (MomentBounds.lean), the averaging step is
pairCharge_average_KL_separate (PairCharge.lean), and the division by \mathrm{Den}(s,j) is
pairCharge_projection_information (MomentBounds.lean); the assembled floor is pairCharge_information_floor
(PairCharge.lean), which states \mathrm{Den}(s,j)>0 and (PC-FLOOR) for s\le1. Lean has no integral formula for I(P): it proves \tau\Delta\le I(P)+\tau^2\,\mathrm{Res}_P in one
orientation, with \mathrm{Res}_P defined algebraically rather than by the integral in (PC4.2), for every real \tau, by a second-derivative comparison on [0,1) and continuity at u=1, and it
combines the two orientations by a reciprocal-mean step on their separate residuals rather than by one Cauchy-Schwarz
over the pooled measure.