diff --git a/LeanPool/PhaseRetrieval/Constant/Internal/HighFreqBandEstimate.lean b/LeanPool/PhaseRetrieval/Constant/Internal/HighFreqBandEstimate.lean index c6e35cf0ff..bbdc375bd5 100644 --- a/LeanPool/PhaseRetrieval/Constant/Internal/HighFreqBandEstimate.lean +++ b/LeanPool/PhaseRetrieval/Constant/Internal/HighFreqBandEstimate.lean @@ -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 -/ @@ -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 @@ -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) @@ -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] diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/CoefficientLimitRigidity.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/CoefficientLimitRigidity.lean index 48dc63eb78..13e522b6d2 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/CoefficientLimitRigidity.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/CoefficientLimitRigidity.lean @@ -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} @@ -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 : ℂ) : @@ -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) : @@ -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) : @@ -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 α] @@ -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) : @@ -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 diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/ExactModulusRecovery.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/ExactModulusRecovery.lean index 21e2baf37c..72c59a9060 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/ExactModulusRecovery.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/ExactModulusRecovery.lean @@ -184,6 +184,16 @@ theorem realHermiteGenerating_integral_mul_conj (u w : ℂ) : simp_rw [realHermiteGenerating_conj] exact realHermiteGenerating_integral_mul u (star w) +private theorem normalized_integral_cexp_quadratic (b c : ℂ) : + (((Real.pi ^ (-(1 / 4 : ℝ)) : ℝ) : ℂ) * + ((Real.pi ^ (-(1 / 4 : ℝ)) : ℝ) : ℂ)) * + (∫ t : ℝ, Complex.exp (-(1 : ℂ) * (t : ℂ) ^ 2 + b * (t : ℂ) + c)) = + Complex.exp (c + b ^ 2 / 4) := by + rw [integral_cexp_quadratic] + · simp only [neg_neg, div_one, mul_neg, mul_one, div_neg, sub_neg_eq_add] + rw [← mul_assoc, ← sq, ← neg_div, piPow_quarter_sq_mul_half, one_mul] + · norm_num + theorem realHermiteGenerating_stft_integral_raw (x ω : ℝ) (u v : ℂ) : (∫ t : ℝ, @@ -240,12 +250,7 @@ theorem realHermiteGenerating_stft_integral_raw ring simp_rw [hquad] rw [MeasureTheory.integral_const_mul] - rw [integral_cexp_quadratic] - · simp only [a, b, c] - ring_nf - rw [piPow_quarter_sq_mul_half] - ring_nf - · simp + exact normalized_integral_cexp_quadratic b c theorem realHermiteGenerating_integral_shift_mul_modulated_completed (u v : ℂ) (x ω : ℝ) : @@ -396,12 +401,7 @@ theorem realHermiteGenerating_ambiguity_integral_raw rw [← Complex.exp_add, ← Complex.exp_add] simp_rw [hquad] rw [MeasureTheory.integral_const_mul] - rw [integral_cexp_quadratic] - · simp only [a, b, c] - ring_nf - rw [piPow_quarter_sq_mul_half] - ring_nf - · simp + exact normalized_integral_cexp_quadratic b c theorem realHermiteGenerating_ambiguity_integral_linear_form (x ω : ℝ) (u v : ℂ) : @@ -2371,7 +2371,8 @@ private lemma ambiguity_kernel_iteratedDeriv_factor (n : ℕ) (x ω : ℝ) : Complex.ofReal (Real.exp (-((x ^ 2 + (2 * Real.pi) ^ 2 * ω ^ 2) / 4))) by funext u - simpa [inner, div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] + simpa only [inner, RCLike.re_to_real, star_trivial, Complex.ofReal_mul, one_mul, + div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using realHermiteGenerating_ambiguity_integral_independent_kernel x ω u w] rw [iteratedDeriv_mul_const_field] @@ -2862,7 +2863,8 @@ theorem realHermiteTensorRep_memLp_of_realHermite1D_memLp (fun y : Fin d -> ℝ => ∏ q : Fin d, ‖realHermite1D (alpha q) (y q)‖ ^ (2 : ℝ)) μpi := - MeasureTheory.Integrable.fintype_prod + MeasureTheory.Integrable.fin_nat_prod (E := fun _ : Fin d => ℝ) + (f := fun q : Fin d => fun t : ℝ => ‖realHermite1D (alpha q) t‖ ^ (2 : ℝ)) (μ := fun _ : Fin d => (volume : Measure ℝ)) hcoord exact hprod.congr (Filter.Eventually.of_forall fun y => by simpa [g, norm_prod] using @@ -3057,12 +3059,7 @@ private theorem skappa_ext_coeff_from_realHermite {d : Nat} {kappa : MultiIndex d} {U V : Skappa d kappa} (hcoeff : ∀ alpha, coeffSkappa U alpha = coeffSkappa V alpha) : U = V := by - cases U - cases V - simp only [coeffSkappa] at hcoeff - congr - funext alpha - exact hcoeff alpha + exact DimdPolyLEAN.skappa_ext_of_coeff_eq hcoeff theorem bKappa_injective_of_realHermite_coeff_recovery {d : Nat} (kappa : MultiIndex d) @@ -3101,33 +3098,9 @@ private theorem ambiguityRep_varphiKappa_eq_tensorRep_integral star (realHermiteTensorRep kappa (t - ((1 / 2 : ℝ) • ξ.1))) * Complex.exp (-(2 * Real.pi : ℂ) * Complex.I * ((inner ℝ ξ.2 t : ℝ) : ℂ)) := by - unfold ambiguityRep - apply MeasureTheory.integral_congr_ae - have hcoe := varphiKappa_coe_ae_eq_realHermiteTensorRep kappa - have hplus : - (fun t : RealVec d => - ((varphiKappa kappa : L2Real d) : RealVec d -> ℂ) - (t + ((1 / 2 : ℝ) • ξ.1))) - =ᵐ[(volume : Measure (RealVec d))] - fun t : RealVec d => - realHermiteTensorRep kappa (t + ((1 / 2 : ℝ) • ξ.1)) := by - exact - ((MeasureTheory.measurePreserving_add_right - (volume : Measure (RealVec d)) - (((1 / 2 : ℝ) • ξ.1))).quasiMeasurePreserving).ae_eq_comp hcoe - have hminus : - (fun t : RealVec d => - ((varphiKappa kappa : L2Real d) : RealVec d -> ℂ) - (t - ((1 / 2 : ℝ) • ξ.1))) - =ᵐ[(volume : Measure (RealVec d))] - fun t : RealVec d => - realHermiteTensorRep kappa (t - ((1 / 2 : ℝ) • ξ.1)) := by - exact - ((MeasureTheory.measurePreserving_add_right - (volume : Measure (RealVec d)) - (-((1 / 2 : ℝ) • ξ.1))).quasiMeasurePreserving).ae_eq_comp hcoe - filter_upwards [hplus, hminus] with t hplus_t hminus_t - rw [hplus_t, hminus_t] + exact ambiguityRep_eq_integral_of_ae_eq + (varphiKappa_coe_ae_eq_realHermiteTensorRep kappa) + (varphiKappa_coe_ae_eq_realHermiteTensorRep kappa) ξ /-- `TKappa`: T Kappa. -/ noncomputable def TKappa {d : Nat} : @@ -3202,7 +3175,8 @@ private theorem complexHermiteMvPolynomial_eval (hZstar : MvPolynomial.eval ev Zstar = star z) : MvPolynomial.eval ev (complexHermiteMvPolynomial m n Z Zstar) = complexHermite m n z := by - simp [complexHermiteMvPolynomial, complexHermite, hZ, hZstar, mul_assoc] + simp only [complexHermiteMvPolynomial, complexHermite, map_sum, map_mul, map_pow, + MvPolynomial.eval_C, hZ, hZstar, mul_assoc] private noncomputable def phi1DMvPolynomial {σ : Type*} (k n : Nat) (Z Zstar : MvPolynomial σ ℂ) : MvPolynomial σ ℂ := @@ -5665,7 +5639,7 @@ private lemma ae_prod_of_ae_ae_of_aestronglyMeasurable hF_meas.aemeasurable.measurable_mk (measurableSet_singleton (0 : E)) have hsections : ∀ᵐ x ∂μ, (fun y : β => F (x, y)) =ᵐ[ν] fun y => Fm (x, y) := - MeasureTheory.Measure.ae_ae_of_ae_prod hF_eq + MeasureTheory.Measure.ae_ae_eq_curry_of_prod (μ := μ) (ν := ν) hF_eq refine hF_eq.trans ((MeasureTheory.Measure.ae_prod_iff_ae_ae hmeas_zero).2 ?_) filter_upwards [hsec, hsections] with x hx hxm exact hxm.symm.trans hx @@ -5753,20 +5727,23 @@ theorem equalAmbiguity_to_rankOneKernel_ae star (g0 (p.2 - ((1 / 2 : ℝ) • p.1))) let endpointDiff : PhaseSpace d -> ℂ := fun p => f0 p.1 * star (f0 p.2) - g0 p.1 * star (g0 p.2) - have hf_mem : MemLp f0 2 μ := by simpa [f0, μ] using MeasureTheory.Lp.memLp f - have hg_mem : MemLp g0 2 μ := by simpa [g0, μ] using MeasureTheory.Lp.memLp g + have hAmb_pair : ∀ x ω : RealVec d, + ambiguityRep f f (x, ω) = ambiguityRep g g (x, ω) := by + simpa only [Prod.forall] using hAmb + have hf_mem : MemLp f0 2 μ := by exact MeasureTheory.Lp.memLp f + have hg_mem : MemLp g0 2 μ := by exact MeasureTheory.Lp.memLp g have hf_center : MemLp (fun p : PhaseSpace d => f0 (p.2 + ((1 / 2 : ℝ) • p.1)) * star (f0 (p.2 - ((1 / 2 : ℝ) • p.1)))) 2 (volume : Measure (PhaseSpace d)) := by - simpa [f0, μ] using centerKernel_memLp_two (d := d) hf_mem + exact centerKernel_memLp_two (d := d) hf_mem have hg_center : MemLp (fun p : PhaseSpace d => g0 (p.2 + ((1 / 2 : ℝ) • p.1)) * star (g0 (p.2 - ((1 / 2 : ℝ) • p.1)))) 2 (volume : Measure (PhaseSpace d)) := by - simpa [g0, μ] using centerKernel_memLp_two (d := d) hg_mem + exact centerKernel_memLp_two (d := d) hg_mem have hcenter_mem : MemLp centerDiff 2 (volume : Measure (PhaseSpace d)) := by refine MeasureTheory.MemLp.ae_eq ?_ (hf_center.sub hg_center) @@ -5775,7 +5752,7 @@ theorem equalAmbiguity_to_rankOneKernel_ae have hcenter_sections : ∀ᵐ x ∂μ, MemLp (fun t : RealVec d => centerDiff (x, t)) 2 μ := by - simpa [μ] using memLp_two_prod_right_ae (d := d) hcenter_mem + exact memLp_two_prod_right_ae (d := d) hcenter_mem have hcenter_zero_sections : ∀ᵐ x ∂μ, (fun t : RealVec d => centerDiff (x, t)) =ᵐ[μ] fun _ => (0 : ℂ) := by @@ -5808,12 +5785,9 @@ theorem equalAmbiguity_to_rankOneKernel_ae calc (𝓕 (fun t : RealVec d => centerDiff (x, t))) ω = ambiguityRep f f (x, ω) - ambiguityRep g g (x, ω) := by - simpa [centerDiff, f0, g0, μ] using - sectionDiff_fourier_eq_ambiguity_sub f g x ω - (by simpa [f0, μ] using hf_int) - (by simpa [g0, μ] using hg_int) + exact sectionDiff_fourier_eq_ambiguity_sub f g x ω hf_int hg_int _ = 0 := by - simp_all only [Prod.forall, one_div, RCLike.star_def, sub_self] + exact sub_eq_zero.mpr (hAmb_pair x ω) exact fourier_l1_l2_eq_zero_ae hdiff_int hx_l2 hfourier have hcenter_zero_prod : centerDiff =ᵐ[μ.prod μ] fun _ => (0 : ℂ) := by @@ -5851,11 +5825,11 @@ theorem equalAmbiguity_to_rankOneKernel_ae ring simp [endpointDiff, centerDiff, L, centerToEndpointsLinearEquiv, hplus, hminus] filter_upwards [hcomp] with p hp - simpa [hendpoint_eq] using hp - have hf_ae : f0 =ᵐ[μ] fRep := by simpa [f0, μ] using l2rep_ae_eq_coe hf_rep - have hg_ae : g0 =ᵐ[μ] gRep := by simpa [g0, μ] using l2rep_ae_eq_coe hg_rep + exact (congrFun hendpoint_eq p).trans hp + have hf_ae : f0 =ᵐ[μ] fRep := by exact l2rep_ae_eq_coe hf_rep + have hg_ae : g0 =ᵐ[μ] gRep := by exact l2rep_ae_eq_coe hg_rep have hendpoint_prod : - endpointDiff =ᵐ[μ.prod μ] fun _ => (0 : ℂ) := by simpa using hendpoint_zero + endpointDiff =ᵐ[μ.prod μ] fun _ => (0 : ℂ) := by exact hendpoint_zero have hf_fst : (fun p : PhaseSpace d => f0 p.1) =ᵐ[μ.prod μ] fun p => fRep p.1 := @@ -5880,7 +5854,8 @@ theorem equalAmbiguity_to_rankOneKernel_ae have h0 : f0 p.1 * star (f0 p.2) - g0 p.1 * star (g0 p.2) = 0 := hp have heq : f0 p.1 * star (f0 p.2) = g0 p.1 * star (g0 p.2) := sub_eq_zero.mp h0 - simp_all only [Prod.forall, one_div, RCLike.star_def] + exact (congrArg₂ (fun a b : ℂ => a * star b) hff hfs).symm.trans + (heq.trans (congrArg₂ (fun a b : ℂ => a * star b) hgf hgs)) simpa [μ, MeasureTheory.Measure.volume_eq_prod] using hrep_prod private lemma exists_eventually_and_ne_zero @@ -5902,6 +5877,72 @@ private lemma norm_eq_one_of_mul_star_eq_one {w : ℂ} have hw_nonneg : 0 ≤ ‖w‖ := norm_nonneg w nlinarith only [h', hw_nonneg] +private theorem rankOneKernel_phase_of_ae + {α : Type*} [MeasurableSpace α] {μ : Measure α} [SFinite μ] + {f g : α → ℂ} + (hkernel : (fun p : α × α => f p.1 * star (f p.2)) =ᵐ[μ.prod μ] + fun p => g p.1 * star (g p.2)) : + ((f =ᵐ[μ] fun _ => 0) ∧ (g =ᵐ[μ] fun _ => 0)) ∨ + ∃ w : ℂ, ‖w‖ = 1 ∧ g =ᵐ[μ] fun v => w * f v := by + have hrow_ae := MeasureTheory.Measure.ae_ae_of_ae_prod hkernel + by_cases hf_zero : f =ᵐ[μ] fun _ => (0 : ℂ) + · left + refine ⟨hf_zero, ?_⟩ + by_contra hg_ne + rcases exists_eventually_and_ne_zero (hrow_ae.and hf_zero) hg_ne with + ⟨u0, ⟨hrow_u0, hf0⟩, hg0_ne⟩ + apply hg_ne + filter_upwards [hrow_u0] with v hv + have hproduct : g u0 * star (g v) = 0 := by + simpa only [hf0, zero_mul] using hv.symm + exact star_eq_zero.mp ((mul_eq_zero.mp hproduct).resolve_left hg0_ne) + · right + rcases exists_eventually_and_ne_zero hrow_ae hf_zero with + ⟨u0, hrow_u0, hf0_ne⟩ + have hg0_ne : g u0 ≠ 0 := by + intro hg0 + apply hf_zero + filter_upwards [hrow_u0] with v hv + have hproduct : f u0 * star (f v) = 0 := by + simpa only [hg0, zero_mul] using hv + exact star_eq_zero.mp ((mul_eq_zero.mp hproduct).resolve_left hf0_ne) + let w : ℂ := star (f u0 / g u0) + have hphase : g =ᵐ[μ] fun v => w * f v := by + filter_upwards [hrow_u0] with v hv + have hstar : star (g v) = (f u0 / g u0) * star (f v) := by + calc + star (g v) = ((g u0)⁻¹ * g u0) * star (g v) := by + rw [inv_mul_cancel₀ hg0_ne, one_mul] + _ = (g u0)⁻¹ * (g u0 * star (g v)) := mul_assoc _ _ _ + _ = (g u0)⁻¹ * (f u0 * star (f v)) := congrArg ((g u0)⁻¹ * ·) hv.symm + _ = (f u0 / g u0) * star (f v) := by rw [div_eq_mul_inv]; ac_rfl + have hconj := congrArg star hstar + calc + g v = f v * star (f u0 / g u0) := by + simpa only [star_mul, star_star] using hconj + _ = w * f v := mul_comm _ _ + have hphase_fst : (fun p : α × α => g p.1) =ᵐ[μ.prod μ] fun p => w * f p.1 := + MeasureTheory.Measure.quasiMeasurePreserving_fst.ae hphase + have hphase_snd : (fun p : α × α => g p.2) =ᵐ[μ.prod μ] fun p => w * f p.2 := + MeasureTheory.Measure.quasiMeasurePreserving_snd.ae hphase + have hscale_prod : (fun p : α × α => f p.1 * star (f p.2)) =ᵐ[μ.prod μ] + fun p => (w * star w) * (f p.1 * star (f p.2)) := by + filter_upwards [hkernel, hphase_fst, hphase_snd] with p hp hp1 hp2 + calc + f p.1 * star (f p.2) = g p.1 * star (g p.2) := hp + _ = (w * f p.1) * star (w * f p.2) := by rw [hp1, hp2] + _ = (w * star w) * (f p.1 * star (f p.2)) := by rw [star_mul]; ac_rfl + have hscale_rows := MeasureTheory.Measure.ae_ae_of_ae_prod hscale_prod + rcases exists_eventually_and_ne_zero hscale_rows hf_zero with + ⟨u1, hscale_u1, hu1_ne⟩ + rcases exists_eventually_and_ne_zero hscale_u1 hf_zero with + ⟨v1, hscale_u1v1, hv1_ne⟩ + have hF_ne : f u1 * star (f v1) ≠ 0 := mul_ne_zero hu1_ne (star_ne_zero.mpr hv1_ne) + have hunit_mul : w * star w = 1 := + mul_right_cancel₀ hF_ne (by simpa only [one_mul] using hscale_u1v1.symm) + exact ⟨w, norm_eq_one_of_mul_star_eq_one hunit_mul, hphase⟩ + + -- Retain the original generated declarations when replacing broad simplification. private theorem rankOneKernel_ae_to_unimodular_phase._simp_1_1.{u_2} {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero (2 : α)] : @@ -5941,101 +5982,15 @@ theorem rankOneKernel_ae_to_unimodular_phase =ᵐ[(MeasureTheory.volume : MeasureTheory.Measure (RealVec d × RealVec d))] fun p => gRep p.1 * star (gRep p.2)) : (f = 0 ∧ g = 0) ∨ ∃ w : ℂ, ‖w‖ = 1 ∧ g = w • f := by - let μ : MeasureTheory.Measure (RealVec d) := MeasureTheory.volume have hkernel_prod : (fun p : RealVec d × RealVec d => fRep p.1 * star (fRep p.2)) - =ᵐ[μ.prod μ] fun p => gRep p.1 * star (gRep p.2) := by - simpa only [μ, MeasureTheory.Measure.volume_eq_prod (RealVec d) (RealVec d)] - using hkernel - have hrow_ae : - ∀ᵐ u ∂μ, ∀ᵐ v ∂μ, - fRep u * star (fRep v) = gRep u * star (gRep v) := by - exact MeasureTheory.Measure.ae_ae_of_ae_prod hkernel_prod - by_cases hf_zero : f = 0 - · left - refine ⟨hf_zero, ?_⟩ - by_contra hg_ne - have hfRep_zero : fRep =ᵐ[μ] fun _ => (0 : ℂ) := - rep_ae_eq_zero_of_L2_eq_zero hf_rep hf_zero - have hgRep_not_zero : ¬ gRep =ᵐ[μ] fun _ => (0 : ℂ) := by - intro hzero - exact hg_ne (L2_eq_zero_of_rep_ae_eq_zero hg_rep hzero) - have hgood : ∀ᵐ u ∂μ, - (∀ᵐ v ∂μ, fRep u * star (fRep v) = gRep u * star (gRep v)) ∧ - fRep u = 0 := hrow_ae.and hfRep_zero - rcases exists_eventually_and_ne_zero hgood hgRep_not_zero with - ⟨u0, hgood_u0, hg0_ne⟩ - rcases hgood_u0 with ⟨hrow_u0, hf0⟩ - have hgRep_zero : gRep =ᵐ[μ] fun _ => (0 : ℂ) := by - filter_upwards [hrow_u0] with v hv - have hproduct : gRep u0 * star (gRep v) = 0 := by - simpa only [hf0, zero_mul] using hv.symm - exact star_eq_zero.mp ((mul_eq_zero.mp hproduct).resolve_left hg0_ne) - exact hg_ne (L2_eq_zero_of_rep_ae_eq_zero hg_rep hgRep_zero) - · right - have hfRep_not_zero : ¬ fRep =ᵐ[μ] fun _ => (0 : ℂ) := by - intro hzero - exact hf_zero (L2_eq_zero_of_rep_ae_eq_zero hf_rep hzero) - rcases exists_eventually_and_ne_zero hrow_ae hfRep_not_zero with - ⟨u0, hrow_u0, hf0_ne⟩ - have hg0_ne : gRep u0 ≠ 0 := by - by_contra hg0 - apply hfRep_not_zero - filter_upwards [hrow_u0] with v hv - have hproduct : fRep u0 * star (fRep v) = 0 := by - simpa only [hg0, zero_mul] using hv - exact star_eq_zero.mp ((mul_eq_zero.mp hproduct).resolve_left hf0_ne) - let w : ℂ := star (fRep u0 / gRep u0) - have hphase : gRep =ᵐ[μ] fun v => w * fRep v := by - filter_upwards [hrow_u0] with v hv - have hstar : - star (gRep v) = (fRep u0 / gRep u0) * star (fRep v) := by - calc - star (gRep v) = - ((gRep u0)⁻¹ * gRep u0) * star (gRep v) := by rw [inv_mul_cancel₀ hg0_ne, one_mul] - _ = (gRep u0)⁻¹ * (gRep u0 * star (gRep v)) := by ring - _ = (gRep u0)⁻¹ * (fRep u0 * star (fRep v)) := by rw [← hv] - _ = (fRep u0 / gRep u0) * star (fRep v) := by rw [div_eq_mul_inv]; ac_rfl - have hconj := congrArg star hstar - calc - gRep v = fRep v * star (fRep u0 / gRep u0) := by - simpa only [star_mul, star_star] using hconj - _ = w * fRep v := by ring - have hL2 : g = w • f := - ae_unimodular_phase_to_L2_eq hf_rep hg_rep hphase - have hphase_fst : - (fun p : RealVec d × RealVec d => gRep p.1) - =ᵐ[μ.prod μ] fun p => w * fRep p.1 := - MeasureTheory.Measure.quasiMeasurePreserving_fst.ae hphase - have hphase_snd : - (fun p : RealVec d × RealVec d => gRep p.2) - =ᵐ[μ.prod μ] fun p => w * fRep p.2 := - MeasureTheory.Measure.quasiMeasurePreserving_snd.ae hphase - have hscale_prod : - (fun p : RealVec d × RealVec d => fRep p.1 * star (fRep p.2)) - =ᵐ[μ.prod μ] - fun p => (w * star w) * (fRep p.1 * star (fRep p.2)) := by - filter_upwards [hkernel_prod, hphase_fst, hphase_snd] with p hp hp1 hp2 - calc - fRep p.1 * star (fRep p.2) = gRep p.1 * star (gRep p.2) := hp - _ = (w * fRep p.1) * star (w * fRep p.2) := by rw [hp1, hp2] - _ = (w * star w) * (fRep p.1 * star (fRep p.2)) := by - rw [star_mul] - ring - have hscale_rows : - ∀ᵐ u ∂μ, ∀ᵐ v ∂μ, - fRep u * star (fRep v) = - (w * star w) * (fRep u * star (fRep v)) := by - exact MeasureTheory.Measure.ae_ae_of_ae_prod hscale_prod - rcases exists_eventually_and_ne_zero hscale_rows hfRep_not_zero with - ⟨u1, hscale_u1, hu1_ne⟩ - rcases exists_eventually_and_ne_zero hscale_u1 hfRep_not_zero with - ⟨v1, hscale_u1v1, hv1_ne⟩ - have hF_ne : fRep u1 * star (fRep v1) ≠ 0 := - mul_ne_zero hu1_ne (star_ne_zero.mpr hv1_ne) - have hunit_mul : w * star w = 1 := by - exact mul_right_cancel₀ hF_ne (by simpa only [one_mul] using hscale_u1v1.symm) - exact ⟨w, norm_eq_one_of_mul_star_eq_one hunit_mul, hL2⟩ + =ᵐ[(volume : Measure (RealVec d)).prod volume] + fun p => gRep p.1 * star (gRep p.2) := by + simpa only [MeasureTheory.Measure.volume_eq_prod (RealVec d) (RealVec d)] using hkernel + rcases rankOneKernel_phase_of_ae hkernel_prod with hzero | ⟨w, hw, hphase⟩ + · exact Or.inl ⟨L2_eq_zero_of_rep_ae_eq_zero hf_rep hzero.1, + L2_eq_zero_of_rep_ae_eq_zero hg_rep hzero.2⟩ + · exact Or.inr ⟨w, hw, ae_unimodular_phase_to_L2_eq hf_rep hg_rep hphase⟩ theorem rankOneRecoveryFromAmbiguity {d : Nat} {f g : L2Real d} {fRep gRep : RealVec d -> ℂ} @@ -6155,12 +6110,7 @@ private theorem skappa_ext_coeff_exact_wip {d : Nat} {kappa : MultiIndex d} {U V : Skappa d kappa} (hcoeff : ∀ alpha, coeffSkappa U alpha = coeffSkappa V alpha) : U = V := by - cases U - cases V - simp only [coeffSkappa] at hcoeff - congr - funext alpha - exact hcoeff alpha + exact DimdPolyLEAN.skappa_ext_of_coeff_eq hcoeff private theorem bKappa_zero_exact_wip {d : Nat} (kappa : MultiIndex d) : diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/FiniteBaseAnnulusEstimate.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/FiniteBaseAnnulusEstimate.lean index 24e048e7a2..634de196a3 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/FiniteBaseAnnulusEstimate.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/FiniteBaseAnnulusEstimate.lean @@ -79,15 +79,12 @@ private theorem toFun_ofPkappa_annulus private lemma continuous_Phi_annulus {d : Nat} (kappa alpha : MultiIndex d) : Continuous (Phi kappa alpha) := by - unfold Phi phi1D complexHermite - continuity + exact DimdPolyLEAN.continuous_Phi kappa alpha private lemma continuous_evalPkappa_annulus {d : Nat} (kappa : MultiIndex d) (F : Pkappa d kappa) : Continuous (evalPkappa kappa F) := by - unfold evalPkappa - exact continuous_finsetSum _ fun alpha _ => - continuous_const.mul (continuous_Phi_annulus kappa alpha) + exact DimdPolyLEAN.continuous_evalPkappa kappa F private lemma measurableSet_productAnnulus_annulus {d : Nat} (j : Idx d) : @@ -421,21 +418,7 @@ private theorem norm_ne_zero_of_ne_zero_pkappa_annulus private theorem integrable_evalPkappa_sq_annulus {d : Nat} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) : Integrable (fun z : Cd d => ‖evalPkappa kappa F z‖ ^ 2) (gammaD d) := by - by_cases hF : F = 0 - · subst hF - simp [evalPkappa] - · have hmeas : - AEStronglyMeasurable (fun z : Cd d => ‖evalPkappa kappa F z‖ ^ 2) (gammaD d) := - ((continuous_evalPkappa_annulus 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_annulus hF - simp_all + exact DimdPolyLEAN.integrable_evalPkappa_sq hd kappa F private theorem evalPkappa_add_apply_annulus {d : Nat} (kappa : MultiIndex d) @@ -1373,28 +1356,7 @@ private theorem Phi_rotate_one_exp_annulus Phi kappa alpha (Function.update z q0 (Complex.exp (Complex.I * t) * z q0)) = Complex.exp (Complex.I * (((alpha q0 : ℤ) - (kappa q0 : ℤ) : ℂ) * t)) * Phi kappa alpha z := by - classical - rw [Phi_eq_PhiKappaAlpha_annulus, Phi_eq_PhiKappaAlpha_annulus] - unfold Hermite1DimdLEAN.PhiKappaAlpha - have hupdate : - (fun q : Fin d => - Hermite1DimdLEAN.oneDimPhi (kappa q) (alpha q) - (Function.update z q0 (Complex.exp (Complex.I * t) * z q0) q)) = - Function.update - (fun q : Fin d => Hermite1DimdLEAN.oneDimPhi (kappa q) (alpha q) (z q)) - q0 - (Hermite1DimdLEAN.oneDimPhi (kappa q0) (alpha q0) - (Complex.exp (Complex.I * t) * z q0)) := by - funext q - by_cases hq : q = q0 - · simp_all - · simp [Function.update, hq] - rw [hupdate, - Finset.prod_update_of_mem (s := Finset.univ) (i := q0) (by simp), - oneDimPhi_phaseLaw_annulus] - conv_rhs => - rw [Finset.prod_eq_mul_prod_sdiff_singleton_of_mem (s := Finset.univ) (i := q0) (by simp)] - ring_nf + exact DimdPolyLEAN.Phi_rotate_one_exp kappa alpha q0 t z private lemma fourier_mk_eq_exp_annulus (n : ℤ) (θ : ℝ) : @@ -1413,27 +1375,7 @@ private theorem Phi_rotateCoord_circle_phase_annulus (Function.update z q0 ((fourier (1 : Int) x : ℂ) * z q0)) = (fourier ((alpha q0 : Nat) : Int) x : ℂ) * Phi kappa alpha z := by - induction x using Quotient.inductionOn with - | h θ => - rw [fourier_mk_eq_exp_annulus ((kappa q0 : Nat) : Int) θ, - fourier_mk_eq_exp_annulus ((alpha q0 : Nat) : Int) θ, - fourier_mk_eq_exp_annulus (1 : Int) θ] - have hone : - Complex.exp (Complex.I * ((1 : ℤ) : ℂ) * θ) = - Complex.exp (Complex.I * θ) := by - simp_all - rw [hone, Phi_rotate_one_exp_annulus] - have hphase : - Complex.exp (Complex.I * (((kappa q0 : Nat) : Int) : ℂ) * θ) * - (Complex.exp (Complex.I * (((alpha q0 : ℤ) - (kappa q0 : ℤ) : ℂ) * θ)) * - Phi kappa alpha z) = - Complex.exp (Complex.I * (((alpha q0 : Nat) : Int) : ℂ) * θ) * - Phi kappa alpha z := by - rw [← mul_assoc, ← Complex.exp_add] - congr 1 - push_cast - ring_nf - exact hphase + exact DimdPolyLEAN.Phi_rotateCoord_circle_phase kappa alpha q0 x z private def fiberIndexLow {d : Nat} (q0 : Fin d) (D : Nat) (alpha : Idx d) : Fin (D + 1) := @@ -1475,29 +1417,7 @@ private theorem evalPkappa_rotateCoord_circle_phase_sum_annulus (Function.update z q0 ((fourier (1 : Int) x : ℂ) * z q0)) = ∑ alpha ∈ F.support, F alpha * Phi kappa alpha z * circleChar (alpha q0) x := by - classical - unfold evalPkappa - rw [Finsupp.sum, Finset.mul_sum] - refine Finset.sum_congr rfl ?_ - intro alpha halpha - have hphase := - Phi_rotateCoord_circle_phase_annulus - (kappa := kappa) (alpha := alpha) (q0 := q0) x z - have hchar : circleChar (alpha q0) x = (fourier ((alpha q0 : Nat) : Int) x : ℂ) := - circleChar_eq_fourier_nat (alpha q0) x - calc - (fourier ((kappa q0 : Nat) : Int) x : ℂ) * - (F alpha * - Phi kappa alpha - (Function.update z q0 ((fourier (1 : Int) x : ℂ) * z q0))) - = F alpha * - ((fourier ((kappa q0 : Nat) : Int) x : ℂ) * - Phi kappa alpha - (Function.update z q0 ((fourier (1 : Int) x : ℂ) * z q0))) := by ring - _ = F alpha * ((fourier ((alpha q0 : Nat) : Int) x : ℂ) * Phi kappa alpha z) := by rw [hphase] - _ = F alpha * Phi kappa alpha z * circleChar (alpha q0) x := by - rw [hchar] - ring + exact DimdPolyLEAN.evalPkappa_rotateCoord_circle_phase_sum kappa q0 F x z private theorem lowPoly_fiberCoeffLow_eq_sum_annulus {d : Nat} {kappa : MultiIndex d} diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/FiniteBaseCircleEstimate.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/FiniteBaseCircleEstimate.lean index 730f477780..bb5cfef133 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/FiniteBaseCircleEstimate.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/FiniteBaseCircleEstimate.lean @@ -1438,70 +1438,25 @@ private theorem carrierBase_mem {N : Nat} (k : Fin N) : private theorem carrierArc_length_pos_wip {N : Nat} (k : Fin N) : 0 < arcLength (carrierArc N k) := by - rw [carrierArc_length k] - have hNnat : 0 < N := Nat.lt_of_le_of_lt (Nat.zero_le k.1) k.2 - have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hNnat - positivity + exact DimdPolyLEAN.carrierArc_length_pos k private theorem carrierArc_left_nonneg_wip {N : Nat} (k : Fin N) : 0 <= (carrierArc N k).left := by - unfold carrierArc - positivity + exact DimdPolyLEAN.carrierArc_left_nonneg k private theorem carrierArc_right_le_period_wip {N : Nat} (k : Fin N) : (carrierArc N k).right <= 2 * Real.pi := by - unfold carrierArc - have hNnat : 0 < N := Nat.lt_of_le_of_lt (Nat.zero_le k.1) k.2 - have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hNnat - have hle : ((k.1 + 1 : Nat) : ℝ) <= (N : ℝ) := by exact_mod_cast k.2 - have hT_nonneg : 0 <= (2 * Real.pi : ℝ) := by positivity - calc - (2 * Real.pi) * ((k.1 + 1 : Nat) : ℝ) / (N : ℝ) - <= (2 * Real.pi) * (N : ℝ) / (N : ℝ) := div_le_div_of_nonneg_right - (mul_le_mul_of_nonneg_left hle hT_nonneg) (le_of_lt hNpos) - _ = 2 * Real.pi := by field_simp [ne_of_gt hNpos] + exact DimdPolyLEAN.carrierArc_right_le_period k private theorem carrierArc_left_lt_right_wip {N : Nat} (k : Fin N) : (carrierArc N k).left < (carrierArc N k).right := by - have hlen := carrierArc_length_pos_wip k - dsimp [arcLength] at hlen - linarith only [hlen] + exact DimdPolyLEAN.carrierArc_left_lt_right k private theorem carrierArc_arcSet_eq_mk_image_Icc_wip {N : Nat} (k : Fin N) : arcSet (carrierArc N k) = QuotientAddGroup.mk '' Set.Icc ((carrierArc N k).left) ((carrierArc N k).right) := by - ext x - constructor - · intro hx - rcases hx with ⟨t, ht, rfl⟩ - refine ⟨(carrierArc N k).left + t * arcLength (carrierArc N k), ?_, rfl⟩ - have hlen_nonneg : 0 <= arcLength (carrierArc N k) := - le_of_lt (carrierArc_length_pos_wip k) - constructor - · dsimp [arcLength] at hlen_nonneg ⊢ - nlinarith only [ht.1, hlen_nonneg] - · dsimp [arcLength] at hlen_nonneg ⊢ - nlinarith only [ht.2, hlen_nonneg] - · intro hx - rcases hx with ⟨y, hy, rfl⟩ - let t : ℝ := (y - (carrierArc N k).left) / arcLength (carrierArc N k) - refine ⟨t, ?_, ?_⟩ - · have hlen_pos : 0 < arcLength (carrierArc N k) := - carrierArc_length_pos_wip k - constructor - · dsimp [t] - exact div_nonneg (sub_nonneg.mpr hy.1) (le_of_lt hlen_pos) - · dsimp [t] - rw [div_le_one hlen_pos] - dsimp [arcLength] - linarith only [hy.2] - · dsimp [arcParam, t] - have hlen_pos : 0 < arcLength (carrierArc N k) := - carrierArc_length_pos_wip k - apply congrArg (fun r : ℝ => (QuotientAddGroup.mk r : Circle)) - field_simp [ne_of_gt hlen_pos] - ring + exact DimdPolyLEAN.carrierArc_arcSet_eq_mk_image_Icc k private theorem circle_dist_mk_le_abs_sub (a b : ℝ) : dist ((QuotientAddGroup.mk a : Circle)) (QuotientAddGroup.mk b) <= |a - b| := by @@ -1617,23 +1572,7 @@ private theorem carrierArc_arcSet_eq_mk_image_Ioc_union_left_wip (QuotientAddGroup.mk '' Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right)) ∪ {(QuotientAddGroup.mk ((carrierArc N k).left) : Circle)} := by - rw [carrierArc_arcSet_eq_mk_image_Icc_wip k] - have hIcc : - Set.Icc ((carrierArc N k).left) ((carrierArc N k).right) = - Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right) ∪ - {((carrierArc N k).left)} := by - ext y - constructor - · intro hy - by_cases hleft : y = (carrierArc N k).left - · exact Or.inr hleft - · exact Or.inl ⟨lt_of_le_of_ne hy.1 (Ne.symm hleft), hy.2⟩ - · intro hy - rcases hy with hy | hy - · exact ⟨le_of_lt hy.1, hy.2⟩ - · rw [Set.mem_singleton_iff.mp hy] - exact ⟨le_rfl, le_of_lt (carrierArc_left_lt_right_wip k)⟩ - rw [hIcc, Set.image_union, Set.image_singleton] + exact DimdPolyLEAN.carrierArc_arcSet_eq_mk_image_Ioc_union_left k private theorem quotient_mk_injOn_Ioc_zero_period_wip : Set.InjOn (fun t : ℝ => (QuotientAddGroup.mk t : Circle)) @@ -1658,21 +1597,7 @@ private theorem carrierArc_mk_preimage_image_Ioc_inter_fundamental_wip Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right)) ∩ Set.Ioc (0 : ℝ) (2 * Real.pi)) = Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right) := by - ext x - constructor - · intro hx - rcases hx.1 with ⟨y, hy, hyx⟩ - have hy_fund : y ∈ Set.Ioc (0 : ℝ) (2 * Real.pi) := by - exact ⟨lt_of_le_of_lt (carrierArc_left_nonneg_wip k) hy.1, - le_trans hy.2 (carrierArc_right_le_period_wip k)⟩ - have hxy : y = x := - quotient_mk_injOn_Ioc_zero_period_wip hy_fund hx.2 hyx - rwa [← hxy] - · intro hx - constructor - · exact ⟨x, hx, rfl⟩ - · exact ⟨lt_of_le_of_lt (carrierArc_left_nonneg_wip k) hx.1, - le_trans hx.2 (carrierArc_right_le_period_wip k)⟩ + exact DimdPolyLEAN.carrierArc_mk_preimage_image_Ioc_inter_fundamental k private theorem volume_singleton_circle_wip (x : Circle) : MeasureTheory.volume ({x} : Set Circle) = 0 := by @@ -1695,81 +1620,21 @@ private theorem carrierArc_arcSet_ae_eq_mk_image_Ioc_wip {N : Nat} (k : Fin N) : arcSet (carrierArc N k) =ᵐ[μCircle] QuotientAddGroup.mk '' Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right) := by - rw [carrierArc_arcSet_eq_mk_image_Ioc_union_left_wip k] - let A : Set Circle := - QuotientAddGroup.mk '' - Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right) - let e : Circle := QuotientAddGroup.mk ((carrierArc N k).left) - change (Set.union A ({e} : Set Circle)) =ᵐ[μCircle] A - rw [MeasureTheory.ae_eq_set] - constructor - · refine MeasureTheory.measure_mono_null (μ := μCircle) (t := {e}) ?_ - (μCircle_singleton_wip e) - intro x hx - rcases hx.1 with hxIoc | hxleft - · exact False.elim (hx.2 hxIoc) - · exact hxleft - · refine MeasureTheory.measure_mono_null (μ := μCircle) (t := (∅ : Set Circle)) ?_ ?_ - · intro x hx - exact False.elim (hx.2 (Or.inl hx.1)) - · simp + exact DimdPolyLEAN.carrierArc_arcSet_ae_eq_mk_image_Ioc k private theorem carrierArc_arcSet_ae_eq_mk_image_Ioc_volume_wip {N : Nat} (k : Fin N) : arcSet (carrierArc N k) =ᵐ[(MeasureTheory.volume : MeasureTheory.Measure Circle)] QuotientAddGroup.mk '' Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right) := by - rw [carrierArc_arcSet_eq_mk_image_Ioc_union_left_wip k] - let A : Set Circle := - QuotientAddGroup.mk '' - Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right) - let e : Circle := QuotientAddGroup.mk ((carrierArc N k).left) - change (Set.union A ({e} : Set Circle)) =ᵐ[(MeasureTheory.volume : MeasureTheory.Measure - Circle)] A - rw [MeasureTheory.ae_eq_set] - constructor - · refine MeasureTheory.measure_mono_null - (μ := (MeasureTheory.volume : MeasureTheory.Measure Circle)) (t := {e}) ?_ - (volume_singleton_circle_wip e) - intro x hx - rcases hx.1 with hxIoc | hxleft - · exact False.elim (hx.2 hxIoc) - · exact hxleft - · refine MeasureTheory.measure_mono_null - (μ := (MeasureTheory.volume : MeasureTheory.Measure Circle)) (t := (∅ : Set Circle)) ?_ ?_ - · intro x hx - exact False.elim (hx.2 (Or.inl hx.1)) - · simp + exact DimdPolyLEAN.carrierArc_arcSet_ae_eq_mk_image_Ioc_volume k private theorem volume_mk_image_carrierArc_Ioc_wip {N : Nat} (k : Fin N) : MeasureTheory.volume ((fun t : ℝ => (QuotientAddGroup.mk t : Circle)) '' Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right)) = ENNReal.ofReal (arcLength (carrierArc N k)) := by - let S : Set Circle := - (fun t : ℝ => (QuotientAddGroup.mk t : Circle)) '' - Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right) - have hS_null : - MeasureTheory.NullMeasurableSet S - (MeasureTheory.volume : MeasureTheory.Measure Circle) := by - exact (measurableSet_arcSet (carrierArc N k)).nullMeasurableSet.congr - (carrierArc_arcSet_ae_eq_mk_image_Ioc_volume_wip k) - have hpre := - (AddCircle.measurePreserving_mk (T := 2 * Real.pi) (t := 0)).measure_preimage hS_null - rw [MeasureTheory.Measure.restrict_apply' measurableSet_Ioc] at hpre - change MeasureTheory.volume - (((fun t : ℝ => (QuotientAddGroup.mk t : Circle)) ⁻¹' S) ∩ - Set.Ioc (0 : ℝ) (0 + 2 * Real.pi)) = - MeasureTheory.volume S at hpre - have hpre_set : - ((fun t : ℝ => (QuotientAddGroup.mk t : Circle)) ⁻¹' S) ∩ - Set.Ioc (0 : ℝ) (0 + 2 * Real.pi) = - Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right) := by - simpa only [zero_add, S] using carrierArc_mk_preimage_image_Ioc_inter_fundamental_wip k - rw [hpre_set, Real.volume_Ioc] at hpre - dsimp [arcLength] - symm - rw [← hpre] + exact DimdPolyLEAN.volume_mk_image_carrierArc_Ioc k private theorem period_smul_μCircle_mk_image_carrierArc_Ioc_wip {N : Nat} (k : Fin N) : @@ -1778,22 +1643,13 @@ private theorem period_smul_μCircle_mk_image_carrierArc_Ioc_wip ((fun t : ℝ => (QuotientAddGroup.mk t : Circle)) '' Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right)) = ENNReal.ofReal (arcLength (carrierArc N k)) := by - let S : Set Circle := - (fun t : ℝ => (QuotientAddGroup.mk t : Circle)) '' - Set.Ioc ((carrierArc N k).left) ((carrierArc N k).right) - have hmeasure := congrArg (fun μ : MeasureTheory.Measure Circle => μ S) - (AddCircle.volume_eq_smul_haarAddCircle (T := 2 * Real.pi)) - change MeasureTheory.volume S = - ENNReal.ofReal (2 * Real.pi) * μCircle S at hmeasure - rw [← hmeasure] - exact volume_mk_image_carrierArc_Ioc_wip k + exact DimdPolyLEAN.period_smul_μCircle_mk_image_carrierArc_Ioc k private theorem period_smul_μCircle_carrierArc_wip {N : Nat} (k : Fin N) : ENNReal.ofReal (2 * Real.pi) * μCircle (arcSet (carrierArc N k)) = ENNReal.ofReal (arcLength (carrierArc N k)) := by - rw [MeasureTheory.measure_congr (carrierArc_arcSet_ae_eq_mk_image_Ioc_wip k)] - exact period_smul_μCircle_mk_image_carrierArc_Ioc_wip k + exact DimdPolyLEAN.period_smul_μCircle_carrierArc k private theorem carrierArc_mu_real_eq_length_div_period {N : Nat} (k : Fin N) : @@ -3600,97 +3456,25 @@ private theorem parseval_fin_fourier {L : Nat} (c : Fin L -> ℂ) : circleL2Sq (fun t : Circle => ∑ m : Fin L, c m * fourier (m.val : ℤ) t) = ∑ m : Fin L, ‖c m‖ ^ 2 := by - let E := Finset.range L - let b' : Nat -> ℂ := fun n => - if h : n < L then c ⟨n, h⟩ else 0 - have h_func_eq : - (fun t : Circle => - ∑ m : Fin L, c m * fourier (↑↑m : ℤ) t) = - fun t => ∑ n ∈ E, b' n * fourier (↑n : ℤ) t := by - ext t - simp only [E] - rw [Finset.sum_fin_eq_sum_range] - refine Finset.sum_congr rfl fun n hn => ?_ - simp [b', Finset.mem_range.mp hn] - rw [h_func_eq] - let Pcont : C(Circle, ℂ) := - ∑ n ∈ E, b' n • fourier (n : ℤ) - let PLp := - (ContinuousMap.toLp (α := Circle) 2 AddCircle.haarAddCircle ℂ) Pcont - let E' := - E.map ⟨(Nat.cast : Nat -> ℤ), Nat.cast_injective⟩ - let d : ℤ -> ℂ := fun k => b' (Int.toNat k) - have hPLp : PLp = ∑ k ∈ E', d k • fourierLp 2 k := by - simp only [PLp, Pcont, E', d, fourierLp, map_sum, map_smul] - simp_all only [fourier_apply, natCast_zsmul, Finset.sum_map, Function.Embedding.coeFn_mk, - Int.toNat_natCast] - have hinner_orth : - @inner ℂ _ _ PLp PLp = - Complex.ofReal (∑ n ∈ E, ‖b' n‖ ^ 2) := by - rw [hPLp, orthonormal_fourier.inner_sum d d E', - show E' = E.map ⟨(Nat.cast : Nat -> ℤ), Nat.cast_injective⟩ from rfl, - Finset.sum_map, Complex.ofReal_sum] - congr 1 - ext n - simp only [Function.Embedding.coeFn_mk, d, Int.toNat_natCast] - rw [mul_comm, Complex.mul_conj] - congr 1 - exact (Complex.sq_norm (b' n)).symm - have hcombine := - (MeasureTheory.L2.inner_def (𝕜 := ℂ) PLp PLp).symm.trans hinner_orth - have hae := ContinuousMap.coeFn_toLp - (μ := AddCircle.haarAddCircle) (𝕜 := ℂ) (p := 2) Pcont - have hPcont_eq : - ∀ t : Circle, (Pcont : Circle -> ℂ) t = - ∑ n ∈ E, b' n * (fourier (n : ℤ)) t := by - intro t - simp [Pcont, ContinuousMap.coe_sum, ContinuousMap.coe_smul, smul_eq_mul] - have h_sum_eq : - ∑ n ∈ E, ‖b' n‖ ^ 2 = ∑ m : Fin L, ‖c m‖ ^ 2 := by - simp only [E] - rw [Finset.sum_fin_eq_sum_range] - refine Finset.sum_congr rfl fun n hn => ?_ - simp [b', Finset.mem_range.mp hn] - calc - circleL2Sq (fun t => ∑ n ∈ E, b' n * (fourier (↑n : ℤ)) t) - = ∫ t : Circle, ‖(↑↑PLp : Circle -> ℂ) t‖ ^ 2 - ∂ AddCircle.haarAddCircle := by - unfold circleL2Sq - symm - apply MeasureTheory.integral_congr_ae - filter_upwards [hae] with t ht - rw [show (↑↑PLp : Circle -> ℂ) t = Pcont t from ht, hPcont_eq t] - _ = (∫ t : Circle, - @inner ℂ ℂ _ - ((↑↑PLp : Circle -> ℂ) t) - ((↑↑PLp : Circle -> ℂ) t) - ∂ AddCircle.haarAddCircle).re := by - have hint := MeasureTheory.L2.integrable_inner (𝕜 := ℂ) PLp PLp - symm - calc - _ = Complex.reCLM (∫ t, - @inner ℂ ℂ _ - ((↑↑PLp : Circle -> ℂ) t) - ((↑↑PLp : Circle -> ℂ) t) - ∂ AddCircle.haarAddCircle) := rfl - _ = ∫ t, Complex.reCLM - (@inner ℂ ℂ _ - ((↑↑PLp : Circle -> ℂ) t) - ((↑↑PLp : Circle -> ℂ) t)) - ∂ AddCircle.haarAddCircle := (ContinuousLinearMap.integral_comp_comm _ hint).symm - _ = _ := by - congr 1 - ext t - exact @inner_self_eq_norm_sq ℂ ℂ _ _ _ - ((↑↑PLp : Circle -> ℂ) t) - _ = ∑ m : Fin L, ‖c m‖ ^ 2 := by - rw [show (∫ t : Circle, - @inner ℂ ℂ _ - ((↑↑PLp : Circle -> ℂ) t) - ((↑↑PLp : Circle -> ℂ) t) - ∂ AddCircle.haarAddCircle) = - Complex.ofReal (∑ n ∈ E, ‖b' n‖ ^ 2) - from hcombine, Complex.ofReal_re, h_sum_eq] + let P : C(Circle, ℂ) := ∑ m : Fin L, c m • fourier (m.val : ℤ) + let f := ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ P + have horth := (orthonormal_fourier (T := 2 * Real.pi)).comp (fun m : Fin L => (m.val : ℤ)) + (Nat.cast_injective.comp Fin.val_injective) + have hnorm : ‖f‖ ^ 2 = ∑ m : Fin L, ‖c m‖ ^ 2 := by + simpa only [f, P, map_sum, map_smul, Function.comp_apply, fourierLp, + LinearIsometry.toSpanSingleton_apply] using + horth.orthogonalFamily.norm_sum c Finset.univ + have hinner := congrArg RCLike.re (@MeasureTheory.L2.inner_def Circle ℂ ℂ _ _ _ _ _ f f) + rw [← integral_re (MeasureTheory.L2.integrable_inner f f)] at hinner + simp only [← norm_sq_eq_re_inner] at hinner + refine Eq.trans ?_ hnorm + rw [hinner] + apply MeasureTheory.integral_congr_ae + filter_upwards [ContinuousMap.coeFn_toLp (p := 2) + (μ := AddCircle.haarAddCircle) (𝕜 := ℂ) P] with t ht + rw [ht] + congr 1 + simp only [P, ContinuousMap.sum_apply, ContinuousMap.smul_apply, smul_eq_mul] private theorem circleL2Sq_slowBandPoly {L : Nat} (p : Fin L -> ℂ) : circleL2Sq (slowBandPoly p) = ∑ m : Fin L, ‖p m‖ ^ 2 := by diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermite1Dimd/ImportedAnalyticInputs.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermite1Dimd/ImportedAnalyticInputs.lean index 9a2069e751..3e375457dd 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermite1Dimd/ImportedAnalyticInputs.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermite1Dimd/ImportedAnalyticInputs.lean @@ -948,7 +948,7 @@ theorem oneVariableAngularFactorization simp only [Finset.mem_range, Nat.lt_add_one_iff, le_min_iff] at hj obtain ⟨hjk, hjn⟩ := hj rw [hstar_z, mul_pow, mul_pow] - simpa [mul_assoc, mul_left_comm, mul_comm] using + simpa only [mul_assoc, mul_left_comm, mul_comm] using oneVariableAngularFactorization_termwise r t k n j hjk hjn have hsum' : Finset.sum (Finset.range (min k n + 1)) @@ -968,7 +968,7 @@ theorem oneVariableAngularFactorization ((r : ℂ) ^ (n + k - j * 2) * ((↑(Real.sqrt (Nat.factorial k : ℝ)))⁻¹ * (↑(Real.sqrt (Nat.factorial n : ℝ)))⁻¹))))) := by - simpa [mul_assoc, mul_left_comm, mul_comm] using hsum + simpa only [mul_assoc, mul_left_comm, mul_comm] using hsum rw [hsum'] congr 1 simp [radial, Polynomial.eval₂_finsetSum, Polynomial.eval₂_monomial, diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/BasisLocalization.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/BasisLocalization.lean index c0514030d2..d75c37e511 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/BasisLocalization.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/BasisLocalization.lean @@ -1126,7 +1126,7 @@ private theorem phi0AnnulusIntegrand_le_shell r ^ (2 * k + 1) * Real.exp (-r ^ 2) ≤ (((j + 1 : ℕ) : ℝ) ^ (2 * k + 1)) * Real.exp (-(j : ℝ) ^ 2) := by gcongr - simpa [mul_assoc, mul_left_comm, mul_comm] using + simpa only [mul_assoc] using (mul_le_mul_of_nonneg_left hprod hcoeff_nonneg) private theorem annulusIntegralSq_phi0_shell_bound diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/ImportedAnalyticInputs.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/ImportedAnalyticInputs.lean index 3304b3422d..c461cf3dd8 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/ImportedAnalyticInputs.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/ImportedAnalyticInputs.lean @@ -69,8 +69,7 @@ theorem phase_normalized_orthogonal_reduction ∀ h : H, ∀ a : ℝ, defect (h - (a : ℂ) • f0) ≤ |a| + defect h) : ∃ δ Mloc : ℝ, 0 < δ ∧ 0 < Mloc ∧ ∀ h : H, ‖h‖ ≤ δ → (inner ℂ h f0).im = 0 → ‖h‖ ≤ Mloc * defect h := by - exact - HermiteLEAN.phase_normalized_orthogonal_reduction - defect hdefect_nonneg f0 hf0 C hC horth hscalar hcompare + exact HermiteLEAN.phase_normalized_orthogonal_reduction + defect hdefect_nonneg f0 hf0 C hC horth hscalar hcompare end HermitekLEAN diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean index 7f0234cfeb..81ed3b6e0d 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean @@ -862,7 +862,8 @@ private lemma alternating_vandermonde_coeff_poly (k s N : ℕ) : ∑ j ∈ Finset.range (k + 1), (((((-1 : ℤ) ^ j * ↑(k.choose j)) : ℤ) • (A ^ (k + s - j))).coeff N) = (A ^ s * Polynomial.X ^ k).coeff N := by - simpa using congrArg (fun p : Polynomial ℤ => p.coeff N) hpoly + simpa only [Polynomial.finsetSum_coeff] using + congrArg (fun p : Polynomial ℤ => p.coeff N) hpoly have hsum : ∑ j ∈ Finset.range (k + 1), (-1 : ℤ) ^ j * ↑(k.choose j) * ↑((k + s - j).choose N) = (A ^ s * Polynomial.X ^ k).coeff N := by @@ -870,23 +871,15 @@ private lemma alternating_vandermonde_coeff_poly (k s N : ℕ) : apply Finset.sum_congr rfl intro j hj rw [zsmul_eq_mul] - simp only [A, Polynomial.C_1, Polynomial.coeff_intCast_mul, + simp only [A, Polynomial.C_1, Polynomial.coeff_intCast_mul, Int.cast_id, Polynomial.coeff_one_add_X_pow] - simp_all - simpa [A] using hsum + exact hsum private lemma alternating_vandermonde_coeff (k s N : ℕ) : ∑ j ∈ Finset.range (k + 1), (-1 : ℤ) ^ j * ↑(k.choose j) * ↑((k + s - j).choose N) = if k ≤ N then ↑(s.choose (N - k)) else 0 := by - calc - ∑ j ∈ Finset.range (k + 1), (-1 : ℤ) ^ j * ↑(k.choose j) * ↑((k + s - j).choose N) = - ((((Polynomial.C (1 : ℤ)) + Polynomial.X) ^ s * Polynomial.X ^ k).coeff N) := - alternating_vandermonde_coeff_poly k s N - _ = if k ≤ N then (((Polynomial.C (1 : ℤ)) + Polynomial.X) ^ s).coeff (N - k) else 0 := by - exact - (Polynomial.coeff_mul_X_pow' (((Polynomial.C (1 : ℤ)) + Polynomial.X) ^ s) k N) - _ = if k ≤ N then ↑(s.choose (N - k)) else 0 := by - by_cases h : k ≤ N <;> simp [h, Polynomial.coeff_one_add_X_pow] + rw [alternating_vandermonde_coeff_poly, Polynomial.coeff_mul_X_pow'] + simp only [Polynomial.C_1, Polynomial.coeff_one_add_X_pow] private theorem alternating_vandermonde_zero (k s : ℕ) : ∑ j ∈ Finset.range (k + 1), (-1 : ℤ) ^ j * ↑(k.choose j) * @@ -3299,7 +3292,7 @@ private lemma continuous_truncCirclePoly (k J : ℕ) (r : ℝ) (G : ℂ → ℂ) classical refine continuous_finsetSum _ ?_ intro n hn - continuity + exact continuous_const.mul (map_continuous (fourier (n : ℤ))) private lemma summable_circleSeries_terms {k : ℕ} {G : ℂ → ℂ} (hG : G ∈ Hk k) {r : ℝ} (hr : 0 < r) (t : Circle) : @@ -3454,6 +3447,58 @@ private theorem circleSeries_l2_identity_canonical : simpa [mul_comm, mul_left_comm, mul_assoc] using hsum_tendsto' exact hlimit_eq +private theorem norm_toLp_sq (F : C(Circle, ℂ)) : + ‖ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ F‖ ^ 2 = circleL2Sq F := by + let f := ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ F + have h := congrArg RCLike.re (@MeasureTheory.L2.inner_def Circle ℂ ℂ _ _ _ _ _ f f) + rw [← integral_re] at h + · simp only [← norm_sq_eq_re_inner] at h + refine h.trans ?_ + apply integral_congr_ae + filter_upwards [ContinuousMap.coeFn_toLp (p := 2) + (μ := AddCircle.haarAddCircle) (𝕜 := ℂ) F] with t ht + exact congrArg (fun z : ℂ => ‖z‖ ^ 2) ht + · exact MeasureTheory.L2.integrable_inner f f + +private theorem summable_circle_continuous (c : ℕ → ℂ) (hc : Summable (fun n => ‖c n‖)) : + Summable (fun n : ℕ => c n • fourier (T := T) (n : ℤ)) := by + apply Summable.of_norm + simpa only [norm_smul, fourier_norm, mul_one] using hc + +private theorem circleL2Sq_tendsto_partial_fourier_sums + (c : ℕ → ℂ) (hc : Summable (fun n => ‖c n‖)) : + Filter.Tendsto + (fun J : ℕ => circleL2Sq (fun t : Circle => + ∑ n : Fin (J + 1), c n.1 * fourier (n.1 : ℤ) t)) + Filter.atTop (nhds (circleL2Sq (fun t : Circle => ∑' n : ℕ, c n * fourier (n : ℤ) t))) := by + let F : ℕ → C(Circle, ℂ) := fun n => c n • fourier (n : ℤ) + have hF : Summable F := summable_circle_continuous c hc + have hpartial : Filter.Tendsto (fun J => ∑ n ∈ Finset.range (J + 1), F n) + Filter.atTop (nhds (∑' n, F n)) := + hF.hasSum.tendsto_sum_nat.comp (Filter.tendsto_add_atTop_nat 1) + have hLp := ((ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ).continuous.tendsto + (∑' n, F n)).comp hpartial + have hnorm := hLp.norm.pow 2 + simp only [Function.comp_apply, norm_toLp_sq] at hnorm + have hvalue : (fun t : Circle => (∑' n, F n) t) = + (fun t : Circle => ∑' n : ℕ, c n * fourier (n : ℤ) t) := by + funext t + exact ((ContinuousMap.evalCLM ℂ t).hasSum hF.hasSum).tsum_eq.symm + rw [show circleL2Sq ((∑' n, F n : C(Circle, ℂ)) : Circle → ℂ) = + circleL2Sq (fun t : Circle => ∑' n : ℕ, c n * fourier (n : ℤ) t) from + congrArg circleL2Sq hvalue] at hnorm + convert hnorm using 1 + ext J + apply congrArg circleL2Sq + funext t + simp only [F, ContinuousMap.sum_apply, ContinuousMap.smul_apply, smul_eq_mul, Finset.sum_range] + +-- Preserve the private arithmetic helper generated by the previous proof. +private theorem circleSeries_l2_identity._proof_1_3 (b n : ℕ) + (hn : @LE.le ℕ Nat.instPreorder.toLE b n) + (h : ¬ @LE.le ℕ Nat.instPreorder.toLE b (n + 1)) : False := + h (Nat.le_succ_of_le hn) + /-- Compatibility statement: circle Parseval identity for an `H_k` expansion. -/ theorem circleSeries_l2_identity : ∀ {k : ℕ} {G : ℂ → ℂ} {g : ℕ → ℂ}, @@ -3507,97 +3552,16 @@ theorem circleSeries_l2_identity : intro x hx have hx' : (x : ℕ) < J + 1 := x.isLt simp [aJ, hx'] - have hcontPoly : - ∀ J, Continuous (finiteCirclePoly k r (fun n : Fin (J + 1) => g n.1)) := by - intro J - rw [hpoly_eq J] - refine continuous_finsetSum _ ?_ - intro n hn - continuity - let M : ℝ := ∑' n : ℕ, ‖c n‖ - have hM_nonneg : 0 ≤ M := tsum_nonneg fun n => norm_nonneg _ - have hbound : - ∀ J : ℕ, ∀ᵐ t : Circle ∂AddCircle.haarAddCircle, - ‖‖finiteCirclePoly k r (fun n : Fin (J + 1) => g n.1) t‖ ^ 2‖ ≤ (fun _ : Circle => M ^ 2) - t := by - intro J - refine Filter.Eventually.of_forall ?_ - intro t - have hpartial_le : - ‖finiteCirclePoly k r (fun n : Fin (J + 1) => g n.1) t‖ ≤ M := by - rw [hpoly_eq J] - calc - ‖∑ n : Fin (J + 1), g n.1 * (qkn k n.1 r : ℂ) * fourier (n.1 : ℤ) t‖ - ≤ ∑ n : Fin (J + 1), ‖g n.1 * (qkn k n.1 r : ℂ) * fourier (n.1 : ℤ) t‖ := - norm_sum_le _ _ - _ = ∑ n : Fin (J + 1), ‖c n.1‖ := by - refine Finset.sum_congr rfl ?_ - intro n hn - calc - ‖g n.1 * (qkn k n.1 r : ℂ) * fourier (n.1 : ℤ) t‖ = ‖c n.1‖ * ‖fourier (n.1 : ℤ) - t‖ := by simp [c, mul_assoc] - _ = ‖c n.1‖ := by - simp only [fourier_apply, Circle.norm_coe, mul_one] - _ = ∑ n ∈ Finset.range (J + 1), ‖c n‖ := by rw [Finset.sum_range] - _ ≤ M := by exact hc_norm.sum_le_tsum _ (fun n hn => norm_nonneg _) - have hnonneg : 0 ≤ ‖finiteCirclePoly k r (fun n : Fin (J + 1) => g n.1) t‖ ^ 2 := sq_nonneg _ - have habs : - ‖‖finiteCirclePoly k r (fun n : Fin (J + 1) => g n.1) t‖ ^ 2‖ = - ‖finiteCirclePoly k r (fun n : Fin (J + 1) => g n.1) t‖ ^ 2 := by - rw [Real.norm_of_nonneg hnonneg] - rw [habs] - have hsq_le : ‖finiteCirclePoly k r (fun n : Fin (J + 1) => g n.1) t‖ ^ 2 ≤ M ^ 2 := by - have hmul := mul_le_mul hpartial_le hpartial_le (norm_nonneg _) hM_nonneg - simpa [pow_two] using hmul - simpa using hsq_le - have hlim : - ∀ᵐ t : Circle ∂AddCircle.haarAddCircle, - Filter.Tendsto - (fun J => ‖finiteCirclePoly k r (fun n : Fin (J + 1) => g n.1) t‖ ^ 2) - Filter.atTop - (nhds (‖circleSeries k g r t‖ ^ 2)) := by - refine Filter.Eventually.of_forall ?_ - intro t - let a : ℕ → ℂ := fun n => g n * (qkn k n r : ℂ) * fourier (n : ℤ) t - have hs : Summable a := by - refine Summable.of_norm_bounded (g := fun n => ‖c n‖) hc_norm ?_ - intro n - have haeq : ‖a n‖ = ‖c n‖ := by - calc - ‖a n‖ = ‖c n‖ * ‖fourier (n : ℤ) t‖ := by simp [a, c, mul_assoc] - _ = ‖c n‖ := by - simp only [fourier_apply, Circle.norm_coe, mul_one] - exact haeq.le - have hconv : - Filter.Tendsto (fun J => ∑ n ∈ Finset.range J, a n) Filter.atTop (nhds (circleSeries k g r - t)) := by simpa [circleSeries, a] using hs.hasSum.tendsto_sum_nat - have hEqFun : - (fun J => finiteCirclePoly k r (fun n : Fin (J + 1) => g n.1) t) = - (fun J => ∑ n ∈ Finset.range (J + 1), a n) := by - ext J - simpa [a, Finset.sum_range] using congrFun (hpoly_eq J) t - have hconv' : - Filter.Tendsto - (fun J => finiteCirclePoly k r (fun n : Fin (J + 1) => g n.1) t) - Filter.atTop - (nhds (circleSeries k g r t)) := by - rw [hEqFun] - exact hconv.comp (Filter.tendsto_atTop_atTop.mpr (fun b => ⟨b, fun n hn => by omega⟩)) - exact (hconv'.norm.pow 2) - have hIntTendsto := - MeasureTheory.tendsto_integral_of_dominated_convergence - (μ := AddCircle.haarAddCircle) - (fun _ : Circle => M ^ 2) - (fun J => ((hcontPoly J).norm.pow 2).aestronglyMeasurable) - (MeasureTheory.integrable_const (M ^ 2)) - hbound hlim have hCircleTendsto : Filter.Tendsto (fun J => circleL2Sq (finiteCirclePoly k r (fun n : Fin (J + 1) => g n.1))) Filter.atTop (nhds (circleL2Sq (circleSeries k g r))) := by - simp only [circleL2Sq] - exact hIntTendsto + change Filter.Tendsto _ Filter.atTop + (nhds (circleL2Sq (fun t : Circle => ∑' n : ℕ, + g n * (qkn k n r : ℂ) * fourier (n : ℤ) t))) + simpa only [hpoly_eq, c] using + circleL2Sq_tendsto_partial_fourier_sums c hc_norm let d : ℕ → ℝ := fun n => |qkn k n r| ^ 2 * ‖g n‖ ^ 2 have hd : Summable d := by refine hc_sq.congr ?_ @@ -4921,4 +4885,9 @@ theorem modulusDefect_le_norm (F0 G : ℂ → ℂ) (z : ℂ) : rw [add_sub_cancel_left] at h exact h +/-- The squared Hermite basis values are summable at every point. -/ +theorem summable_norm_sq_Phi_eval (k : ℕ) (z : ℂ) : + Summable (fun n : ℕ => ‖Phi k n z‖ ^ 2) := + summable_sq_Phi_eval k z + end HermitekLEAN diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/ImportedAnalyticInputs.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/ImportedAnalyticInputs.lean index 69528a6cf6..c254613e57 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/ImportedAnalyticInputs.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/ImportedAnalyticInputs.lean @@ -1420,7 +1420,9 @@ private theorem stftRep_schwartz_eq_fourier_apply {d : Nat} (h.coeFn_toLp 2 (MeasureTheory.volume : MeasureTheory.Measure (RealVec d))) filter_upwards [hf_ae, hh_ae] with t hft hht rw [hft, hht] - simp [Real.fourierChar_apply, Circle.smul_def, real_inner_comm, mul_assoc, mul_comm] + simp only [Real.fourierChar_apply, Circle.smul_def, stftSliceSchwartz_apply, + Complex.ofReal_neg, Complex.ofReal_mul, Complex.ofReal_ofNat, smul_eq_mul, + real_inner_comm, mul_neg, neg_mul, mul_assoc, mul_comm] private theorem integral_fourier_sq_phase_schwartz_realVec {d : Nat} (f : SchwartzMap (RealVec d) ℂ) (x : RealVec d) : @@ -1593,6 +1595,34 @@ private theorem integrable_stftRep_sq_slice_schwartz_realVec {d : Nat} simp_rw [stftRep_schwartz_eq_fourier_apply h f x] exact h_fourier +/-- The ambiguity integral may use any almost-everywhere equal representatives. -/ +theorem ambiguityRep_eq_integral_of_ae_eq + {d : ℕ} {f g : L2Real d} {F G : RealVec d → ℂ} + (hf : (f : RealVec d → ℂ) =ᵐ[volume] F) + (hg : (g : RealVec d → ℂ) =ᵐ[volume] G) (ξ : PhaseSpace d) : + ambiguityRep f g ξ = ∫ t : RealVec d, + F (t + (1 / 2 : ℝ) • ξ.1) * star (G (t - (1 / 2 : ℝ) • ξ.1)) * + modulationPhase ξ.2 t := by + have hplus := ((measurePreserving_add_right volume + ((1 / 2 : ℝ) • ξ.1)).quasiMeasurePreserving).ae_eq_comp hf + have hminus : (fun t : RealVec d => (g : RealVec d → ℂ) + (t - (1 / 2 : ℝ) • ξ.1)) =ᵐ[volume] + fun t => G (t - (1 / 2 : ℝ) • ξ.1) := by + simpa only [sub_eq_add_neg, Function.comp_def] using + ((measurePreserving_add_right volume + (-((1 / 2 : ℝ) • ξ.1))).quasiMeasurePreserving).ae_eq_comp hg + apply integral_congr_ae + filter_upwards [hplus, hminus] with t htF htG + exact congrArg (fun a : ℂ => a * modulationPhase ξ.2 t) + (congrArg₂ (fun a b : ℂ => a * star b) htF htG) + +private theorem ambiguityRep_schwartz_eq_integral {d : ℕ} + (f g : SchwartzMap (RealVec d) ℂ) (ξ : PhaseSpace d) : + ambiguityRep (f.toLp 2 volume) (g.toLp 2 volume) ξ = ∫ t : RealVec d, + f (t + (1 / 2 : ℝ) • ξ.1) * star (g (t - (1 / 2 : ℝ) • ξ.1)) * + modulationPhase ξ.2 t := + ambiguityRep_eq_integral_of_ae_eq (f.coeFn_toLp 2 volume) (g.coeFn_toLp 2 volume) ξ + private theorem integral_signal_autocorr_phase_schwartz_realVec {d : Nat} (f : SchwartzMap (RealVec d) ℂ) (x ω : RealVec d) : ∫ t, star (f t) * f (t + x) * modulationPhase ω (t + (1 / 2 : ℝ) • x) = @@ -1615,27 +1645,8 @@ private theorem integral_signal_autocorr_phase_schwartz_realVec {d : Nat} ac_rfl _ = _ := integral_add_right_eq_self (μ := μ) (f := fun t : RealVec d => f (t + a) * star (f (t - a)) * modulationPhase ω t) a - unfold ambiguityRep - rw [hshift] - have hf_ae : - (f.toLp 2 μ : RealVec d -> ℂ) =ᵐ[μ] f := - f.coeFn_toLp 2 μ - have hplus : - (fun t : RealVec d => (f.toLp 2 μ : RealVec d -> ℂ) (t + a)) =ᵐ[μ] - fun t : RealVec d => f (t + a) := by - simpa only [Function.comp_def] using - ((MeasureTheory.measurePreserving_add_right μ a).quasiMeasurePreserving).ae_eq_comp - hf_ae - have hminus : - (fun t : RealVec d => (f.toLp 2 μ : RealVec d -> ℂ) (t - a)) =ᵐ[μ] - fun t : RealVec d => f (t - a) := by - simpa only [sub_eq_add_neg, Function.comp_def] using - ((MeasureTheory.measurePreserving_add_right μ (-a)).quasiMeasurePreserving).ae_eq_comp - hf_ae - apply integral_congr_ae - filter_upwards [hplus, hminus] with t hplus_t hminus_t - rw [hplus_t, hminus_t] - simp [modulationPhase] + rw [ambiguityRep_schwartz_eq_integral] + exact hshift private theorem signal_autocorr_integrable_schwartz_realVec {d : Nat} (f : SchwartzMap (RealVec d) ℂ) (x : RealVec d) : @@ -1657,7 +1668,7 @@ private theorem window_autocorr_integrable_schwartz_realVec {d : Nat} (MeasureTheory.volume : MeasureTheory.Measure (RealVec d)) := by let μ : MeasureTheory.Measure (RealVec d) := MeasureTheory.volume have hneg : MemLp (fun y : RealVec d => h (-y)) 2 μ := by - simpa [μ] using reflected_memLp_schwartz_realVec h + exact reflected_memLp_schwartz_realVec h have hleft' : MemLp (fun y : RealVec d => h (-(y - t))) 2 μ := by simpa only [neg_sub, Function.comp_def, μ] using hneg.comp_measurePreserving (MeasureTheory.measurePreserving_sub_right μ t) @@ -1736,77 +1747,12 @@ private theorem ambiguityRep_neg_neg_schwartz_realVec {d : Nat} star (ambiguityRep (f.toLp 2 (MeasureTheory.volume : MeasureTheory.Measure (RealVec d))) (f.toLp 2 (MeasureTheory.volume : MeasureTheory.Measure (RealVec d))) (x, ω)) := by - let μ : MeasureTheory.Measure (RealVec d) := MeasureTheory.volume - let a : RealVec d := (1 / 2 : ℝ) • x - have hneg_half : (1 / 2 : ℝ) • (-x) = -a := by simp [a] - unfold ambiguityRep - have hf_ae : - (f.toLp 2 μ : RealVec d -> ℂ) =ᵐ[μ] f := - f.coeFn_toLp 2 μ - have hleft_plus : - (fun t : RealVec d => - (f.toLp 2 μ : RealVec d -> ℂ) (t + (1 / 2 : ℝ) • (-x))) - =ᵐ[μ] fun t : RealVec d => f (t - a) := by - have h := - ((MeasureTheory.measurePreserving_add_right μ (-a)).quasiMeasurePreserving).ae_eq_comp - hf_ae - filter_upwards [h] with t ht - rw [hneg_half] - simpa only [sub_eq_add_neg, Function.comp_apply, Function.comp_def] using ht - have hleft_minus : - (fun t : RealVec d => - (f.toLp 2 μ : RealVec d -> ℂ) (t - (1 / 2 : ℝ) • (-x))) - =ᵐ[μ] fun t : RealVec d => f (t + a) := by - have h := - ((MeasureTheory.measurePreserving_add_right μ a).quasiMeasurePreserving).ae_eq_comp - hf_ae - filter_upwards [h] with t ht - rw [hneg_half] - simpa only [sub_eq_add_neg, neg_neg, Function.comp_apply, Function.comp_def] using ht - have hright_plus : - (fun t : RealVec d => (f.toLp 2 μ : RealVec d -> ℂ) (t + a)) =ᵐ[μ] - fun t : RealVec d => f (t + a) := by - simpa only [Function.comp_def] using - ((MeasureTheory.measurePreserving_add_right μ a).quasiMeasurePreserving).ae_eq_comp - hf_ae - have hright_minus : - (fun t : RealVec d => (f.toLp 2 μ : RealVec d -> ℂ) (t - a)) =ᵐ[μ] - fun t : RealVec d => f (t - a) := by - simpa only [sub_eq_add_neg, Function.comp_def] using - ((MeasureTheory.measurePreserving_add_right μ (-a)).quasiMeasurePreserving).ae_eq_comp - hf_ae - calc - ∫ t : RealVec d, - (f.toLp 2 μ : RealVec d -> ℂ) (t + (1 / 2 : ℝ) • (-x)) * - star ((f.toLp 2 μ : RealVec d -> ℂ) (t - (1 / 2 : ℝ) • (-x))) * - Complex.exp (-(2 * Real.pi : ℂ) * Complex.I * ↑(inner ℝ (-ω) t)) - = ∫ t : RealVec d, f (t - a) * star (f (t + a)) * - modulationPhase (-ω) t := by - apply integral_congr_ae - filter_upwards [hleft_plus, hleft_minus] with t ht1 ht2 - rw [ht1, ht2] - simp [modulationPhase] - _ = star (∫ t : RealVec d, f (t + a) * star (f (t - a)) * - modulationPhase ω t) := by - calc - ∫ t : RealVec d, f (t - a) * star (f (t + a)) * - modulationPhase (-ω) t = - ∫ t : RealVec d, star (f (t + a) * star (f (t - a)) * - modulationPhase ω t) := by - apply integral_congr_ae - filter_upwards with t - simp [star_mul, star_modulationPhase, mul_comm] - _ = star (∫ t : RealVec d, f (t + a) * star (f (t - a)) * - modulationPhase ω t) := integral_conj - _ = star (∫ t : RealVec d, - (f.toLp 2 μ : RealVec d -> ℂ) (t + (1 / 2 : ℝ) • x) * - star ((f.toLp 2 μ : RealVec d -> ℂ) (t - (1 / 2 : ℝ) • x)) * - Complex.exp (-(2 * Real.pi : ℂ) * Complex.I * ↑(inner ℝ ω t))) := by - congr 1 - apply integral_congr_ae - filter_upwards [hright_plus, hright_minus] with t ht1 ht2 - rw [ht1, ht2] - simp [modulationPhase, a] + rw [ambiguityRep_schwartz_eq_integral, ambiguityRep_schwartz_eq_integral] + refine Eq.trans ?_ integral_conj + apply integral_congr_ae + filter_upwards with t + simp only [← Complex.star_def, smul_neg, sub_eq_add_neg, neg_neg, star_mul, star_star, + star_modulationPhase, mul_comm] private theorem integral_window_autocorr_phase_schwartz_realVec {d : Nat} (h : SchwartzMap (RealVec d) ℂ) (t x ω : RealVec d) : @@ -1902,33 +1848,8 @@ private theorem integral_window_autocorr_phase_schwartz_realVec {d : Nat} have hamb : ∫ y : RealVec d, h (y - a) * star (h (y + a)) * modulationPhase (-ω) y = ambiguityRep (h.toLp 2 μ) (h.toLp 2 μ) (-x, -ω) := by - unfold ambiguityRep - have hh_ae : (h.toLp 2 μ : RealVec d -> ℂ) =ᵐ[μ] h := h.coeFn_toLp 2 μ - have hplus : - (fun y : RealVec d => - (h.toLp 2 μ : RealVec d -> ℂ) (y + (1 / 2 : ℝ) • (-x))) - =ᵐ[μ] fun y : RealVec d => h (y - a) := by - have hq := - ((MeasureTheory.measurePreserving_add_right μ (-a)).quasiMeasurePreserving).ae_eq_comp - hh_ae - filter_upwards [hq] with y hy - rw [hneg_half] - simpa only [sub_eq_add_neg, Function.comp_apply, Function.comp_def] using hy - have hminus : - (fun y : RealVec d => - (h.toLp 2 μ : RealVec d -> ℂ) (y - (1 / 2 : ℝ) • (-x))) - =ᵐ[μ] fun y : RealVec d => h (y + a) := by - have hq := - ((MeasureTheory.measurePreserving_add_right μ a).quasiMeasurePreserving).ae_eq_comp - hh_ae - filter_upwards [hq] with y hy - rw [hneg_half] - simpa only [sub_eq_add_neg, neg_neg, Function.comp_apply, Function.comp_def] using hy - symm - apply integral_congr_ae - filter_upwards [hplus, hminus] with y hy1 hy2 - rw [hy1, hy2] - simp [modulationPhase] + rw [ambiguityRep_schwartz_eq_integral] + simp only [hneg_half, sub_eq_add_neg, neg_neg] calc ∫ y : RealVec d, h (t - y) * star (h (t + x - y)) * modulationPhase ω y = modulationPhase ω t * @@ -2345,20 +2266,23 @@ private theorem norm_stftRep_sub_le {d : Nat} (MeasureTheory.volume : MeasureTheory.Measure (RealVec d)) 2 2) let T : L2Real d → L2Real d := fun h => modulateL2 ξ.2 (star (translateL2 (-ξ.1) h)) - have hT_norm : ‖T h₁‖ = ‖h₁‖ := by simp [T, norm_modulateL2, norm_star_L2, norm_translateL2] + have hT_norm : ‖T h₁‖ = ‖h₁‖ := + (norm_modulateL2 ξ.2 _).trans ((norm_star_L2 _).trans (norm_translateL2 (-ξ.1) h₁)) have hT_sub_norm : ‖T h₁ - T h₂‖ = ‖h₁ - h₂‖ := by calc ‖T h₁ - T h₂‖ = dist (T h₁) (T h₂) := by rw [dist_eq_norm] _ = dist (star (translateL2 (-ξ.1) h₁)) (star (translateL2 (-ξ.1) h₂)) := by - simp [T, dist_modulateL2] + exact dist_modulateL2 ξ.2 _ _ _ = dist (translateL2 (-ξ.1) h₁) (translateL2 (-ξ.1) h₂) := by rw [dist_star_L2] _ = dist h₁ h₂ := by rw [dist_translateL2] _ = ‖h₁ - h₂‖ := by rw [dist_eq_norm] - rw [stftRep_eq_lpPairing h₁ f₁ ξ, stftRep_eq_lpPairing h₂ f₂ ξ] - change ‖P f₁ (T h₁) - P f₂ (T h₂)‖ ≤ - ‖f₁ - f₂‖ * ‖h₁‖ + ‖f₂‖ * ‖h₁ - h₂‖ - simpa only [hT_norm, hT_sub_norm] using - norm_bilinear_sub_le P (fun f g => lpPairing_mul_norm_le f g) f₁ f₂ (T h₁) (T h₂) + calc + ‖stftRep h₁ f₁ ξ - stftRep h₂ f₂ ξ‖ = ‖P f₁ (T h₁) - P f₂ (T h₂)‖ := + congrArg norm (congrArg₂ (fun a b : ℂ => a - b) + (stftRep_eq_lpPairing h₁ f₁ ξ) (stftRep_eq_lpPairing h₂ f₂ ξ)) + _ ≤ ‖f₁ - f₂‖ * ‖h₁‖ + ‖f₂‖ * ‖h₁ - h₂‖ := by + simpa only [hT_norm, hT_sub_norm] using + norm_bilinear_sub_le P (fun f g => lpPairing_mul_norm_le f g) f₁ f₂ (T h₁) (T h₂) theorem continuous_stftRep {d : Nat} (h f : L2Real d) : @@ -2812,13 +2736,17 @@ private theorem stftRep_sub_eq_add {d : Nat} modulateL2 ξ.2 (star (translateL2 (-ξ.1) h)) have hT_sub : T (h₁ - h₂) = T h₁ - T h₂ := by simp [T, translateL2_sub, star_L2_sub, modulateL2_sub] - rw [stftRep_eq_lpPairing h₁ f₁ ξ, stftRep_eq_lpPairing h₂ f₂ ξ, - stftRep_eq_lpPairing h₁ (f₁ - f₂) ξ, - stftRep_eq_lpPairing (h₁ - h₂) f₂ ξ] - change P f₁ (T h₁) - P f₂ (T h₂) = - P (f₁ - f₂) (T h₁) + P f₂ (T (h₁ - h₂)) - rw [hT_sub] - exact bilinear_sub P f₁ f₂ (T h₁) (T h₂) + calc + stftRep h₁ f₁ ξ - stftRep h₂ f₂ ξ = P f₁ (T h₁) - P f₂ (T h₂) := + congrArg₂ (fun a b : ℂ => a - b) + (stftRep_eq_lpPairing h₁ f₁ ξ) (stftRep_eq_lpPairing h₂ f₂ ξ) + _ = P (f₁ - f₂) (T h₁) + P f₂ (T h₁ - T h₂) := + bilinear_sub P f₁ f₂ (T h₁) (T h₂) + _ = stftRep h₁ (f₁ - f₂) ξ + stftRep (h₁ - h₂) f₂ ξ := + congrArg₂ (fun a b : ℂ => a + b) + (stftRep_eq_lpPairing h₁ (f₁ - f₂) ξ).symm + ((congrArg (P f₂) hT_sub.symm).trans + (stftRep_eq_lpPairing (h₁ - h₂) f₂ ξ).symm) private theorem lpNorm_stftRep_sub_le {d : Nat} (h₁ h₂ f₁ f₂ : L2Real d) : @@ -2842,10 +2770,8 @@ private theorem lpNorm_stftRep_sub_le {d : Nat} _ ≤ MeasureTheory.lpNorm (stftRep h₁ (f₁ - f₂)) 2 μP + MeasureTheory.lpNorm (stftRep (h₁ - h₂) f₂) 2 μP := MeasureTheory.lpNorm_add_le hmem₁ (by norm_num) - _ ≤ ‖f₁ - f₂‖ * ‖h₁‖ + ‖f₂‖ * ‖h₁ - h₂‖ := by - gcongr - · exact lpNorm_stftRep_le h₁ (f₁ - f₂) - · exact lpNorm_stftRep_le (h₁ - h₂) f₂ + _ ≤ ‖f₁ - f₂‖ * ‖h₁‖ + ‖f₂‖ * ‖h₁ - h₂‖ := + add_le_add (lpNorm_stftRep_le h₁ (f₁ - f₂)) (lpNorm_stftRep_le (h₁ - h₂) f₂) -- This convergence proof has a large phase-space `lpNorm` expression; the algebra is direct, -- but normalization exceeds the default heartbeat budget. @@ -2886,7 +2812,8 @@ private theorem lpNorm_mul_le_real (eLpNorm f 2 μ).toReal * (eLpNorm g 2 μ).toReal rw [← ENNReal.toReal_mul] exact ENNReal.toReal_mono (ENNReal.mul_ne_top hf.eLpNorm_ne_top hg.eLpNorm_ne_top) - (eLpNorm_smul_le_mul_eLpNorm hf.aestronglyMeasurable hg.aestronglyMeasurable) + (eLpNorm_smul_le_mul_eLpNorm (p := 2) (q := 2) (r := 1) + hf.aestronglyMeasurable hg.aestronglyMeasurable) private theorem lpNorm_norm_sq_sub_le {α : Type*} [MeasurableSpace α] {μ : Measure α} {F G : α → ℂ} @@ -2950,7 +2877,7 @@ private theorem lpNorm_stftRep_sq_sub_tendsto_zero {d : Nat} Tendsto (fun n : Nat => MeasureTheory.lpNorm (fun ξ : PhaseSpace d => Fₙ n ξ - F ξ) 2 μP) atTop (nhds 0) := by - simpa [F, Fₙ, hN, fN, μ, μP] using lpNorm_stftRep_tendsto_schwartzApprox h f + exact lpNorm_stftRep_tendsto_schwartzApprox h f have hC_tendsto : Tendsto Cₙ atTop (nhds (‖f‖ * ‖h‖ + ‖f‖ * ‖h‖)) := by have hprod : Tendsto (fun n : Nat => ‖fN n‖ * ‖hN n‖) atTop @@ -2979,28 +2906,32 @@ private theorem norm_ambiguityRep_sub_le {d : Nat} let T₁ : L2Real d → L2Real d := fun f => translateL2 ((1 / 2 : ℝ) • ξ.1) f let T₂ : L2Real d → L2Real d := fun g => modulateL2 ξ.2 (star (translateL2 (-((1 / 2 : ℝ) • ξ.1)) g)) - have hT₁_norm : ‖T₁ f₂‖ = ‖f₂‖ := by simp [T₁, norm_translateL2] - have hT₂_norm : ‖T₂ g₁‖ = ‖g₁‖ := by simp [T₂, norm_modulateL2, norm_star_L2, norm_translateL2] + have hT₁_norm : ‖T₁ f₂‖ = ‖f₂‖ := norm_translateL2 _ f₂ + have hT₂_norm : ‖T₂ g₁‖ = ‖g₁‖ := + (norm_modulateL2 ξ.2 _).trans ((norm_star_L2 _).trans (norm_translateL2 _ g₁)) have hT₁_sub_norm : ‖T₁ f₁ - T₁ f₂‖ = ‖f₁ - f₂‖ := by calc ‖T₁ f₁ - T₁ f₂‖ = dist (T₁ f₁) (T₁ f₂) := by rw [dist_eq_norm] - _ = dist f₁ f₂ := by simp [T₁, dist_translateL2] + _ = dist f₁ f₂ := dist_translateL2 _ f₁ f₂ _ = ‖f₁ - f₂‖ := by rw [dist_eq_norm] have hT₂_sub_norm : ‖T₂ g₁ - T₂ g₂‖ = ‖g₁ - g₂‖ := by calc ‖T₂ g₁ - T₂ g₂‖ = dist (T₂ g₁) (T₂ g₂) := by rw [dist_eq_norm] _ = dist (star (translateL2 (-((1 / 2 : ℝ) • ξ.1)) g₁)) - (star (translateL2 (-((1 / 2 : ℝ) • ξ.1)) g₂)) := by simp [T₂, dist_modulateL2] + (star (translateL2 (-((1 / 2 : ℝ) • ξ.1)) g₂)) := dist_modulateL2 ξ.2 _ _ _ = dist (translateL2 (-((1 / 2 : ℝ) • ξ.1)) g₁) (translateL2 (-((1 / 2 : ℝ) • ξ.1)) g₂) := by rw [dist_star_L2] _ = dist g₁ g₂ := by rw [dist_translateL2] _ = ‖g₁ - g₂‖ := by rw [dist_eq_norm] - rw [ambiguityRep_eq_lpPairing f₁ g₁ ξ, ambiguityRep_eq_lpPairing f₂ g₂ ξ] - change ‖P (T₁ f₁) (T₂ g₁) - P (T₁ f₂) (T₂ g₂)‖ ≤ - ‖f₁ - f₂‖ * ‖g₁‖ + ‖f₂‖ * ‖g₁ - g₂‖ - simpa only [hT₁_sub_norm, hT₂_norm, hT₁_norm, hT₂_sub_norm] using - norm_bilinear_sub_le P (fun f g => lpPairing_mul_norm_le f g) - (T₁ f₁) (T₁ f₂) (T₂ g₁) (T₂ g₂) + calc + ‖ambiguityRep f₁ g₁ ξ - ambiguityRep f₂ g₂ ξ‖ = + ‖P (T₁ f₁) (T₂ g₁) - P (T₁ f₂) (T₂ g₂)‖ := + congrArg norm (congrArg₂ (fun a b : ℂ => a - b) + (ambiguityRep_eq_lpPairing f₁ g₁ ξ) (ambiguityRep_eq_lpPairing f₂ g₂ ξ)) + _ ≤ ‖f₁ - f₂‖ * ‖g₁‖ + ‖f₂‖ * ‖g₁ - g₂‖ := by + simpa only [hT₁_sub_norm, hT₂_norm, hT₁_norm, hT₂_sub_norm] using + norm_bilinear_sub_le P (fun f g => lpPairing_mul_norm_le f g) + (T₁ f₁) (T₁ f₂) (T₂ g₁) (T₂ g₂) private theorem ambiguityRep_tendsto_schwartzApprox {d : Nat} (f : L2Real d) (ξ : PhaseSpace d) : @@ -3021,7 +2952,7 @@ private theorem ambiguityRep_tendsto_schwartzApprox {d : Nat} refine squeeze_zero (fun _ => dist_nonneg) ?_ (cross_norm_bound_tendsto_zero hfN hfN) intro n rw [dist_eq_norm] - simpa [fN, μ] using norm_ambiguityRep_sub_le (fN n) f (fN n) f ξ + exact norm_ambiguityRep_sub_le (fN n) f (fN n) f ξ /-- Fubini/phase unfolding of `symplecticFourierRep` applied to the spectrogram density: it rewrites the phase-space integral as the iterated integral with the @@ -3339,39 +3270,36 @@ theorem spectrogram_ambiguity_identity let A : ℂ := ambiguityRep f f ξ * star (ambiguityRep h h ξ) let Aₙ : Nat → ℂ := fun n => ambiguityRep (fN n) (fN n) ξ * star (ambiguityRep (hN n) (hN n) ξ) - have hG : Integrable G μP := by simpa [G, μP] using stftRep_sq_complex_integrable h f + have hG : Integrable G μP := by exact stftRep_sq_complex_integrable h f have hGₙ : ∀ n : Nat, Integrable (Gₙ n) μP := by intro n - simpa [Gₙ, hN, fN, μ, μP] using - stftRep_sq_complex_integrable_schwartz_realVec + exact stftRep_sq_complex_integrable_schwartz_realVec (schwartzApproxRealVec (MeasureTheory.Lp.memLp h) n) (schwartzApproxRealVec (MeasureTheory.Lp.memLp f) n) have hLp : Tendsto (fun n : Nat => MeasureTheory.lpNorm (fun η : PhaseSpace d => Gₙ n η - G η) 1 μP) atTop (nhds 0) := by - simpa [G, Gₙ, hN, fN, μ, μP] using lpNorm_stftRep_sq_sub_tendsto_zero h f + exact lpNorm_stftRep_sq_sub_tendsto_zero h f have hfAmb : Tendsto (fun n : Nat => ambiguityRep (fN n) (fN n) ξ) atTop (nhds (ambiguityRep f f ξ)) := by - simpa [fN, μ] using ambiguityRep_tendsto_schwartzApprox f ξ + exact ambiguityRep_tendsto_schwartzApprox f ξ have hhAmb : Tendsto (fun n : Nat => ambiguityRep (hN n) (hN n) ξ) atTop (nhds (ambiguityRep h h ξ)) := by - simpa [hN, μ] using ambiguityRep_tendsto_schwartzApprox h ξ + exact ambiguityRep_tendsto_schwartzApprox h ξ have hA : Tendsto Aₙ atTop (nhds A) := by have hhAmbStar : Tendsto (fun n : Nat => star (ambiguityRep (hN n) (hN n) ξ)) atTop (nhds (star (ambiguityRep h h ξ))) := hhAmb.star - simpa [A, Aₙ] using hfAmb.mul hhAmbStar + exact hfAmb.mul hhAmbStar have hEq : ∀ n : Nat, symplecticFourierRep (Gₙ n) ξ = Aₙ n := by intro n - simpa [Gₙ, Aₙ, hN, fN, μ] using - symplecticFourier_stft_sq_schwartz_realVec + exact symplecticFourier_stft_sq_schwartz_realVec (schwartzApproxRealVec (MeasureTheory.Lp.memLp h) n) (schwartzApproxRealVec (MeasureTheory.Lp.memLp f) n) ξ.1 ξ.2 - simpa [G, A, μP] using - symplecticFourierRep_eq_of_lpNorm_one_approx + exact symplecticFourierRep_eq_of_lpNorm_one_approx (G := G) (Gₙ := Gₙ) (A := A) (Aₙ := Aₙ) hG hGₙ hLp hA ξ hEq theorem continuous_ambiguityRep diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/OrthogonalCoercivity.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/OrthogonalCoercivity.lean index bc9fc7dd85..36fab9b5f3 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/OrthogonalCoercivity.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/OrthogonalCoercivity.lean @@ -12,7 +12,6 @@ import LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermite1Dimd.ImportedAnalyticIn import LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermitek.TrueLevelBasis import LeanPool.PhaseRetrieval.DimdPoly.Internal.ProductAnnulusLocalization import LeanPool.PhaseRetrieval.DimdPoly.Internal.TensorBasis -import Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm import Mathlib.Tactic.NormNum.Parity /-! # OrthogonalCoercivity -/ @@ -180,16 +179,12 @@ private theorem phi1D_eq_oneDimPhi_wip private lemma continuous_Phi_wip {d : Nat} (kappa alpha : MultiIndex d) : Continuous (Phi kappa alpha) := by - unfold Phi phi1D complexHermite - continuity + exact DimdPolyLEAN.continuous_Phi kappa alpha private lemma continuous_evalPkappa_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_wip kappa alpha) + exact DimdPolyLEAN.continuous_evalPkappa kappa F private lemma integrable_oneDimPhi_cross_gaussian_wip (k m n : Nat) : @@ -321,44 +316,17 @@ private theorem gaussianL2Norm_eq_lpNorm_wip (hF : AEStronglyMeasurable F (gammaD d)) : Real.sqrt (∫ z : Cd d, ‖F z‖ ^ (2 : ℝ) ∂ gammaD d) = MeasureTheory.lpNorm F 2 (gammaD d) := by - have htwo : (2 : NNReal) ≠ 0 := by norm_num - have hlp := MeasureTheory.lpNorm_nnreal_eq_integral_norm_rpow - (μ := gammaD d) (p := (2 : NNReal)) (f := F) htwo hF - change - Real.sqrt (∫ z : Cd d, ‖F z‖ ^ (2 : ℝ) ∂ gammaD d) = - MeasureTheory.lpNorm F (↑(2 : NNReal)) (gammaD d) - rw [hlp] - change - Real.sqrt (∫ z : Cd d, ‖F z‖ ^ (2 : ℝ) ∂ gammaD d) = - (∫ z : Cd d, ‖F z‖ ^ (2 : ℝ) ∂ gammaD d) ^ ((2 : ℝ)⁻¹) - rw [Real.sqrt_eq_rpow] - norm_num + exact gaussianL2Norm_eq_lpNorm_from_measurability F hF private theorem memLp_two_evalPkappa_wip (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) : MeasureTheory.MemLp (evalPkappa kappa F) 2 (gammaD d) := by - let _ := hd - have hmeas : - AEStronglyMeasurable (evalPkappa kappa F) (gammaD d) := - (continuous_evalPkappa_wip kappa F).stronglyMeasurable.aestronglyMeasurable - refine (MeasureTheory.memLp_two_iff_integrable_sq_norm hmeas).2 ?_ - simpa [pow_two, norm_mul] using (integrable_evalPkappa_cross_wip kappa F F).norm + exact DimdPolyLEAN.memLp_two_evalPkappa hd kappa F private theorem evalPkappa_lpNorm_eq_norm_wip (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) : MeasureTheory.lpNorm (evalPkappa kappa F) 2 (gammaD d) = ‖F‖ := by - calc - MeasureTheory.lpNorm (evalPkappa kappa F) 2 (gammaD d) - = Real.sqrt (∫ z : Cd d, ‖evalPkappa kappa F z‖ ^ (2 : ℝ) ∂ gammaD d) := - (gaussianL2Norm_eq_lpNorm_wip (evalPkappa kappa F) - (memLp_two_evalPkappa_wip hd kappa F).aestronglyMeasurable).symm - _ = ‖F‖ := by - have hpow : - (∫ z : Cd d, ‖evalPkappa kappa F z‖ ^ (2 : ℝ) ∂ gammaD d) = - ∫ z : Cd d, ‖evalPkappa kappa F z‖ ^ 2 ∂ gammaD d := by - simp_all - rw [hpow, evalPkappa_total_mass hd kappa F, Real.sqrt_sq_eq_abs] - exact abs_of_nonneg (norm_nonneg_pkappa_wip hd F) + exact evalPkappa_lpNorm_eq_coefficient_norm hd kappa F private def defectFunctionPkappa_wip {d : Nat} (kappa : MultiIndex d) (F G : Pkappa d kappa) : @@ -453,61 +421,7 @@ private theorem norm_le_defect_add_two_wip (hd : 0 < d) (kappa : MultiIndex d) (F G : Pkappa d kappa) (hF_norm : ‖F‖ = 1) : ‖G‖ ≤ defect F G + 2 := by - let _ := hd - have hdef_mem := memLp_two_defectFunctionPkappa_wip hd kappa F G - have htwoF_mem : - MeasureTheory.MemLp (fun z : Cd d => 2 * ‖evalPkappa kappa F z‖) 2 (gammaD d) := - (memLp_two_evalPkappa_wip hd kappa F).norm.const_smul (2 : ℝ) - have hsum_mem : - MeasureTheory.MemLp - (defectFunctionPkappa_wip kappa F G + fun z : Cd d => 2 * ‖evalPkappa kappa F z‖) - 2 (gammaD d) := hdef_mem.add htwoF_mem - have hmono : - MeasureTheory.lpNorm (evalPkappa kappa G) 2 (gammaD d) ≤ - MeasureTheory.lpNorm - (defectFunctionPkappa_wip kappa F G + fun z : Cd d => 2 * ‖evalPkappa kappa F z‖) - 2 (gammaD d) := by - refine MeasureTheory.lpNorm_mono_real hsum_mem ?_ - intro z - simpa using evalPkappa_pointwise_bound_wip kappa F G z - have htri : - MeasureTheory.lpNorm - (defectFunctionPkappa_wip kappa F G + fun z : Cd d => 2 * ‖evalPkappa kappa F z‖) - 2 (gammaD d) - ≤ MeasureTheory.lpNorm (defectFunctionPkappa_wip kappa F G) 2 (gammaD d) + - MeasureTheory.lpNorm (fun z : Cd d => 2 * ‖evalPkappa kappa F z‖) 2 (gammaD d) := by - exact MeasureTheory.lpNorm_add_le hdef_mem (g := fun z : Cd d => 2 * ‖evalPkappa kappa F z‖) - (by norm_num) - have hnormEq : - MeasureTheory.lpNorm (fun z : Cd d => ‖evalPkappa kappa F z‖) 2 (gammaD d) = - MeasureTheory.lpNorm (evalPkappa kappa F) 2 (gammaD d) := by - simpa using - (MeasureTheory.lpNorm_norm (μ := gammaD d) (p := (2 : ENNReal)) - (memLp_two_evalPkappa_wip hd kappa F).aestronglyMeasurable) - have htwoF_norm : - MeasureTheory.lpNorm (fun z : Cd d => 2 * ‖evalPkappa kappa F z‖) - 2 (gammaD d) = 2 := by - calc - MeasureTheory.lpNorm (fun z : Cd d => 2 * ‖evalPkappa kappa F z‖) 2 (gammaD d) - = MeasureTheory.lpNorm - ((2 : ℝ) • fun z : Cd d => ‖evalPkappa kappa F z‖) 2 (gammaD d) := by rfl - _ = ‖(2 : ℝ)‖ * - MeasureTheory.lpNorm (fun z : Cd d => ‖evalPkappa kappa F z‖) 2 (gammaD d) := by - rw [MeasureTheory.lpNorm_const_smul] - norm_num - _ = 2 * MeasureTheory.lpNorm (evalPkappa kappa F) 2 (gammaD d) := by - simp_all - _ = 2 * ‖F‖ := by rw [evalPkappa_lpNorm_eq_norm_wip hd kappa F] - _ = 2 := by simp [hF_norm] - calc - ‖G‖ = MeasureTheory.lpNorm (evalPkappa kappa G) 2 (gammaD d) := - (evalPkappa_lpNorm_eq_norm_wip hd kappa G).symm - _ ≤ MeasureTheory.lpNorm - (defectFunctionPkappa_wip kappa F G + fun z : Cd d => 2 * ‖evalPkappa kappa F z‖) - 2 (gammaD d) := hmono - _ ≤ MeasureTheory.lpNorm (defectFunctionPkappa_wip kappa F G) 2 (gammaD d) + - MeasureTheory.lpNorm (fun z : Cd d => 2 * ‖evalPkappa kappa F z‖) 2 (gammaD d) := htri - _ = defect F G + 2 := by rw [← defect_lpNorm_eq_wip hd kappa F G, htwoF_norm] + exact norm_le_defect_add_two_of_norm_one hd kappa F G hF_norm theorem orthogonal_coercivity (hd : 0 < d) (F : Pk) (hF_ne : F ≠ 0) (hF_norm : ‖F‖ = 1) : diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/PhaseStability.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/PhaseStability.lean index 0847efa6f4..b57d87f64c 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/PhaseStability.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/PhaseStability.lean @@ -110,34 +110,12 @@ private theorem gaussianL2Norm_eq_lpNorm (hF : AEStronglyMeasurable F (gammaD d)) : Real.sqrt (∫ z : Cd d, ‖F z‖ ^ (2 : ℝ) ∂ gammaD d) = lpNorm F 2 (gammaD d) := by - have htwo : (2 : NNReal) ≠ 0 := by norm_num - have hlp := MeasureTheory.lpNorm_nnreal_eq_integral_norm_rpow - (μ := gammaD d) (p := (2 : NNReal)) (f := F) htwo hF - change - Real.sqrt (∫ z : Cd d, ‖F z‖ ^ (2 : ℝ) ∂ gammaD d) = - lpNorm F (↑(2 : NNReal)) (gammaD d) - rw [hlp] - change - Real.sqrt (∫ z : Cd d, ‖F z‖ ^ (2 : ℝ) ∂ gammaD d) = - (∫ z : Cd d, ‖F z‖ ^ (2 : ℝ) ∂ gammaD d) ^ ((2 : ℝ)⁻¹) - rw [Real.sqrt_eq_rpow] - norm_num + exact gaussianL2Norm_eq_lpNorm_from_measurability F hF theorem evalPkappa_lpNorm_eq_norm {d : Nat} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) : lpNorm (evalPkappa kappa F) 2 (gammaD d) = ‖F‖ := by - calc - lpNorm (evalPkappa kappa F) 2 (gammaD d) - = Real.sqrt (∫ z : Cd d, ‖evalPkappa kappa F z‖ ^ (2 : ℝ) ∂ gammaD d) := - (gaussianL2Norm_eq_lpNorm (evalPkappa kappa F) - (memLp_two_evalPkappa hd kappa F).aestronglyMeasurable).symm - _ = ‖F‖ := by - have hpow : - (∫ z : Cd d, ‖evalPkappa kappa F z‖ ^ (2 : ℝ) ∂ gammaD d) = - ∫ z : Cd d, ‖evalPkappa kappa F z‖ ^ 2 ∂ gammaD d := by - simp_all - rw [hpow, evalPkappa_total_mass hd kappa F, Real.sqrt_sq_eq_abs] - exact abs_of_nonneg (Real.sqrt_nonneg _) + exact evalPkappa_lpNorm_eq_coefficient_norm hd kappa F theorem evalPkappaL2_norm {d : Nat} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) : diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/ProductAnnulusLocalization.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/ProductAnnulusLocalization.lean index 45ce2728b9..aac30e677b 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/ProductAnnulusLocalization.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/ProductAnnulusLocalization.lean @@ -80,16 +80,12 @@ private theorem norm_ne_zero_of_ne_zero_pkappa_wip private lemma continuous_Phi_wip {d : Nat} (kappa alpha : MultiIndex d) : Continuous (Phi kappa alpha) := by - unfold Phi phi1D complexHermite - continuity + exact DimdPolyLEAN.continuous_Phi kappa alpha private lemma continuous_evalPkappa_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_wip kappa alpha) + exact DimdPolyLEAN.continuous_evalPkappa kappa F private lemma measurableSet_productAnnulus_wip {d : Nat} (j : Idx d) : @@ -136,21 +132,7 @@ private lemma sum_indicator_productAnnulus_le_wip private theorem integrable_evalPkappa_sq_wip {d : Nat} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) : Integrable (fun z : Cd d => ‖evalPkappa kappa F z‖ ^ 2) (gammaD d) := by - by_cases hF : F = 0 - · subst hF - simp [evalPkappa] - · have hmeas : - AEStronglyMeasurable (fun z : Cd d => ‖evalPkappa kappa F z‖ ^ 2) (gammaD d) := - ((continuous_evalPkappa_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_wip hd hF - simp_all + exact DimdPolyLEAN.integrable_evalPkappa_sq hd kappa F private theorem finite_sum_annulusMass_le_wip {d : Nat} (hd : 0 < d) (kappa : MultiIndex d) diff --git a/LeanPool/PhaseRetrieval/DimdPoly/Internal/TensorBasis.lean b/LeanPool/PhaseRetrieval/DimdPoly/Internal/TensorBasis.lean index 8e9897b347..bd0e81c280 100644 --- a/LeanPool/PhaseRetrieval/DimdPoly/Internal/TensorBasis.lean +++ b/LeanPool/PhaseRetrieval/DimdPoly/Internal/TensorBasis.lean @@ -352,59 +352,12 @@ theorem toFun_ofPkappa private theorem summable_sq_hermite_phi_eval (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 (k : Nat) (z : ℂ) :