Signed two-point square entropy upper bound
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.TwoPointEntropy.two_point_squared_entropy_le_half_sq_sub · theorem · Teaching coverage
Mathematical statement
For every signed real a,b, including zero, the homogeneous two-point entropy of their squares is at most half their squared difference.
Lean statement · two_point_squared_entropy_le_half_sq_sub
For every signed real a,b, including zero, the homogeneous two-point entropy of their squares is at most half their squared difference.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem two_point_squared_entropy_le_half_sq_sub (a b : ℝ) :
(a ^ 2 * Real.log (a ^ 2) + b ^ 2 * Real.log (b ^ 2)) / 2 -
((a ^ 2 + b ^ 2) / 2) * Real.log ((a ^ 2 + b ^ 2) / 2) ≤
(a - b) ^ 2 / 2Proof roadmap
- 1Positive squares: the upper Rothaus direction
For positive A,B, the actual scalar calculus proves the positive defect 2-2sqrt(1-t²)-phi(t) by two mean-value arguments, then rescales m=(A+B)/2, t=(A-B)/(A+B). All logarithm/sqrt derivative domains are proved inside the helper closure.
- 2Pass to signed inputs
Apply the positive inequality to A=a²,B=b², then use sqrt(a²)=|a| and the reverse absolute-value triangle inequality. This is the upper entropy bound, not the unrelated lower-bound theorem.
- 3Include zero values
If one square vanishes, expand log(A/2)=log A-log2. The remaining entropy is A log2/2≤A/2 because log2≤1; if both vanish, both sides are zero.
Full assumptions and notation
All objects and hypotheses
- Arbitrary a,b in real numbers; signed and zero inputs retained. No extra hypotheses.
Mathematical proof
1. Positive squares: the upper Rothaus direction
For positive A,B, the actual scalar calculus proves the positive defect 2-2sqrt(1-t²)-phi(t) by two mean-value arguments, then rescales m=(A+B)/2, t=(A-B)/(A+B). All logarithm/sqrt derivative domains are proved inside the helper closure.
Corresponding Lean step
private rothausDefect_nonneg; rothaus_lemma
2. Pass to signed inputs
Apply the positive inequality to A=a²,B=b², then use sqrt(a²)=|a| and the reverse absolute-value triangle inequality. This is the upper entropy bound, not the unrelated lower-bound theorem.
Corresponding Lean step
Real.sqrt_sq_eq_abs; abs_abs_sub_abs_le_abs_sub
3. Include zero values
If one square vanishes, expand log(A/2)=log A-log2. The remaining entropy is A log2/2≤A/2 because log2≤1; if both vanish, both sides are zero.
Corresponding Lean step
Real.log_div; Real.log_le_sub_one_of_pos; actual zero branches
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · two_point_squared_entropy_le_half_sq_sub
Positive squares: the upper Rothaus direction; Pass to signed inputs; Include zero values
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem two_point_squared_entropy_le_half_sq_sub (a b : ℝ) :
(a ^ 2 * Real.log (a ^ 2) + b ^ 2 * Real.log (b ^ 2)) / 2 -
((a ^ 2 + b ^ 2) / 2) * Real.log ((a ^ 2 + b ^ 2) / 2) ≤
(a - b) ^ 2 / 2 := by
have hlog2 : Real.log 2 ≤ 1 := by
have h := Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 2)
norm_num at h
exact h
by_cases ha : a = 0
· subst a
by_cases hb : b = 0
· simp [hb]
· have hb2 : b ^ 2 ≠ 0 := pow_ne_zero 2 hb
have hlog := Real.log_div hb2 (by norm_num : (2 : ℝ) ≠ 0)
simp only [zero_pow (by norm_num : (2 : ℕ) ≠ 0), zero_mul, zero_add,
zero_sub, neg_sq]
rw [hlog]
nlinarith [sq_nonneg b, mul_le_mul_of_nonneg_left hlog2 (sq_nonneg b)]
· by_cases hb : b = 0
· subst b
have ha2 : a ^ 2 ≠ 0 := pow_ne_zero 2 ha
have hlog := Real.log_div ha2 (by norm_num : (2 : ℝ) ≠ 0)
simp only [zero_pow (by norm_num : (2 : ℕ) ≠ 0), zero_mul, add_zero, sub_zero]
rw [hlog]
nlinarith [sq_nonneg a, mul_le_mul_of_nonneg_left hlog2 (sq_nonneg a)]
· have h := rothaus_lemma (sq_pos_of_ne_zero ha) (sq_pos_of_ne_zero hb)
rw [Real.sqrt_sq_eq_abs, Real.sqrt_sq_eq_abs] at h
have hab : (|a| - |b|)^2 ≤ (a-b)^2 := by
rw [sq_le_sq]
exact abs_abs_sub_abs_le_abs_sub a b
linarith
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.TwoPointEntropySource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Positive Rothaus and true finite Boolean function-LSI. | For every signed real a,b, including zero, the homogeneous two-point entropy of their squares is at most half their squared difference. | source-implicit | Signed squares including zero are internally derived from positive Rothaus; exact arbitrary Boolean function-LSI is unchanged. |
| Han tensorization implementation upstream. | Minimal private positive-Rothaus port. | same | Proof route disclosed; no caller certificate or statement weakening. |
| Gaussian limits and SPHMC LSI/T2/W2/main/composition. | Genuine signed two-point and true finite Bool function LSI with exact half coefficient, derived probability/L1 domains; authored direct RMS-induction route. No GaussianLSI/T2/FIRST4.6/W2/bias/main/work/composition. Focused2653 passed actual n0/indicator/signed/normalizedRademacher n2 tests; all6 prints standard3 only. Independent wholeproof/blind/source/exactcommit admission, integration and exposition remain separate. | unresolved | All downstream analytic/algorithm/cost dependencies remain open. |
Genuine signed two-point and true finite Bool function LSI with exact half coefficient, derived probability/L1 domains; authored direct RMS-induction route. No GaussianLSI/T2/FIRST4.6/W2/bias/main/work/composition. Focused2653 passed actual n0/indicator/signed/normalizedRademacher n2 tests; all6 prints standard3 only. Independent wholeproof/blind/source/exactcommit admission, integration and exposition remain separate.
Encoder–denoiser: accepted · equivalent-after-elaboration
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
Scope and omitted-condition boundaries
- Genuine signed two-point and true finite Bool function LSI with exact half coefficient, derived probability/L1 domains; authored direct RMS-induction route. No GaussianLSI/T2/FIRST4.6/W2/bias/main/work/composition. Focused2653 passed actual n0/indicator/signed/normalizedRademacher n2 tests; all6 prints standard3 only. Independent wholeproof/blind/source/exactcommit admission, integration and exposition remain separate.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- Real.log_le_sub_one_of_pos
- Real.sqrt_sq_eq_abs
Mathematical sources
- rothaus_lemma L734-L814 and signed-square/zero extension — Genuine signed two-point and true finite Bool function LSI with exact half coefficient, derived probability/L1 domains; authored direct RMS-induction route. No GaussianLSI/T2/FIRST4.6/W2/bias/main/work/composition. Focused2653 passed actual n0/indicator/signed/normalizedRademacher n2 tests; all6 prints standard3 only. Independent wholeproof/blind/source/exactcommit admission, integration and exposition remain separate.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.