Skip to content

Optimize PhaseRetrieval analytic proofs and shared estimates #701

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Vilin97 wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Optimize PhaseRetrieval analytic proofs and shared estimates #701

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 22 additions & 9 deletions LeanPool/PhaseRetrieval/Constant/Internal/HighFreqBandEstimate.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -345,7 +345,9 @@ private lemma parseval_partition {N L : ℕ}
simp only [smul_eq_mul]
unfold totalDelta Q
have hT_ne' : T ≠ 0 := ne_of_gt hT_pos
field_simp
have hcoefficient : (1 / T) * (T / (N : ℝ)) = 1 / (N : ℝ) := by
rw [one_div, div_eq_mul_inv, ← mul_assoc, inv_mul_cancel₀ hT_ne', one_mul, one_div]
rw [mul_add, ← mul_assoc, hcoefficient]

/-! ## Parseval identity for finite Fourier sums indexed by Fin L -/

Expand Down Expand Up @@ -935,7 +937,8 @@ private lemma assembly {N L : ℕ} (hN : 1 ≤ N)
((1/2) * (rho (fourier (N : ℤ) (↑t : AddCircle T) * qAvg b N k)) ^ 2 -
‖slowFactor b (↑t : AddCircle T) - qAvg b N k‖ ^ 2) =
(1/2) * A - B := by
simp_all
rw [intervalIntegral.integral_sub (hi_rho.const_mul _) hi_norm,
intervalIntegral.integral_const_mul]
rw [h_split] at h_int_bound
-- Multiply by 1/T
have h_mul := mul_le_mul_of_nonneg_left h_int_bound hT_inv_pos.le
Expand Down Expand Up @@ -998,9 +1001,12 @@ The hypothesis `1343 * L^2 ≤ N^2` implies `136π²(L-1)² ≤ 136π²L² ≤ 1

-- Numerical fact: 136 * π² < 1343
private lemma pi_sq_bound : 136 * Real.pi ^ 2 < 1343 := by
have hpi : Real.pi < 3.141593 := Real.pi_lt_d6
have hpi_pos : (0 : ℝ) < Real.pi := Real.pi_pos
nlinarith only [hpi, hpi_pos, sq_nonneg (3.141593 - Real.pi)]
calc
136 * Real.pi ^ 2 < 136 * (3.1416 : ℝ) ^ 2 :=
mul_lt_mul_of_pos_left
((sq_lt_sq₀ Real.pi_pos.le (by norm_num : (0 : ℝ) ≤ 3.1416)).2 Real.pi_lt_d4)
(by norm_num)
_ < 1343 := by norm_num

private lemma rho_integral_lower_bound {N L : ℕ}
(hN : 1 ≤ N) (hL : 1 ≤ L)
Expand Down Expand Up @@ -1036,16 +1042,23 @@ private lemma rho_integral_lower_bound {N L : ℕ}
exact_mod_cast this
-- Key: 4π²(L-1)² ≤ N²/34
have h_rate_bound : 34 * (4 * Real.pi ^ 2 * (↑L - 1) ^ 2) ≤ (↑N : ℝ) ^ 2 := by
have hLm1_sq : ((↑L : ℝ) - 1) ^ 2 ≤ (↑L : ℝ) ^ 2 := by apply sq_le_sq' <;> linarith
-- 34 * 4π² * (L-1)² ≤ 136π² * L² < 1343 * L² ≤ N²
nlinarith only [hpi2, hL_real, hNL_cast, sq_nonneg Real.pi, sq_nonneg (↑L : ℝ)]
have hLm1_sq : ((↑L : ℝ) - 1) ^ 2 ≤ (↑L : ℝ) ^ 2 := by
apply sq_le_sq' <;> linarith only [hL_real]
calc
34 * (4 * Real.pi ^ 2 * (↑L - 1) ^ 2) =
(136 * Real.pi ^ 2) * (↑L - 1) ^ 2 := by ring
_ ≤ (136 * Real.pi ^ 2) * (↑L : ℝ) ^ 2 :=
mul_le_mul_of_nonneg_left hLm1_sq (by positivity)
_ ≤ 1343 * (↑L : ℝ) ^ 2 :=
mul_le_mul_of_nonneg_right hpi2.le (sq_nonneg _)
_ ≤ (↑N : ℝ) ^ 2 := hNL_cast
-- r·C ≤ C/34 where r = 4π²(L-1)²/N²
have h_key : 4 * Real.pi ^ 2 * (↑L - 1) ^ 2 / ↑N ^ 2 * C ≤ C / 34 := by
have h1 : 4 * Real.pi ^ 2 * (↑L - 1) ^ 2 / ↑N ^ 2 ≤ 1 / 34 := by
rw [div_le_div_iff₀ hN2_pos (by norm_num : (0:ℝ) < 34)]
linarith only [h_rate_bound]
calc 4 * Real.pi ^ 2 * (↑L - 1) ^ 2 / ↑N ^ 2 * C
≤ (1 / 34) * C := by nlinarith only [h_nn, h1]
≤ (1 / 34) * C := mul_le_mul_of_nonneg_right h1 h_nn
_ = C / 34 := by ring
-- Combine: ∫ρ² ≥ C/16 - (17/16)δ ≥ C/16 - (17/16)·(C/34) = C/16 - C/32 = C/32
linarith only [h_asm, h_poi, h_key]
Expand Down
195 changes: 36 additions & 159 deletions LeanPool/PhaseRetrieval/DimdPoly/Internal/CoefficientLimitRigidity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,38 +50,13 @@ private theorem norm_nonneg_pkappa_coeff_wip
private theorem toFun_ofPkappa_wip
{d : Nat} (kappa : MultiIndex d) (F : Pkappa d kappa) :
toFun kappa (ofPkappa kappa F) = evalPkappa kappa F := by
ext z
rw [toFun, evalPkappa, Finsupp.sum]
have hzero :
∀ alpha ∉ F.support,
coeffSkappa (ofPkappa kappa F) alpha * Phi kappa alpha z = 0 := by
intro alpha halpha
simp [coeffSkappa, ofPkappa, Finsupp.notMem_support_iff.mp halpha]
rw [tsum_eq_sum hzero]
refine Finset.sum_congr rfl ?_
intro alpha halpha
simp [coeffSkappa, ofPkappa]
exact toFun_ofPkappa kappa F

private theorem summable_skappa_eval_mul_of_phi_sq_wip
{d : Nat} (kappa : MultiIndex d) (U : Skappa d kappa) (z : Cd d)
(hPhi : Summable (fun alpha : Idx d => ‖Phi kappa alpha z‖ ^ 2)) :
Summable (fun alpha : Idx d => coeffSkappa U alpha * Phi kappa alpha z) := by
have hU : Summable (fun alpha : Idx d => ‖coeffSkappa U alpha‖ ^ 2) := by
exact U.summable_norm_sq
refine Summable.of_norm_bounded
(g := fun alpha : Idx d =>
(‖coeffSkappa U alpha‖ ^ 2 + ‖Phi kappa alpha z‖ ^ 2) / 2)
((hU.add hPhi).div_const 2) ?_
intro alpha
have hmul :
‖coeffSkappa U alpha * Phi kappa alpha z‖ <=
‖coeffSkappa U alpha‖ * ‖Phi kappa alpha z‖ :=
norm_mul_le _ _
have hsq :
‖coeffSkappa U alpha‖ * ‖Phi kappa alpha z‖ <=
(‖coeffSkappa U alpha‖ ^ 2 + ‖Phi kappa alpha z‖ ^ 2) / 2 := by
nlinarith only [sq_nonneg (‖coeffSkappa U alpha‖ - ‖Phi kappa alpha z‖)]
exact le_trans hmul hsq
exact summable_skappa_eval_mul_of_phi_sq kappa U z hPhi

private theorem finite_eval_sum_tendsto_wip
{d : Nat} {kappa : MultiIndex d}
Expand Down Expand Up @@ -133,59 +108,12 @@ private theorem phi1D_eq_oneDimPhi_wip
private theorem summable_sq_hermite_phi_eval_wip
(k : Nat) (z : ℂ) :
Summable (fun n : Nat => ‖HermitekLEAN.Phi k n z‖ ^ 2) := by
obtain ⟨C, hC_nonneg, hC⟩ := HermitekLEAN.point_eval_bounded (k := k) z
apply summable_of_sum_range_le (c := C ^ 2) (fun n => sq_nonneg _)
intro J
let a' : Fin J -> ℂ := fun n => star (HermitekLEAN.Phi k n.1 z)
have hNS :
HermitekLEAN.weightedNormSq (HermitekLEAN.finiteHermiteSum k a') =
Finset.sum Finset.univ (fun n : Fin J => ‖HermitekLEAN.Phi k n.1 z‖ ^ 2) := by
rw [HermitekLEAN.finiteHermiteSum_normSq]
refine Finset.sum_congr rfl ?_
intro n hn
simp [a']
let S : ℝ := Finset.sum Finset.univ
(fun n : Fin J => ‖HermitekLEAN.Phi k n.1 z‖ ^ 2)
have hS_nonneg : 0 <= S := by
dsimp [S]
exact Finset.sum_nonneg fun n hn => sq_nonneg _
have hWN :
HermitekLEAN.weightedNorm (HermitekLEAN.finiteHermiteSum k a') =
Real.sqrt S := by
change Real.sqrt (HermitekLEAN.weightedNormSq (HermitekLEAN.finiteHermiteSum k a')) =
Real.sqrt S
rw [hNS]
have hFz : HermitekLEAN.finiteHermiteSum k a' z = (S : ℂ) := by
simp only [HermitekLEAN.finiteHermiteSum, a', S]
push_cast
congr 1
ext1 n
calc
star (HermitekLEAN.Phi k n.1 z) * HermitekLEAN.Phi k n.1 z
= HermitekLEAN.Phi k n.1 z * star (HermitekLEAN.Phi k n.1 z) := by ring
_ = (‖HermitekLEAN.Phi k n.1 z‖ ^ 2 : ℂ) := by
simpa [Complex.normSq_eq_norm_sq] using
Complex.mul_conj (HermitekLEAN.Phi k n.1 z)
have hev :
‖HermitekLEAN.finiteHermiteSum k a' z‖ <=
C * HermitekLEAN.weightedNorm (HermitekLEAN.finiteHermiteSum k a') :=
hC (HermitekLEAN.finiteHermiteSum_mem_Hk k a')
have hFz_bound : S <= ‖HermitekLEAN.finiteHermiteSum k a' z‖ := by
calc
S <= |S| := le_abs_self S
_ = ‖(S : ℂ)‖ := (Complex.norm_real S).symm
_ = ‖HermitekLEAN.finiteHermiteSum k a' z‖ := by rw [hFz]
have hSle : S <= C ^ 2 := by
have hev' : ‖HermitekLEAN.finiteHermiteSum k a' z‖ <= C * Real.sqrt S := by
simpa [hWN] using hev
linarith only [
hS_nonneg, hFz_bound, hev', Real.sq_sqrt hS_nonneg, sq_nonneg (Real.sqrt S - C),
hC_nonneg
]
calc
Finset.sum (Finset.range J) (fun n => ‖HermitekLEAN.Phi k n z‖ ^ 2)
= S := (Fin.sum_univ_eq_sum_range (fun n : Nat => ‖HermitekLEAN.Phi k n z‖ ^ 2) J).symm
_ <= C ^ 2 := hSle
-- Preserve the imported definition's local equation lemma.
have hsum_apply {D : ℕ} (a : Fin D → ℂ) (w : ℂ) :
HermitekLEAN.finiteHermiteSum k a w =
∑ n : Fin D, a n * HermitekLEAN.Phi k n.1 w := by
simp only [HermitekLEAN.finiteHermiteSum]
exact HermitekLEAN.summable_norm_sq_Phi_eval k z

private theorem summable_sq_phi1D_eval_wip
(k : Nat) (z : ℂ) :
Expand All @@ -210,59 +138,12 @@ private theorem Phi_norm_sq_eq_prod_wip
private theorem summable_sq_Phi_eval_wip
{d : Nat} (kappa : MultiIndex d) (z : Cd d) :
Summable (fun alpha : Idx d => ‖Phi kappa alpha z‖ ^ 2) := by
refine summable_of_sum_le
(c := Finset.prod Finset.univ
(fun q : Fin d => ∑' n : Nat, ‖phi1D (kappa q) n (z q)‖ ^ 2))
(fun alpha : Idx d => sq_nonneg _) ?_
intro E
let J : Fin d -> Nat := fun q => Finset.sup E (fun alpha : Idx d => alpha q)
let B : Finset (Idx d) := Fintype.piFinset fun q : Fin d => Finset.range (J q + 1)
have hE_subset : E ⊆ B := by
intro alpha halpha
dsimp [B]
rw [Fintype.mem_piFinset]
intro q
rw [Finset.mem_range, Nat.lt_succ_iff]
exact Finset.le_sup (s := E) (f := fun beta : Idx d => beta q) halpha
have hsum_E_le_B :
Finset.sum E (fun alpha : Idx d => ‖Phi kappa alpha z‖ ^ 2) <=
Finset.sum B (fun alpha : Idx d => ‖Phi kappa alpha z‖ ^ 2) := by
exact Finset.sum_le_sum_of_subset_of_nonneg hE_subset
(by intro alpha hB hnot; exact sq_nonneg _)
have hbox_eq :
Finset.sum B (fun alpha : Idx d => ‖Phi kappa alpha z‖ ^ 2) =
Finset.prod Finset.univ
(fun q : Fin d =>
Finset.sum (Finset.range (J q + 1))
(fun n : Nat => ‖phi1D (kappa q) n (z q)‖ ^ 2)) := by
dsimp [B]
symm
rw [Finset.prod_univ_sum]
refine Finset.sum_congr rfl ?_
intro alpha halpha
exact (Phi_norm_sq_eq_prod_wip kappa alpha z).symm
have hprod_le :
Finset.prod Finset.univ
(fun q : Fin d =>
Finset.sum (Finset.range (J q + 1))
(fun n : Nat => ‖phi1D (kappa q) n (z q)‖ ^ 2)) <=
Finset.prod Finset.univ
(fun q : Fin d =>
∑' n : Nat, ‖phi1D (kappa q) n (z q)‖ ^ 2) := Finset.prod_le_prod₀
(by
intro q hq
exact Finset.sum_nonneg fun n hn => sq_nonneg _)
(by
intro q hq
exact (summable_sq_phi1D_eval_wip (kappa q) (z q)).sum_le_tsum
(Finset.range (J q + 1)) (fun n hn => sq_nonneg _))
exact le_trans hsum_E_le_B (by rw [hbox_eq]; exact hprod_le)
exact summable_sq_Phi_eval kappa z

private theorem summable_skappa_eval_mul_wip
{d : Nat} (kappa : MultiIndex d) (U : Skappa d kappa) (z : Cd d) :
Summable (fun alpha : Idx d => coeffSkappa U alpha * Phi kappa alpha z) :=
summable_skappa_eval_mul_of_phi_sq_wip kappa U z
(summable_sq_Phi_eval_wip kappa z)
Summable (fun alpha : Idx d => coeffSkappa U alpha * Phi kappa alpha z) := by
exact summable_skappa_eval_mul kappa U z

private theorem summable_pkappa_eval_mul_wip
{d : Nat} (kappa : MultiIndex d) (H : Pkappa d kappa) (z : Cd d) :
Expand Down Expand Up @@ -1365,16 +1246,12 @@ private theorem defect_nonneg_wip
private lemma continuous_Phi_coeff_wip
{d : Nat} (kappa alpha : MultiIndex d) :
Continuous (Phi kappa alpha) := by
unfold Phi phi1D complexHermite
continuity
exact continuous_Phi kappa alpha

private lemma continuous_evalPkappa_coeff_wip
{d : Nat} (kappa : MultiIndex d) (F : Pkappa d kappa) :
Continuous (evalPkappa kappa F) := by
unfold evalPkappa
refine continuous_finsetSum _ ?_
intro alpha halpha
exact continuous_const.mul (continuous_Phi_coeff_wip kappa alpha)
exact continuous_evalPkappa kappa F

private def defectFunctionPkappa_coeff_wip
{d : Nat} (kappa : MultiIndex d) (F G : Pkappa d kappa) :
Expand Down Expand Up @@ -1473,22 +1350,7 @@ private theorem integrable_evalPkappa_sq_coeff_wip
{d : Nat} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) :
MeasureTheory.Integrable
(fun z : Cd d => ‖evalPkappa kappa F z‖ ^ 2) (gammaD d) := by
by_cases hF : F = 0
· subst hF
simp [evalPkappa]
· have hmeas :
MeasureTheory.AEStronglyMeasurable (fun z : Cd d => ‖evalPkappa kappa F z‖ ^ 2)
(gammaD d) :=
((continuous_evalPkappa_coeff_wip kappa F).norm.pow 2).stronglyMeasurable.aestronglyMeasurable
by_contra hInt
have hundef :
(∫ z : Cd d, ‖evalPkappa kappa F z‖ ^ 2 ∂ gammaD d) = 0 :=
MeasureTheory.integral_undef hInt
have hmass :
(∫ z : Cd d, ‖evalPkappa kappa F z‖ ^ 2 ∂ gammaD d) = ‖F‖ ^ 2 :=
evalPkappa_total_mass hd kappa F
have hnorm_ne : ‖F‖ ≠ 0 := norm_ne_zero_of_ne_zero_pkappa_coeff_wip hF
simp_all
exact integrable_evalPkappa_sq hd kappa F

private theorem gaussianL2Norm_eq_lpNorm_coeff_wip
{d : Nat} {α : Type*} [NormedAddCommGroup α]
Expand All @@ -1512,13 +1374,7 @@ private theorem gaussianL2Norm_eq_lpNorm_coeff_wip
private theorem memLp_two_evalPkappa_coeff_wip
{d : Nat} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) :
MeasureTheory.MemLp (evalPkappa kappa F) 2 (gammaD d) := by
let _ := hd
have hmeas :
MeasureTheory.AEStronglyMeasurable (evalPkappa kappa F) (gammaD d) :=
(continuous_evalPkappa_coeff_wip kappa F).stronglyMeasurable.aestronglyMeasurable
exact
(MeasureTheory.memLp_two_iff_integrable_sq_norm hmeas).2
(integrable_evalPkappa_sq_coeff_wip hd kappa F)
exact memLp_two_evalPkappa hd kappa F

private theorem evalPkappa_lpNorm_eq_norm_coeff_wip
{d : Nat} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) :
Expand Down Expand Up @@ -3034,4 +2890,25 @@ theorem lowAnnulusDefectControl
simp [lowAnnulusMass, hempty]
· exact finite_window_lowAnnulusDefectControl_core_wip hd kappa F hF_ne hF_norm J

/-- The Gaussian square-integral norm equals `lpNorm` for a measurable representative. -/
theorem gaussianL2Norm_eq_lpNorm_from_measurability
{d : Nat} {α : Type*} [NormedAddCommGroup α] (F : Cd d → α)
(hF : MeasureTheory.AEStronglyMeasurable F (gammaD d)) :
Real.sqrt (∫ z : Cd d, ‖F z‖ ^ (2 : ℝ) ∂ gammaD d) =
MeasureTheory.lpNorm F 2 (gammaD d) :=
gaussianL2Norm_eq_lpNorm_coeff_wip F hF

/-- The polynomial's Gaussian `lpNorm` is its coefficient norm. -/
theorem evalPkappa_lpNorm_eq_coefficient_norm
{d : Nat} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) :
MeasureTheory.lpNorm (evalPkappa kappa F) 2 (gammaD d) = ‖F‖ :=
evalPkappa_lpNorm_eq_norm_coeff_wip hd kappa F

/-- A unit reference polynomial bounds coefficient size through its modulus defect. -/
theorem norm_le_defect_add_two_of_norm_one
{d : Nat} (hd : 0 < d) (kappa : MultiIndex d)
(F G : Pkappa d kappa) (hF_norm : ‖F‖ = 1) :
‖G‖ ≤ defect F G + 2 :=
norm_le_defect_add_two_coeff_wip hd kappa F G hF_norm

end DimdPolyLEAN
Loading
Loading