EllipsoidDualCS.lean

1 import KomorebiLSM.EllipsoidGeometry
2 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
3 
4 /-! The actual inverse-metric dual Cauchy--Schwarz inequality and the mass
5 orientation implication used by the full P62 certificate. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.OrientedEllipsoid
8 open Matrix
9 open scoped BigOperators
10 variable {D : Type*} [Fintype D] [DecidableEq D]
11 
12 /-- The inverse in the dual quadratic form is the actual nonsingular matrix
13 inverse. Positivity of the primal metric entails this inequality. -/
14 theorem metric_dual_cauchy_schwarz (H : Matrix D D ℝ) (hH : H.PosDef)
15     (b y : D → ℝ) :
16     (b ⬝ᵥ y)^2 ≤ (b ⬝ᵥ (H⁻¹ *ᵥ b)) * (y ⬝ᵥ (H *ᵥ y)) := by
17   let L := factor H hH
18   let v := H⁻¹ *ᵥ b
19   have hL : L.transpose * L=H := factor_square H hH
20   have hHv : H *ᵥ v=b := by
21     change H *ᵥ (H⁻¹ *ᵥ b)=b
22     rw [Matrix.mulVec_mulVec,Matrix.mul_nonsing_inv _
23       ((Matrix.isUnit_iff_isUnit_det _).mp hH.isUnit),Matrix.one_mulVec]
24   have hcross : (L *ᵥ v) ⬝ᵥ (L *ᵥ y)=b ⬝ᵥ y := by
25     rw [← Matrix.dotProduct_transpose_mulVec L y (L *ᵥ v),Matrix.mulVec_mulVec,hL,hHv,
26       dotProduct_comm]
27   have hleft : (L *ᵥ v) ⬝ᵥ (L *ᵥ v)=b ⬝ᵥ (H⁻¹ *ᵥ b) := by
28     rw [← Matrix.dotProduct_transpose_mulVec L v (L *ᵥ v),Matrix.mulVec_mulVec,hL,hHv,
29       dotProduct_comm]
30   have hright : (L *ᵥ y) ⬝ᵥ (L *ᵥ y)=y ⬝ᵥ (H *ᵥ y) := by
31     rw [← Matrix.dotProduct_transpose_mulVec L y (L *ᵥ y),Matrix.mulVec_mulVec,hL]
32   have hcs : ((L *ᵥ v) ⬝ᵥ (L *ᵥ y))^2 ≤
33       ((L *ᵥ v) ⬝ᵥ (L *ᵥ v)) * ((L *ᵥ y) ⬝ᵥ (L *ᵥ y)) := by
34     simpa only [dotProduct,pow_two] using
35       Finset.sum_mul_sq_le_sq_mul_sq Finset.univ (L *ᵥ v) (L *ᵥ y)
36   rwa [hcross,hleft,hright] at hcs
37 
38 /-- The complete orientation hypotheses force the desired nonnegative mass
39 sheet, including zero mass and empty spatial dimension. -/
40 theorem mass_orientation (H : Matrix D D ℝ) (hH : H.PosDef)
41     (b y : D → ℝ) (β m : ℝ) (hm : 0≤m)
42     (hy : y ⬝ᵥ (H *ᵥ y)≤m^2) (hβ : 0≤β)
43     (hdual : 0≤β^2-b ⬝ᵥ (H⁻¹ *ᵥ b)) : 0≤β*m+b ⬝ᵥ y := by
44   have hq : 0≤y ⬝ᵥ (H *ᵥ y) := by
45     simpa only [Pi.star_apply,star_trivial] using hH.posSemidef.dotProduct_mulVec_nonneg y
46   have hbound : (b ⬝ᵥ y)^2≤(β*m)^2 := by
47     calc
48       _≤(b ⬝ᵥ (H⁻¹ *ᵥ b)) * (y ⬝ᵥ (H *ᵥ y)) := metric_dual_cauchy_schwarz H hH b y
49       _≤β^2*m^2 := mul_le_mul (sub_nonneg.mp hdual) hy hq (sq_nonneg β)
50       _=(β*m)^2 := by ring
51   have habs : |b ⬝ᵥ y|≤β*m :=
52     (sq_le_sq₀ (abs_nonneg _) (mul_nonneg hβ hm)).mp (by simpa only [sq_abs] using hbound)
53   linarith [(abs_le.mp habs).1]
54 
55 end Komorebi.LSM.OrientedEllipsoid

Back to source controls