diff --git a/Expdb.lean b/Expdb.lean index 3f46d17..ee921a0 100644 --- a/Expdb.lean +++ b/Expdb.lean @@ -1,9 +1,15 @@ module public import Expdb.Basic.AutomaticUniformity +public import Expdb.Basic.PowerAsymptotics public import Expdb.ExponentialSums.ExponentSumGrowthNonAsymptotic public import Expdb.ExponentialSums.LogPhase +public import Expdb.ExponentialSums.FixedExponentialSum public import Expdb.ExponentialSums.OscillatoryBounds +public import Expdb.ExponentialSums.ScaleTransfer public import Expdb.ExponentialSums.TrivialBounds +public import Expdb.ExponentialSums.UpperSemicontinuity +public import Expdb.Fourier.Bump public import Expdb.Fourier.L2Integral public import Expdb.Mathlib.EulerMaclaurin +public import Expdb.Mathlib.IteratedDeriv diff --git a/Expdb/Basic/Asymptotics.lean b/Expdb/Basic/Asymptotics.lean index be39f1c..1d03bc2 100644 --- a/Expdb/Basic/Asymptotics.lean +++ b/Expdb/Basic/Asymptotics.lean @@ -20,7 +20,7 @@ These are represented by `VariableObject`. Their asymptotic properties are encod `VariableObject` namespace. Variable functions whose domain type may depend on the ambient parameter are represented by -`VariableFunction`. Their pointwise asymptotic properties are encoded in the +`VariableFunction`. Their choicewise asymptotic properties are encoded in the `VariableFunction` namespace. -/ @@ -59,6 +59,13 @@ theorem isUnbounded_iff_forall_eventually_norm_ge (X : VariableObject α) : X.IsUnbounded ↔ ∀ C : ℝ, ∀ᶠ i in atTop, C ≤ ‖X i‖ := by rw [IsUnbounded, tendsto_atTop] +/-- For a nonnegative real variable object, being unbounded is the same as tending to +infinity. -/ +theorem isUnbounded_iff_tendsto_atTop {X : VariableObject ℝ} (hX : ∀ i, 0 ≤ X i) : + X.IsUnbounded ↔ Tendsto X atTop atTop := by + rw [IsUnbounded] + exact tendsto_congr fun i ↦ by rw [Real.norm_eq_abs, abs_of_nonneg (hX i)] + /-- A variable object whose norm tends to zero. -/ def IsInfinitesimal (X : VariableObject α) : Prop := Tendsto (fun i ↦ ‖X i‖) atTop (nhds 0) @@ -80,14 +87,42 @@ variable {α : Type v} [SeminormedAddCommGroup α] /-- A variable function that is bounded along every variable choice. The choice may vary with the ambient index; it is not a fixed point of the domain. -/ -def IsPointwiseBounded (f : VariableFunction domain α) : Prop := +def IsChoicewiseBounded (f : VariableFunction domain α) : Prop := ∀ x : ∀ i, domain i, VariableObject.IsBounded (fun i ↦ f i (x i)) /-- A variable function that is infinitesimal along every variable choice. The choice may vary with the ambient index; it is not a fixed point of the domain. -/ -def IsPointwiseInfinitesimal (f : VariableFunction domain α) : Prop := +def IsChoicewiseInfinitesimal (f : VariableFunction domain α) : Prop := ∀ x : ∀ i, domain i, VariableObject.IsInfinitesimal (fun i ↦ f i (x i)) +/-! An example from the blueprint that shows why choices must be allowed to vary. +For `fᵢ(x) = x / (i + 1)`, every fixed input gives an infinitesimal variable object, but the +variable choice `xᵢ = i + 1` makes `fᵢ(xᵢ) = 1`. -/ + +example : + (∀ x : ℝ, VariableObject.IsInfinitesimal + (fun i : ℕ ↦ x / ((i : ℝ) + 1))) ∧ + ¬ IsChoicewiseInfinitesimal + ((fun i (x : ℝ) ↦ x / ((i : ℝ) + 1)) : + VariableFunction (VariableObject.fixed ℝ) ℝ) := by + constructor + · intro x + rw [VariableObject.IsInfinitesimal] + have h := (tendsto_const_nhds (x := x)).mul + (tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ)) + simpa [div_eq_mul_inv] using h.norm + · intro h + have hx := h (fun i : ℕ ↦ (i : ℝ) + 1) + have hsmall := + (VariableObject.isInfinitesimal_iff_forall_pos _).1 hx 1 zero_lt_one + rw [Filter.eventually_atTop] at hsmall + obtain ⟨N, hN⟩ := hsmall + have hcontra := hN N le_rfl + have hdenom : (N : ℝ) + 1 ≠ 0 := by positivity + change ‖((N : ℝ) + 1) / ((N : ℝ) + 1)‖ < 1 at hcontra + rw [div_self hdenom, norm_one] at hcontra + exact (lt_irrefl (1 : ℝ)) hcontra + end VariableFunction section InfinitesimalRelations diff --git a/Expdb/Basic/AutomaticUniformity.lean b/Expdb/Basic/AutomaticUniformity.lean index 6243c16..7f4f7d6 100644 --- a/Expdb/Basic/AutomaticUniformity.lean +++ b/Expdb/Basic/AutomaticUniformity.lean @@ -7,7 +7,7 @@ public import Expdb.Basic.Asymptotics This module formalizes the automatic uniformity results of the blueprint's Basic notation chapter (`notation-chapter`): -pointwise boundedness or infinitesimality along every variable sequence can be made uniform +choicewise boundedness or infinitesimality along every variable sequence can be made uniform after passing to a subsequence. -/ @@ -121,10 +121,10 @@ private lemma norm_extend_subsequence_apply /-- **Automatic uniform bound (blueprint `auto`, case (i)).** If f(x) = O(1) for every variable x ∈ E, then after passing to a subsequence there exists a *fixed* C with |f(x)| ≤ C for all x ∈ E. -/ -theorem automatic_uniformity_of_pointwise_bounded +theorem automatic_uniformity_of_choicewise_bounded (E : VariableObject (Set ℝ)) (hE : ∀ i, (E i).Nonempty) (f : VariableFunction (fun i ↦ E i) α) - (hf : f.IsPointwiseBounded) : + (hf : f.IsChoicewiseBounded) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∃ C : ℝ, ∀ i, ∀ x : E (φ i), ‖f (φ i) x‖ ≤ C := by @@ -139,7 +139,7 @@ theorem automatic_uniformity_of_pointwise_bounded exact ⟨i, hi, x, hx⟩ obtain ⟨φ, hφ, x_bad, hx_bad⟩ := extract_bad_seq_i E f bad let y : ∀ j, E j := extend_subsequence E hE φ x_bad - -- Apply pointwise bound to y + -- Apply the choicewise bound to y obtain ⟨C_y, hC_y⟩ := hf y rw [Filter.eventually_atTop] at hC_y obtain ⟨j₀, hj₀⟩ := hC_y @@ -167,10 +167,10 @@ theorem automatic_uniformity_of_pointwise_bounded /-- **Automatic uniform infinitesimal (blueprint `auto`, case (ii)).** If f(x) = o(1) for every variable x ∈ E, then after passing to a subsequence there exists an *infinitesimal* c with |f(x)| ≤ c for all x ∈ E. -/ -theorem automatic_uniformity_of_pointwise_infinitesimal +theorem automatic_uniformity_of_choicewise_infinitesimal (E : VariableObject (Set ℝ)) (hE : ∀ i, (E i).Nonempty) (f : VariableFunction (fun i ↦ E i) α) - (hf : f.IsPointwiseInfinitesimal) : + (hf : f.IsChoicewiseInfinitesimal) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∃ c : VariableObject ℝ, c.IsInfinitesimal ∧ ∀ i, ∀ x : E (φ i), @@ -209,11 +209,11 @@ theorem automatic_uniformity_of_pointwise_infinitesimal /-! ### Full-tail uniformity -/ /-- Boundedness along every variable choice is equivalent to an eventual bound uniform over -the original variable sets. This strengthens `automatic_uniformity_of_pointwise_bounded`. -/ -theorem VariableFunction.isPointwiseBounded_iff_eventually_uniform +the original variable sets. This strengthens `automatic_uniformity_of_choicewise_bounded`. -/ +theorem VariableFunction.isChoicewiseBounded_iff_eventually_uniform (E : VariableObject (Set ℝ)) (hE : ∀ i, (E i).Nonempty) (f : VariableFunction (fun i ↦ E i) α) : - f.IsPointwiseBounded ↔ + f.IsChoicewiseBounded ↔ ∃ C : ℝ, ∀ᶠ i in atTop, ∀ x : E i, ‖f i x‖ ≤ C := by constructor · intro hf @@ -241,11 +241,11 @@ theorem VariableFunction.isPointwiseBounded_iff_eventually_uniform /-- Infinitesimality along every variable choice is equivalent to convergence that is eventually uniform over the original variable sets. This strengthens -`automatic_uniformity_of_pointwise_infinitesimal`. -/ -theorem VariableFunction.isPointwiseInfinitesimal_iff_forall_pos_uniform +`automatic_uniformity_of_choicewise_infinitesimal`. -/ +theorem VariableFunction.isChoicewiseInfinitesimal_iff_forall_pos_uniform (E : VariableObject (Set ℝ)) (hE : ∀ i, (E i).Nonempty) (f : VariableFunction (fun i ↦ E i) α) : - f.IsPointwiseInfinitesimal ↔ + f.IsChoicewiseInfinitesimal ↔ ∀ ε : ℝ, 0 < ε → ∀ᶠ i in atTop, ∀ x : E i, ‖f i x‖ < ε := by constructor diff --git a/Expdb/Basic/PowerAsymptotics.lean b/Expdb/Basic/PowerAsymptotics.lean new file mode 100644 index 0000000..22d1d75 --- /dev/null +++ b/Expdb/Basic/PowerAsymptotics.lean @@ -0,0 +1,523 @@ +module + +public import Expdb.Basic.Asymptotics +public import Mathlib.Analysis.Asymptotics.Defs +public import Mathlib.Analysis.Asymptotics.Lemmas +public import Mathlib.Analysis.SpecialFunctions.Log.Base +public import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics + +/-! +# Power asymptotics + +This module collects the project-wide notation and elementary calculus for quantities of the +form `T ^ (α + o(1))`. It is independent of exponential sums and can therefore be reused by +all later asymptotic arguments. +-/ + +@[expose] public section + +open Filter Topology +open scoped Expdb + +noncomputable section + +namespace Expdb + +/-! ## Definitions -/ + +/-- `N = T ^ (α + o(1))`, expressed using a variable exponent that is equal to `α` up to an +infinitesimal. -/ +def IsPowerAsymptotic (N T : VariableObject ℝ) (α : ℝ) : Prop := + ∃ exponent : VariableObject ℝ, + exponent =o VariableObject.fixed α ∧ + ∀ᶠ i in atTop, N i = T i ^ exponent i + +/-- `X ≪ T ^ (β + o(1))`, expressed using a variable exponent that is equal to `β` up to +an infinitesimal. -/ +def IsPowerBounded {E : Type*} [SeminormedAddCommGroup E] + (X : VariableObject E) (T : VariableObject ℝ) (β : ℝ) : Prop := + ∃ exponent : VariableObject ℝ, + exponent =o VariableObject.fixed β ∧ + Asymptotics.IsBigO atTop X (fun i ↦ T i ^ exponent i) + +/-! ## Power asymptotics -/ + +/-- If `N = T ^ (α + o(1))`, then `N` eventually lies between the powers with exponents +`α - ε` and `α + ε`. -/ +theorem IsPowerAsymptotic.eventually_between + {N T : VariableObject ℝ} {α ε : ℝ} + (hNT : IsPowerAsymptotic N T α) + (hT : ∀ᶠ i in atTop, 1 ≤ T i) + (hε : 0 < ε) : + ∀ᶠ i in atTop, T i ^ (α - ε) ≤ N i ∧ N i ≤ T i ^ (α + ε) := by + obtain ⟨exponent, hexponent, hN⟩ := hNT + obtain ⟨hexponent_le, halpha_le⟩ := + (isEqUpToInfinitesimal_iff_leUpToInfinitesimal + exponent (VariableObject.fixed α)).1 hexponent + have hupper := (isLEUpToInfinitesimal_iff_forall_pos + exponent (VariableObject.fixed α)).1 hexponent_le ε hε + have hlower := (isLEUpToInfinitesimal_iff_forall_pos + (VariableObject.fixed α) exponent).1 halpha_le ε hε + filter_upwards [hT, hN, hupper, hlower] with i hiT hiN hiupper hilower + rw [hiN] + exact + ⟨Real.rpow_le_rpow_of_exponent_le hiT (by linarith), + Real.rpow_le_rpow_of_exponent_le hiT (by linarith)⟩ + +/-- Convergence of the logarithmic exponent gives a power asymptotic. -/ +theorem isPowerAsymptotic_of_logb_tendsto + {N T : VariableObject ℝ} {α : ℝ} + (hT : ∀ᶠ i in atTop, 1 < T i) (hN : ∀ᶠ i in atTop, 0 < N i) + (hexponent : Tendsto (fun i ↦ Real.logb (T i) (N i)) atTop (nhds α)) : + IsPowerAsymptotic N T α := by + let exponent : VariableObject ℝ := fun i ↦ Real.logb (T i) (N i) + refine ⟨exponent, ?_, ?_⟩ + · rw [IsEqUpToInfinitesimal, VariableObject.IsInfinitesimal] + have hsub : Tendsto (fun i ↦ Real.logb (T i) (N i) - α) atTop (nhds 0) := by + simpa using hexponent.sub + (tendsto_const_nhds : Tendsto (fun _ : ℕ ↦ α) atTop (nhds α)) + convert (continuous_norm.tendsto 0).comp hsub using 1 <;> + simp [Function.comp_def, exponent, VariableObject.fixed] + · filter_upwards [hT, hN] with i hiT hiN + exact (Real.rpow_logb (zero_lt_one.trans hiT) hiT.ne' hiN).symm + +/-- A variable power sandwich with an infinitesimal error determines a power asymptotic. No +sign condition on the error is needed. -/ +theorem isPowerAsymptotic_of_between_of_infinitesimal + {N T δ : VariableObject ℝ} {α : ℝ} + (hT : ∀ i, 1 < T i) (hN : ∀ i, 0 < N i) + (hδ : δ.IsInfinitesimal) + (hbetween : ∀ i, + T i ^ (α - δ i) ≤ N i ∧ N i ≤ T i ^ (α + δ i)) : + IsPowerAsymptotic N T α := by + let exponent : VariableObject ℝ := fun i ↦ Real.logb (T i) (N i) + refine ⟨exponent, ?_, Filter.Eventually.of_forall fun i ↦ ?_⟩ + · apply (isEqUpToInfinitesimal_iff_forall_pos + exponent (VariableObject.fixed α)).2 + intro ε hε + have hδsmall := + (VariableObject.isInfinitesimal_iff_forall_pos δ).1 hδ ε hε + filter_upwards [hδsmall] with i hi + have hlower : α - δ i ≤ exponent i := + (Real.le_logb_iff_rpow_le (hT i) (hN i)).2 (hbetween i).1 + have hupper : exponent i ≤ α + δ i := + (Real.logb_le_iff_le_rpow (hT i) (hN i)).2 (hbetween i).2 + rw [Real.norm_eq_abs, abs_lt] + rw [Real.norm_eq_abs] at hi + have hδupper : δ i < ε := (le_abs_self (δ i)).trans_lt hi + constructor <;> dsimp [exponent, VariableObject.fixed] at * <;> linarith + · exact (Real.rpow_logb (lt_trans zero_lt_one (hT i)) + (hT i).ne' (hN i)).symm + +/-- A variable power sandwich with a nonnegative infinitesimal error determines a power +asymptotic. This is the compatibility form of +`isPowerAsymptotic_of_between_of_infinitesimal`. -/ +theorem isPowerAsymptotic_of_between + {N T δ : VariableObject ℝ} {α : ℝ} + (hT : ∀ i, 1 < T i) (hN : ∀ i, 0 < N i) + (_hδnonneg : ∀ i, 0 ≤ δ i) (hδ : δ.IsInfinitesimal) + (hbetween : ∀ i, + T i ^ (α - δ i) ≤ N i ∧ N i ≤ T i ^ (α + δ i)) : + IsPowerAsymptotic N T α := + isPowerAsymptotic_of_between_of_infinitesimal hT hN hδ hbetween + +/-- If `T` lies between fixed positive multiples of `N ^ α⁻¹`, then the logarithm of `N` to +base `T` tends to `α`. -/ +private lemma tendsto_logb_of_between_const_rpow + {N T : VariableObject ℝ} {α A B : ℝ} + (hα : 0 < α) (hA : 0 < A) (hB : 0 < B) + (hNtop : Tendsto N atTop atTop) + (hT : ∀ᶠ i in atTop, A * N i ^ α⁻¹ ≤ T i ∧ T i ≤ B * N i ^ α⁻¹) : + Tendsto (fun i ↦ Real.logb (T i) (N i)) atTop (nhds α) := by + have hlogNtop : Tendsto (fun i ↦ Real.log (N i)) atTop atTop := + Real.tendsto_log_atTop.comp hNtop + have hNgt : ∀ᶠ i in atTop, 1 < N i := hNtop.eventually (eventually_gt_atTop 1) + have hlogNpos : ∀ᶠ i in atTop, 0 < Real.log (N i) := by + filter_upwards [hNgt] with i hi + exact Real.log_pos hi + have hpowtop : Tendsto (fun i ↦ N i ^ α⁻¹) atTop atTop := + (tendsto_rpow_atTop (inv_pos.mpr hα)).comp hNtop + have hpowlarge : ∀ᶠ i in atTop, 1 / A < N i ^ α⁻¹ := + hpowtop.eventually (eventually_gt_atTop (1 / A)) + have hTgt : ∀ᶠ i in atTop, 1 < T i := by + filter_upwards [hpowlarge, hT] with i hi hTi + have : 1 < A * N i ^ α⁻¹ := by + simpa [mul_comm] using (div_lt_iff₀ hA).1 hi + exact this.trans_le hTi.1 + have hratio : Tendsto (fun i ↦ Real.log (T i) / Real.log (N i)) atTop (nhds α⁻¹) := by + have hlowerLimit : Tendsto + (fun i ↦ Real.log A / Real.log (N i) + α⁻¹) atTop (nhds α⁻¹) := by + simpa using (tendsto_const_nhds.div_atTop hlogNtop).add + (tendsto_const_nhds : Tendsto (fun _ : ℕ ↦ α⁻¹) atTop (nhds α⁻¹)) + have hupperLimit : Tendsto + (fun i ↦ Real.log B / Real.log (N i) + α⁻¹) atTop (nhds α⁻¹) := by + simpa using (tendsto_const_nhds.div_atTop hlogNtop).add + (tendsto_const_nhds : Tendsto (fun _ : ℕ ↦ α⁻¹) atTop (nhds α⁻¹)) + apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hlowerLimit hupperLimit + · filter_upwards [hNgt, hlogNpos, hT] with i hNi hlogNi hTi + have hbase : 0 < N i := zero_lt_one.trans hNi + have hlower := Real.log_le_log (mul_pos hA (Real.rpow_pos_of_pos hbase _)) hTi.1 + rw [Real.log_mul hA.ne' (Real.rpow_pos_of_pos hbase _).ne', + Real.log_rpow hbase] at hlower + apply (le_div_iff₀ hlogNi).2 + rw [add_mul, div_mul_cancel₀ _ hlogNi.ne'] + simpa [mul_comm] using hlower + · filter_upwards [hNgt, hlogNpos, hT] with i hNi hlogNi hTi + have hbase : 0 < N i := zero_lt_one.trans hNi + have hupper := Real.log_le_log (lt_of_lt_of_le + (mul_pos hA (Real.rpow_pos_of_pos hbase _)) hTi.1) hTi.2 + rw [Real.log_mul hB.ne' (Real.rpow_pos_of_pos hbase _).ne', + Real.log_rpow hbase] at hupper + apply (div_le_iff₀ hlogNi).2 + rw [add_mul, div_mul_cancel₀ _ hlogNi.ne'] + simpa [mul_comm] using hupper + have hinv := hratio.inv₀ (inv_ne_zero hα.ne') + have hinv' : Tendsto (fun i ↦ Real.logb (T i) (N i)) atTop (nhds α⁻¹⁻¹) := + hinv.congr' <| by + filter_upwards [hlogNpos, hTgt] with i hlogNi hTi + dsimp [Real.logb] + field_simp [hlogNi.ne', (Real.log_pos hTi).ne'] + simpa using hinv' + +/-- Fixed positive multiplicative uncertainty in `T = N ^ α⁻¹` does not affect the +power asymptotic `N = T ^ (α + o(1))`. -/ +theorem isPowerAsymptotic_of_between_const_rpow + {N T : VariableObject ℝ} {α A B : ℝ} + (hα : 0 < α) (hA : 0 < A) (hB : 0 < B) + (hNtop : Tendsto N atTop atTop) + (hT : ∀ᶠ i in atTop, A * N i ^ α⁻¹ ≤ T i ∧ T i ≤ B * N i ^ α⁻¹) : + IsPowerAsymptotic N T α := by + have hNpos : ∀ᶠ i in atTop, 0 < N i := + hNtop.eventually (eventually_gt_atTop 0) + have hpowtop : Tendsto (fun i ↦ N i ^ α⁻¹) atTop atTop := + (tendsto_rpow_atTop (inv_pos.mpr hα)).comp hNtop + have hpowlarge : ∀ᶠ i in atTop, 1 / A < N i ^ α⁻¹ := + hpowtop.eventually (eventually_gt_atTop (1 / A)) + have hTgt : ∀ᶠ i in atTop, 1 < T i := by + filter_upwards [hpowlarge, hT] with i hi hTi + have : 1 < A * N i ^ α⁻¹ := by + simpa [mul_comm] using (div_lt_iff₀ hA).1 hi + exact this.trans_le hTi.1 + exact isPowerAsymptotic_of_logb_tendsto hTgt + hNpos (tendsto_logb_of_between_const_rpow hα hA hB hNtop hT) + +/-! ## Algebra and limits -/ + +/-- A base is power-asymptotic to itself with exponent one. -/ +theorem isPowerAsymptotic_self (T : VariableObject ℝ) : + IsPowerAsymptotic T T 1 := + ⟨VariableObject.fixed 1, IsEqUpToInfinitesimal.refl _, + Filter.Eventually.of_forall fun i ↦ (Real.rpow_one (T i)).symm⟩ + +/-- Products of powers add their asymptotic exponents. -/ +theorem IsPowerAsymptotic.mul + {A B T : VariableObject ℝ} {α β : ℝ} + (hA : IsPowerAsymptotic A T α) (hB : IsPowerAsymptotic B T β) + (hT : ∀ i, 1 ≤ T i) : + IsPowerAsymptotic (A * B) T (α + β) := by + obtain ⟨a, ha, hAeq⟩ := hA + obtain ⟨b, hb, hBeq⟩ := hB + refine ⟨a + b, ?_, ?_⟩ + · have hab := ha.add hb + convert hab using 1 + · ext i + rfl + · filter_upwards [hAeq, hBeq] with i hiA hiB + simp only [Pi.mul_apply, hiA, hiB] + simpa only [Pi.add_apply] using + (Real.rpow_add (zero_lt_one.trans_le (hT i)) (a i) (b i)).symm + +/-- Quotients of powers subtract their asymptotic exponents. -/ +theorem IsPowerAsymptotic.div + {A B T : VariableObject ℝ} {α β : ℝ} + (hA : IsPowerAsymptotic A T α) (hB : IsPowerAsymptotic B T β) + (hT : ∀ i, 1 ≤ T i) : + IsPowerAsymptotic (A / B) T (α - β) := by + obtain ⟨a, ha, hAeq⟩ := hA + obtain ⟨b, hb, hBeq⟩ := hB + refine ⟨a - b, ?_, ?_⟩ + · have hab := ha.sub hb + convert hab using 1 + · ext i + rfl + · filter_upwards [hAeq, hBeq] with i hiA hiB + simp only [Pi.div_apply, hiA, hiB] + simpa only [Pi.sub_apply] using + (Real.rpow_sub (zero_lt_one.trans_le (hT i)) (a i) (b i)).symm + +/-- A negative power-asymptotic exponent forces convergence to zero. -/ +theorem IsPowerAsymptotic.tendsto_zero_of_neg + {X T : VariableObject ℝ} {α : ℝ} (hX : IsPowerAsymptotic X T α) + (hα : α < 0) (hT : ∀ i, 1 ≤ T i) (hTunbounded : T.IsUnbounded) : + Tendsto X atTop (𝓝 0) := by + have hTtop : Tendsto T atTop atTop := + (VariableObject.isUnbounded_iff_tendsto_atTop + (fun i ↦ zero_le_one.trans (hT i))).mp hTunbounded + have hbetween := hX.eventually_between (Filter.Eventually.of_forall hT) + (show 0 < -α / 2 by linarith) + have hpowzero : Tendsto (fun i ↦ T i ^ (α + -α / 2)) atTop (𝓝 0) := by + have : 0 < -(α + -α / 2) := by linarith + simpa [Function.comp_def, neg_neg] using + (tendsto_rpow_neg_atTop this).comp hTtop + apply squeeze_zero' + · filter_upwards [hbetween] with i hi + exact (Real.rpow_nonneg (zero_le_one.trans (hT i)) _).trans hi.1 + · exact hbetween.mono fun _ hi ↦ hi.2 + · exact hpowzero + +/-- A positive power-asymptotic exponent forces convergence to infinity. -/ +theorem IsPowerAsymptotic.tendsto_atTop_of_pos + {X T : VariableObject ℝ} {α : ℝ} (hX : IsPowerAsymptotic X T α) + (hα : 0 < α) (hT : ∀ i, 1 ≤ T i) (hTunbounded : T.IsUnbounded) : + Tendsto X atTop atTop := by + have hTtop : Tendsto T atTop atTop := + (VariableObject.isUnbounded_iff_tendsto_atTop + (fun i ↦ zero_le_one.trans (hT i))).mp hTunbounded + have hbetween := hX.eventually_between (Filter.Eventually.of_forall hT) + (show 0 < α / 2 by linarith) + apply tendsto_atTop_mono' atTop (hbetween.mono fun _ hi ↦ hi.1) + exact (tendsto_rpow_atTop (show 0 < α - α / 2 by linarith)).comp hTtop + +/-- A quantity tending to one has power-asymptotic exponent zero relative to any unbounded +base that is at least one. -/ +theorem isPowerAsymptotic_zero_of_tendsto_one + {X T : VariableObject ℝ} (hX : Tendsto X atTop (𝓝 1)) + (hT : ∀ i, 1 ≤ T i) (hTunbounded : T.IsUnbounded) : + IsPowerAsymptotic X T 0 := by + have hTtop : Tendsto T atTop atTop := + (VariableObject.isUnbounded_iff_tendsto_atTop + (fun i ↦ zero_le_one.trans (hT i))).mp hTunbounded + have hTgt : ∀ᶠ i in atTop, 1 < T i := hTtop.eventually (eventually_gt_atTop 1) + have hXpos : ∀ᶠ i in atTop, 0 < X i := hX.eventually (eventually_gt_nhds zero_lt_one) + apply isPowerAsymptotic_of_logb_tendsto hTgt hXpos + have hlogX : Tendsto (fun i ↦ Real.log (X i)) atTop (𝓝 0) := by + simpa [Function.comp_def] using + (Real.continuousAt_log one_ne_zero).tendsto.comp hX + have hlogTtop := Real.tendsto_log_atTop.comp hTtop + simpa [Real.logb] using hlogX.div_atTop hlogTtop + +/-! ## Natural-valued power scales -/ + +/-- The positive natural scale obtained by taking the floor of `T ^ κ`. -/ +def floorRpow (T : VariableObject ℝ) (κ : ℝ) : VariableObject ℕ := + fun i ↦ max 1 ⌊T i ^ κ⌋₊ + +theorem floorRpow_pos (T : VariableObject ℝ) (κ : ℝ) (i : ℕ) : + 0 < floorRpow T κ i := by + simp [floorRpow] + +/-- Flooring a divergent positive power introduces only a multiplicative `1 + o(1)` error. -/ +theorem tendsto_floorRpow_cast_div_rpow_one + {T : VariableObject ℝ} {κ : ℝ} (hκ : 0 < κ) + (hT : Tendsto T atTop atTop) : + Tendsto (fun i ↦ (floorRpow T κ i : ℝ) / T i ^ κ) atTop (𝓝 1) := by + have hpow : Tendsto (fun i ↦ T i ^ κ) atTop atTop := + (tendsto_rpow_atTop hκ).comp hT + have hlarge : ∀ᶠ i in atTop, 1 ≤ T i ^ κ := hpow.eventually (eventually_ge_atTop 1) + have hfloor : ∀ᶠ i in atTop, + floorRpow T κ i = ⌊T i ^ κ⌋₊ := by + filter_upwards [hlarge] with i hi + exact max_eq_right ((Nat.one_le_floor_iff _).mpr hi) + apply (tendsto_nat_floor_div_atTop.comp hpow).congr' + filter_upwards [hfloor] with i hi + simp only [Function.comp_apply] + rw [hi] + +/-- The cast of `floorRpow T κ` is power-asymptotic to exponent `κ`. -/ +theorem isPowerAsymptotic_floorRpow + {T : VariableObject ℝ} {κ : ℝ} (hκ : 0 < κ) + (hT : ∀ i, 1 ≤ T i) (hTunbounded : T.IsUnbounded) : + IsPowerAsymptotic (fun i ↦ (floorRpow T κ i : ℝ)) T κ := by + have hTtop : Tendsto T atTop atTop := + (VariableObject.isUnbounded_iff_tendsto_atTop + (fun i ↦ zero_le_one.trans (hT i))).mp hTunbounded + have hratio := tendsto_floorRpow_cast_div_rpow_one hκ hTtop + have hTgt : ∀ᶠ i in atTop, 1 < T i := hTtop.eventually (eventually_gt_atTop 1) + have hqpos : ∀ᶠ i in atTop, 0 < (floorRpow T κ i : ℝ) := + Filter.Eventually.of_forall fun i ↦ by exact_mod_cast floorRpow_pos T κ i + apply isPowerAsymptotic_of_logb_tendsto hTgt hqpos + have hlogratio : Tendsto (fun i ↦ + Real.log ((floorRpow T κ i : ℝ) / T i ^ κ)) atTop (𝓝 0) := by + simpa [Function.comp_def] using + (Real.continuousAt_log one_ne_zero).tendsto.comp hratio + have hlogTtop := Real.tendsto_log_atTop.comp hTtop + have hsmall := hlogratio.div_atTop hlogTtop + have hlimit : Tendsto (fun i ↦ κ + + Real.log ((floorRpow T κ i : ℝ) / T i ^ κ) / (Real.log ∘ T) i) + atTop (𝓝 κ) := by + simpa using (tendsto_const_nhds : Tendsto (fun _ : ℕ ↦ κ) atTop (𝓝 κ)).add hsmall + apply hlimit.congr' + filter_upwards [hTgt] with i hi + rw [Real.logb] + have hTi : 0 < T i := zero_lt_one.trans hi + have hqi : 0 < (floorRpow T κ i : ℝ) := by exact_mod_cast floorRpow_pos T κ i + rw [Real.log_div hqi.ne' (Real.rpow_pos_of_pos hTi κ).ne', Real.log_rpow hTi] + dsimp only [Function.comp_apply] + field_simp [(Real.log_pos hi).ne'] + ring + +/-! ## Power bounds -/ + +/-- Strictly increasing a fixed exponent makes a real power little-o along a base tending to +infinity. -/ +theorem isLittleO_rpow_comp_tendsto_of_lt + {T : VariableObject ℝ} {β γ : ℝ} + (hT : Tendsto T atTop atTop) (hβγ : β < γ) : + (fun i ↦ T i ^ β) =o[atTop] (fun i ↦ T i ^ γ) := by + have hzero : ∀ᶠ i in atTop, T i ^ γ = 0 → T i ^ β = 0 := by + filter_upwards [hT.eventually (eventually_gt_atTop 0)] with i hi + exact fun hzero ↦ ((Real.rpow_pos_of_pos hi γ).ne' hzero).elim + rw [Asymptotics.isLittleO_iff_tendsto' hzero] + have hlimit := (tendsto_rpow_neg_atTop (sub_pos.mpr hβγ)).comp hT + apply hlimit.congr' + filter_upwards [hT.eventually (eventually_gt_atTop 0)] with i hi + change T i ^ (-(γ - β)) = T i ^ β / T i ^ γ + rw [← Real.rpow_sub hi] + congr 1 + ring + +/-- If `T` is at least one and unbounded, then `X ≪ T ^ (β + o(1))` iff +`X = O(T ^ (β + ε))` for every fixed `ε > 0`. -/ +theorem isPowerBounded_iff_forall_pos + {E : Type*} [SeminormedAddCommGroup E] + (X : VariableObject E) (T : VariableObject ℝ) (β : ℝ) + (hT : ∀ i, 1 ≤ T i) (hTunbounded : T.IsUnbounded) : + IsPowerBounded X T β ↔ + ∀ ε : ℝ, 0 < ε → + Asymptotics.IsBigO atTop X (fun i ↦ T i ^ (β + ε)) := by + have hTtop : Tendsto T atTop atTop := + (VariableObject.isUnbounded_iff_tendsto_atTop + fun i ↦ zero_le_one.trans (hT i)).1 hTunbounded + have hTgt : ∀ᶠ i in atTop, 1 < T i := + (tendsto_atTop.1 hTtop 2).mono fun _ hi ↦ by linarith + constructor + · rintro ⟨exponent, hexponent, hX⟩ ε hε + refine hX.trans (Asymptotics.IsBigO.of_bound 1 ?_) + have hexponent_upper := + (isEqUpToInfinitesimal_iff_forall_pos + exponent (VariableObject.fixed β)).1 hexponent ε hε + filter_upwards [hexponent_upper] with i hi + rw [one_mul, Real.norm_eq_abs, + abs_of_nonneg (Real.rpow_nonneg (le_trans zero_le_one (hT i)) _), + Real.norm_eq_abs, + abs_of_nonneg (Real.rpow_nonneg (le_trans zero_le_one (hT i)) _)] + apply Real.rpow_le_rpow_of_exponent_le (hT i) + rw [Real.norm_eq_abs] at hi + linarith [le_abs_self (exponent i - β)] + · intro hX + let exponent : VariableObject ℝ := fun i ↦ + if ‖X i‖ = 0 then β else + max β (Real.log ‖X i‖ / Real.log (T i)) + refine ⟨exponent, ?_, Asymptotics.IsBigO.of_bound 1 ?_⟩ + · apply (isEqUpToInfinitesimal_iff_forall_pos + exponent (VariableObject.fixed β)).2 + intro δ hδ + have hδ3 : 0 < δ / 3 := by linarith + obtain ⟨C, hCpos, hC⟩ := (hX (δ / 3) hδ3).exists_pos + have hC' : ∀ᶠ i in atTop, + ‖X i‖ ≤ C * T i ^ (β + δ / 3) := hC.bound.mono fun i hi ↦ by + simpa only [Real.norm_eq_abs, + abs_of_nonneg (Real.rpow_nonneg (zero_le_one.trans (hT i)) _)] using hi + have hpowtop : Tendsto (fun i ↦ T i ^ (δ / 3)) atTop atTop := + (tendsto_rpow_atTop hδ3).comp hTtop + have hCpower : ∀ᶠ i in atTop, C ≤ T i ^ (δ / 3) := + tendsto_atTop.1 hpowtop C + filter_upwards [hTgt, hC', hCpower] with i hiT hiX hiC + by_cases hXi : ‖X i‖ = 0 + · simp [exponent, hXi, hδ] + · have hXpos : 0 < ‖X i‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hXi) + have hiTpos : 0 < T i := lt_trans zero_lt_one hiT + have hXpower : ‖X i‖ ≤ T i ^ (β + 2 * δ / 3) := by + calc + ‖X i‖ ≤ C * T i ^ (β + δ / 3) := hiX + _ ≤ T i ^ (δ / 3) * T i ^ (β + δ / 3) := by gcongr + _ = T i ^ (β + 2 * δ / 3) := by + rw [← Real.rpow_add hiTpos] + congr 1 + ring + have hratio : + Real.log ‖X i‖ / Real.log (T i) ≤ β + 2 * δ / 3 := by + apply (div_le_iff₀ (Real.log_pos hiT)).2 + exact (Real.le_rpow_iff_log_le hXpos hiTpos).1 hXpower + rw [Real.norm_eq_abs, abs_lt] + constructor + · simp only [exponent, hXi, ↓reduceIte, VariableObject.fixed] + linarith [le_max_left β + (Real.log ‖X i‖ / Real.log (T i))] + · simp only [exponent, hXi, ↓reduceIte, VariableObject.fixed] + have := max_lt (show β < β + δ by linarith) + (lt_of_le_of_lt hratio (show β + 2 * δ / 3 < β + δ by linarith)) + linarith + · filter_upwards [hTgt] with i hiT + rw [one_mul, Real.norm_eq_abs, + abs_of_nonneg (Real.rpow_nonneg (le_trans zero_le_one (hT i)) _)] + by_cases hXi : ‖X i‖ = 0 + · rw [hXi] + exact Real.rpow_nonneg (le_trans zero_le_one (hT i)) _ + · have hXpos : 0 < ‖X i‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hXi) + have hiTpos : 0 < T i := lt_trans zero_lt_one hiT + apply (Real.le_rpow_iff_log_le hXpos hiTpos).2 + apply (div_le_iff₀ (Real.log_pos hiT)).1 + simp only [exponent, hXi, ↓reduceIte] + exact le_max_right β (Real.log ‖X i‖ / Real.log (T i)) + +/-- Increasing the exponent preserves a power bound when the base is eventually at least one. -/ +theorem IsPowerBounded.mono + {E : Type*} [SeminormedAddCommGroup E] + {X : VariableObject E} {T : VariableObject ℝ} {β γ : ℝ} + (hX : IsPowerBounded X T β) (hT : ∀ᶠ i in atTop, 1 ≤ T i) + (hβγ : β ≤ γ) : + IsPowerBounded X T γ := by + obtain ⟨exponent, hexponent, hX⟩ := hX + let shiftedExponent : VariableObject ℝ := + fun i ↦ exponent i + (γ - β) + refine ⟨shiftedExponent, ?_, hX.trans (Asymptotics.IsBigO.of_bound 1 ?_)⟩ + · have hshift := hexponent.add + (IsEqUpToInfinitesimal.refl (VariableObject.fixed (γ - β))) + convert hshift using 1 + · ext i + dsimp [shiftedExponent] + · ext i + dsimp [shiftedExponent] + ring + filter_upwards [hT] with i hiT + have hT0 : 0 ≤ T i := zero_le_one.trans hiT + rw [one_mul, Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg hT0 _), + Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg hT0 _)] + exact Real.rpow_le_rpow_of_exponent_le hiT (by + dsimp [shiftedExponent] + linarith) + +/-- A power lower bound for an unbounded object forces its exponent to be no larger than any +admissible power-bound exponent. -/ +theorem exponent_le_of_isPowerBounded_of_eventually_norm_ge_rpow + {E : Type*} [SeminormedAddCommGroup E] + {X : VariableObject E} {T : VariableObject ℝ} {β γ c : ℝ} + (hT : ∀ i, 1 ≤ T i) (hTunbounded : T.IsUnbounded) + (hbound : IsPowerBounded X T β) (hc : 0 < c) + (hlower : ∀ᶠ i in atTop, c * T i ^ γ ≤ ‖X i‖) : + γ ≤ β := by + by_contra hγβ + have hβγ : β < γ := lt_of_not_ge hγβ + let ε := (γ - β) / 2 + have hε : 0 < ε := by dsimp [ε]; linarith + have hO := (isPowerBounded_iff_forall_pos X T β hT hTunbounded).1 hbound ε hε + have hTtop : Tendsto T atTop atTop := + (VariableObject.isUnbounded_iff_tendsto_atTop + fun i ↦ zero_le_one.trans (hT i)).1 hTunbounded + have hpowO : (fun i ↦ T i ^ γ) =O[atTop] X := by + apply Asymptotics.IsBigO.of_bound (1 / c) + filter_upwards [hlower] with i hi + rw [Real.norm_eq_abs, abs_of_nonneg + (Real.rpow_nonneg (zero_le_one.trans (hT i)) _)] + calc + T i ^ γ ≤ ‖X i‖ / c := (le_div_iff₀ hc).2 (by simpa [mul_comm] using hi) + _ = 1 / c * ‖X i‖ := by ring + have hsmall : (fun i ↦ T i ^ (β + ε)) =o[atTop] (fun i ↦ T i ^ γ) := + isLittleO_rpow_comp_tendsto_of_lt hTtop (by dsimp [ε]; linarith) + have hnonzero : ∃ᶠ i in atTop, T i ^ (β + ε) ≠ 0 := + (Filter.Eventually.of_forall fun i ↦ + (Real.rpow_pos_of_pos (zero_lt_one.trans_le (hT i)) _).ne').frequently + exact hsmall.not_isBigO hnonzero (hpowO.trans hO) + +end Expdb diff --git a/Expdb/ExponentialSums/ExponentSumGrowth.lean b/Expdb/ExponentialSums/ExponentSumGrowth.lean index d5beeaa..60c9a0e 100644 --- a/Expdb/ExponentialSums/ExponentSumGrowth.lean +++ b/Expdb/ExponentialSums/ExponentSumGrowth.lean @@ -1,13 +1,10 @@ module +public import Expdb.Basic.PowerAsymptotics public import Expdb.ExponentialSums.LogPhase -public import Mathlib.Analysis.Asymptotics.Defs -public import Mathlib.Analysis.SpecialFunctions.Log.Base +public import Expdb.ExponentialSums.FixedExponentialSum public import Mathlib.Order.Interval.Finset.Nat -import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics -import Mathlib.Analysis.Asymptotics.Lemmas - /-! # Exponential sum growth exponents @@ -31,22 +28,7 @@ noncomputable section namespace Expdb -/-! ## Asymptotic definition -/ - -/-- `N = T ^ (α + o(1))`, expressed using a variable exponent that is equal to `α` up to an -infinitesimal. -/ -def IsPowerAsymptotic (N T : VariableObject ℝ) (α : ℝ) : Prop := - ∃ exponent : VariableObject ℝ, - exponent =o VariableObject.fixed α ∧ - ∀ᶠ i in atTop, N i = T i ^ exponent i - -/-- `X ≪ T ^ (β + o(1))`, expressed using a variable exponent that is equal to `β` up to -an infinitesimal. -/ -def IsPowerBounded {E : Type*} [SeminormedAddCommGroup E] - (X : VariableObject E) (T : VariableObject ℝ) (β : ℝ) : Prop := - ∃ exponent : VariableObject ℝ, - exponent =o VariableObject.fixed β ∧ - Asymptotics.IsBigO atTop X (fun i ↦ T i ^ exponent i) +/-! ## Exponential-sum growth definition -/ /-- The variable exponential sum `∑ n ∈ [a, b], e(T F(n / N))`. -/ @@ -54,9 +36,13 @@ def exponentialSum (F : VariableFunction (VariableObject.fixed ℝ) ℝ) (T N : VariableObject ℝ) (a b : VariableObject ℕ) : VariableObject ℂ := - fun i ↦ - ∑ n ∈ Finset.Icc (a i) (b i), - (𝐞 (T i * F i ((n : ℝ) / N i)) : ℂ) + fun i ↦ exponentialSumAt (F i) (T i) (N i) (a i) (b i) + +@[simp] theorem exponentialSum_apply + (F : VariableFunction (VariableObject.fixed ℝ) ℝ) + (T N : VariableObject ℝ) (a b : VariableObject ℕ) (i : ℕ) : + exponentialSum F T N a b i = exponentialSumAt (F i) (T i) (N i) (a i) (b i) := + rfl /-- The assertion that `β` is an admissible exponential-sum growth exponent at scale `α`. -/ def IsExponentSumBound (α : ℝ≥0) (β : ℝ) : Prop := @@ -71,306 +57,17 @@ def IsExponentSumBound (α : ℝ≥0) (β : ℝ) : Prop := (∀ i, N i ≤ (a i : ℝ) ∧ (b i : ℝ) ≤ 2 * N i) → IsPowerBounded (exponentialSum F T N a b) T β +/-- The set of admissible exponential-sum growth exponents at scale `α`. -/ +def exponentSumBounds (α : ℝ≥0) : Set ℝ := + {β : ℝ | IsExponentSumBound α β} + +@[simp] theorem mem_exponentSumBounds {α : ℝ≥0} {β : ℝ} : + β ∈ exponentSumBounds α ↔ IsExponentSumBound α β := + Iff.rfl + /-- The exponential sum growth exponent `β(α)` from the blueprint definition `beta-def`. -/ def exponentSumGrowthExponent (α : ℝ≥0) : ℝ := - sInf {β : ℝ | IsExponentSumBound α β} - -/-! ## Power asymptotics -/ - -/-- If `N = T ^ (α + o(1))`, then `N` eventually lies between the powers with exponents -`α - ε` and `α + ε`. -/ -theorem IsPowerAsymptotic.eventually_between - {N T : VariableObject ℝ} {α ε : ℝ} - (hNT : IsPowerAsymptotic N T α) - (hT : ∀ᶠ i in atTop, 1 ≤ T i) - (hε : 0 < ε) : - ∀ᶠ i in atTop, T i ^ (α - ε) ≤ N i ∧ N i ≤ T i ^ (α + ε) := by - obtain ⟨exponent, hexponent, hN⟩ := hNT - obtain ⟨hexponent_le, halpha_le⟩ := - (isEqUpToInfinitesimal_iff_leUpToInfinitesimal - exponent (VariableObject.fixed α)).1 hexponent - have hupper := (isLEUpToInfinitesimal_iff_forall_pos - exponent (VariableObject.fixed α)).1 hexponent_le ε hε - have hlower := (isLEUpToInfinitesimal_iff_forall_pos - (VariableObject.fixed α) exponent).1 halpha_le ε hε - filter_upwards [hT, hN, hupper, hlower] with i hiT hiN hiupper hilower - rw [hiN] - exact - ⟨Real.rpow_le_rpow_of_exponent_le hiT (by linarith), - Real.rpow_le_rpow_of_exponent_le hiT (by linarith)⟩ - -/-- Convergence of the logarithmic exponent gives a power asymptotic. -/ -theorem isPowerAsymptotic_of_logb_tendsto - {N T : VariableObject ℝ} {α : ℝ} - (hT : ∀ᶠ i in atTop, 1 < T i) (hN : ∀ᶠ i in atTop, 0 < N i) - (hexponent : Tendsto (fun i ↦ Real.logb (T i) (N i)) atTop (nhds α)) : - IsPowerAsymptotic N T α := by - let exponent : VariableObject ℝ := fun i ↦ Real.logb (T i) (N i) - refine ⟨exponent, ?_, ?_⟩ - · rw [IsEqUpToInfinitesimal, VariableObject.IsInfinitesimal] - have hsub : Tendsto (fun i ↦ Real.logb (T i) (N i) - α) atTop (nhds 0) := by - simpa using hexponent.sub - (tendsto_const_nhds : Tendsto (fun _ : ℕ ↦ α) atTop (nhds α)) - convert (continuous_norm.tendsto 0).comp hsub using 1 <;> - simp [Function.comp_def, exponent, VariableObject.fixed] - · filter_upwards [hT, hN] with i hiT hiN - exact (Real.rpow_logb (zero_lt_one.trans hiT) hiT.ne' hiN).symm - -/-- A variable power sandwich with an infinitesimal error determines a power asymptotic. -/ -theorem isPowerAsymptotic_of_between - {N T δ : VariableObject ℝ} {α : ℝ} - (hT : ∀ i, 1 < T i) (hN : ∀ i, 0 < N i) - (hδnonneg : ∀ i, 0 ≤ δ i) (hδ : δ.IsInfinitesimal) - (hbetween : ∀ i, - T i ^ (α - δ i) ≤ N i ∧ N i ≤ T i ^ (α + δ i)) : - IsPowerAsymptotic N T α := by - let exponent : VariableObject ℝ := fun i ↦ Real.logb (T i) (N i) - refine ⟨exponent, ?_, Filter.Eventually.of_forall fun i ↦ ?_⟩ - · apply (isEqUpToInfinitesimal_iff_forall_pos - exponent (VariableObject.fixed α)).2 - intro ε hε - have hδsmall := - (VariableObject.isInfinitesimal_iff_forall_pos δ).1 hδ ε hε - filter_upwards [hδsmall] with i hi - have hlower : α - δ i ≤ exponent i := - (Real.le_logb_iff_rpow_le (hT i) (hN i)).2 (hbetween i).1 - have hupper : exponent i ≤ α + δ i := - (Real.logb_le_iff_le_rpow (hT i) (hN i)).2 (hbetween i).2 - rw [Real.norm_eq_abs, abs_lt] - rw [Real.norm_eq_abs, abs_of_nonneg (hδnonneg i)] at hi - constructor <;> dsimp [exponent, VariableObject.fixed] at * <;> linarith - · exact (Real.rpow_logb (lt_trans zero_lt_one (hT i)) - (hT i).ne' (hN i)).symm - -/-- If `T` lies between fixed positive multiples of `N ^ α⁻¹`, then the logarithm of `N` to -base `T` tends to `α`. -/ -private lemma tendsto_logb_of_between_const_rpow - {N T : VariableObject ℝ} {α A B : ℝ} - (hα : 0 < α) (hA : 0 < A) (hB : 0 < B) - (hNtop : Tendsto N atTop atTop) - (hT : ∀ᶠ i in atTop, A * N i ^ α⁻¹ ≤ T i ∧ T i ≤ B * N i ^ α⁻¹) : - Tendsto (fun i ↦ Real.logb (T i) (N i)) atTop (nhds α) := by - have hlogNtop : Tendsto (fun i ↦ Real.log (N i)) atTop atTop := - Real.tendsto_log_atTop.comp hNtop - have hNgt : ∀ᶠ i in atTop, 1 < N i := hNtop.eventually (eventually_gt_atTop 1) - have hlogNpos : ∀ᶠ i in atTop, 0 < Real.log (N i) := by - filter_upwards [hNgt] with i hi - exact Real.log_pos hi - have hpowtop : Tendsto (fun i ↦ N i ^ α⁻¹) atTop atTop := - (tendsto_rpow_atTop (inv_pos.mpr hα)).comp hNtop - have hpowlarge : ∀ᶠ i in atTop, 1 / A < N i ^ α⁻¹ := - hpowtop.eventually (eventually_gt_atTop (1 / A)) - have hTgt : ∀ᶠ i in atTop, 1 < T i := by - filter_upwards [hpowlarge, hT] with i hi hTi - have : 1 < A * N i ^ α⁻¹ := by - simpa [mul_comm] using (div_lt_iff₀ hA).1 hi - exact this.trans_le hTi.1 - have hratio : Tendsto (fun i ↦ Real.log (T i) / Real.log (N i)) atTop (nhds α⁻¹) := by - have hlowerLimit : Tendsto - (fun i ↦ Real.log A / Real.log (N i) + α⁻¹) atTop (nhds α⁻¹) := by - simpa using (tendsto_const_nhds.div_atTop hlogNtop).add - (tendsto_const_nhds : Tendsto (fun _ : ℕ ↦ α⁻¹) atTop (nhds α⁻¹)) - have hupperLimit : Tendsto - (fun i ↦ Real.log B / Real.log (N i) + α⁻¹) atTop (nhds α⁻¹) := by - simpa using (tendsto_const_nhds.div_atTop hlogNtop).add - (tendsto_const_nhds : Tendsto (fun _ : ℕ ↦ α⁻¹) atTop (nhds α⁻¹)) - apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hlowerLimit hupperLimit - · filter_upwards [hNgt, hlogNpos, hT] with i hNi hlogNi hTi - have hbase : 0 < N i := zero_lt_one.trans hNi - have hlower := Real.log_le_log (mul_pos hA (Real.rpow_pos_of_pos hbase _)) hTi.1 - rw [Real.log_mul hA.ne' (Real.rpow_pos_of_pos hbase _).ne', - Real.log_rpow hbase] at hlower - apply (le_div_iff₀ hlogNi).2 - rw [add_mul, div_mul_cancel₀ _ hlogNi.ne'] - simpa [mul_comm] using hlower - · filter_upwards [hNgt, hlogNpos, hT] with i hNi hlogNi hTi - have hbase : 0 < N i := zero_lt_one.trans hNi - have hupper := Real.log_le_log (lt_of_lt_of_le - (mul_pos hA (Real.rpow_pos_of_pos hbase _)) hTi.1) hTi.2 - rw [Real.log_mul hB.ne' (Real.rpow_pos_of_pos hbase _).ne', - Real.log_rpow hbase] at hupper - apply (div_le_iff₀ hlogNi).2 - rw [add_mul, div_mul_cancel₀ _ hlogNi.ne'] - simpa [mul_comm] using hupper - have hinv := hratio.inv₀ (inv_ne_zero hα.ne') - have hinv' : Tendsto (fun i ↦ Real.logb (T i) (N i)) atTop (nhds α⁻¹⁻¹) := - hinv.congr' <| by - filter_upwards [hlogNpos, hTgt] with i hlogNi hTi - dsimp [Real.logb] - field_simp [hlogNi.ne', (Real.log_pos hTi).ne'] - simpa using hinv' - -/-- Fixed positive multiplicative uncertainty in `T = N ^ α⁻¹` does not affect the -power asymptotic `N = T ^ (α + o(1))`. -/ -theorem isPowerAsymptotic_of_between_const_rpow - {N T : VariableObject ℝ} {α A B : ℝ} - (hα : 0 < α) (hA : 0 < A) (hB : 0 < B) - (hNtop : Tendsto N atTop atTop) - (hT : ∀ᶠ i in atTop, A * N i ^ α⁻¹ ≤ T i ∧ T i ≤ B * N i ^ α⁻¹) : - IsPowerAsymptotic N T α := by - have hNpos : ∀ᶠ i in atTop, 0 < N i := - hNtop.eventually (eventually_gt_atTop 0) - have hpowtop : Tendsto (fun i ↦ N i ^ α⁻¹) atTop atTop := - (tendsto_rpow_atTop (inv_pos.mpr hα)).comp hNtop - have hpowlarge : ∀ᶠ i in atTop, 1 / A < N i ^ α⁻¹ := - hpowtop.eventually (eventually_gt_atTop (1 / A)) - have hTgt : ∀ᶠ i in atTop, 1 < T i := by - filter_upwards [hpowlarge, hT] with i hi hTi - have : 1 < A * N i ^ α⁻¹ := by - simpa [mul_comm] using (div_lt_iff₀ hA).1 hi - exact this.trans_le hTi.1 - exact isPowerAsymptotic_of_logb_tendsto hTgt - hNpos (tendsto_logb_of_between_const_rpow hα hA hB hNtop hT) - -/-! ## Power bounds -/ - -private lemma isLittleO_rpow_comp_tendsto_of_lt - {T : VariableObject ℝ} {β γ : ℝ} - (hT : Tendsto T atTop atTop) (hβγ : β < γ) : - (fun i ↦ T i ^ β) =o[atTop] (fun i ↦ T i ^ γ) := by - have hzero : ∀ᶠ i in atTop, T i ^ γ = 0 → T i ^ β = 0 := by - filter_upwards [hT.eventually (eventually_gt_atTop 0)] with i hi - exact fun hzero ↦ ((Real.rpow_pos_of_pos hi γ).ne' hzero).elim - rw [Asymptotics.isLittleO_iff_tendsto' hzero] - have hlimit := (tendsto_rpow_neg_atTop (sub_pos.mpr hβγ)).comp hT - apply hlimit.congr' - filter_upwards [hT.eventually (eventually_gt_atTop 0)] with i hi - change T i ^ (-(γ - β)) = T i ^ β / T i ^ γ - rw [← Real.rpow_sub hi] - congr 1 - ring - -/-- If `T` is at least one and unbounded, then `X ≪ T ^ (β + o(1))` iff -`X = O(T ^ (β + ε))` for every fixed `ε > 0`. -/ -theorem isPowerBounded_iff_forall_pos - {E : Type*} [SeminormedAddCommGroup E] - (X : VariableObject E) (T : VariableObject ℝ) (β : ℝ) - (hT : ∀ i, 1 ≤ T i) (hTunbounded : T.IsUnbounded) : - IsPowerBounded X T β ↔ - ∀ ε : ℝ, 0 < ε → - Asymptotics.IsBigO atTop X (fun i ↦ T i ^ (β + ε)) := by - -- Positivity and unboundedness make powers of `T` eventually monotone in the exponent. - have hTtop : Tendsto T atTop atTop := by - rw [VariableObject.IsUnbounded] at hTunbounded - exact hTunbounded.congr' <| Filter.Eventually.of_forall fun i ↦ by - rw [Real.norm_eq_abs, abs_of_nonneg (le_trans zero_le_one (hT i))] - have hTgt : ∀ᶠ i in atTop, 1 < T i := - (tendsto_atTop.1 hTtop 2).mono fun _ hi ↦ by linarith - constructor - -- An infinitesimal exponent error is eventually smaller than each fixed `ε`. - · rintro ⟨exponent, hexponent, hX⟩ ε hε - refine hX.trans (Asymptotics.IsBigO.of_bound 1 ?_) - have hexponent_upper := - (isEqUpToInfinitesimal_iff_forall_pos - exponent (VariableObject.fixed β)).1 hexponent ε hε - filter_upwards [hexponent_upper] with i hi - rw [one_mul, Real.norm_eq_abs, - abs_of_nonneg (Real.rpow_nonneg (le_trans zero_le_one (hT i)) _), - Real.norm_eq_abs, - abs_of_nonneg (Real.rpow_nonneg (le_trans zero_le_one (hT i)) _)] - apply Real.rpow_le_rpow_of_exponent_le (hT i) - rw [Real.norm_eq_abs] at hi - linarith [le_abs_self (exponent i - β)] - -- Conversely, choose the smallest pointwise exponent that bounds `‖X i‖`. - · intro hX - let exponent : VariableObject ℝ := fun i ↦ - if ‖X i‖ = 0 then β else - max β (Real.log ‖X i‖ / Real.log (T i)) - refine ⟨exponent, ?_, Asymptotics.IsBigO.of_bound 1 ?_⟩ - · apply (isEqUpToInfinitesimal_iff_forall_pos - exponent (VariableObject.fixed β)).2 - intro δ hδ - have hδ3 : 0 < δ / 3 := by linarith - obtain ⟨C, hC⟩ := (hX (δ / 3) hδ3).bound - let D : ℝ := max C 1 - have hDpos : 0 < D := lt_of_lt_of_le zero_lt_one (le_max_right C 1) - have hC' : ∀ᶠ i in atTop, - ‖X i‖ ≤ D * T i ^ (β + δ / 3) := hC.mono fun i hi ↦ by - calc - ‖X i‖ ≤ C * ‖T i ^ (β + δ / 3)‖ := hi - _ ≤ D * ‖T i ^ (β + δ / 3)‖ := by - gcongr - exact le_max_left C 1 - _ = D * T i ^ (β + δ / 3) := by - rw [Real.norm_eq_abs, - abs_of_nonneg (Real.rpow_nonneg - (le_trans zero_le_one (hT i)) _)] - have hpowtop : Tendsto (fun i ↦ T i ^ (δ / 3)) atTop atTop := - (tendsto_rpow_atTop hδ3).comp hTtop - have hD : ∀ᶠ i in atTop, D ≤ T i ^ (δ / 3) := - tendsto_atTop.1 hpowtop D - filter_upwards [hTgt, hC', hD] with i hiT hiX hiD - by_cases hXi : ‖X i‖ = 0 - · simp [exponent, hXi, hδ] - · have hXpos : 0 < ‖X i‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hXi) - have hiTpos : 0 < T i := lt_trans zero_lt_one hiT - have hXpower : ‖X i‖ ≤ T i ^ (β + 2 * δ / 3) := by - calc - ‖X i‖ ≤ D * T i ^ (β + δ / 3) := hiX - _ ≤ T i ^ (δ / 3) * T i ^ (β + δ / 3) := by - gcongr - _ = T i ^ (β + 2 * δ / 3) := by - rw [← Real.rpow_add hiTpos] - congr 1 - ring - have hratio : - Real.log ‖X i‖ / Real.log (T i) ≤ β + 2 * δ / 3 := by - apply (div_le_iff₀ (Real.log_pos hiT)).2 - exact (Real.le_rpow_iff_log_le hXpos hiTpos).1 hXpower - rw [Real.norm_eq_abs, abs_lt] - constructor - · simp only [exponent, hXi, ↓reduceIte, VariableObject.fixed] - linarith [le_max_left β - (Real.log ‖X i‖ / Real.log (T i))] - · simp only [exponent, hXi, ↓reduceIte, VariableObject.fixed] - have := max_lt (show β < β + δ by linarith) - (lt_of_le_of_lt hratio (show β + 2 * δ / 3 < β + δ by linarith)) - linarith - · filter_upwards [hTgt] with i hiT - rw [one_mul, Real.norm_eq_abs, - abs_of_nonneg (Real.rpow_nonneg (le_trans zero_le_one (hT i)) _)] - by_cases hXi : ‖X i‖ = 0 - · rw [hXi] - exact Real.rpow_nonneg (le_trans zero_le_one (hT i)) _ - · have hXpos : 0 < ‖X i‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hXi) - have hiTpos : 0 < T i := lt_trans zero_lt_one hiT - apply (Real.le_rpow_iff_log_le hXpos hiTpos).2 - apply (div_le_iff₀ (Real.log_pos hiT)).1 - simp only [exponent, hXi, ↓reduceIte] - exact le_max_right β (Real.log ‖X i‖ / Real.log (T i)) - -/-- A power lower bound for an unbounded object forces its exponent to be no larger than any -admissible power-bound exponent. -/ -theorem exponent_le_of_isPowerBounded_of_eventually_norm_ge_rpow - {E : Type*} [SeminormedAddCommGroup E] - {X : VariableObject E} {T : VariableObject ℝ} {β γ c : ℝ} - (hT : ∀ i, 1 ≤ T i) (hTunbounded : T.IsUnbounded) - (hbound : IsPowerBounded X T β) (hc : 0 < c) - (hlower : ∀ᶠ i in atTop, c * T i ^ γ ≤ ‖X i‖) : - γ ≤ β := by - by_contra hγβ - have hβγ : β < γ := lt_of_not_ge hγβ - let ε := (γ - β) / 2 - have hε : 0 < ε := by dsimp [ε]; linarith - have hO := (isPowerBounded_iff_forall_pos X T β hT hTunbounded).1 hbound ε hε - have hTtop : Tendsto T atTop atTop := by - rw [VariableObject.IsUnbounded] at hTunbounded - exact hTunbounded.congr' <| Filter.Eventually.of_forall fun i ↦ by - rw [Real.norm_eq_abs, abs_of_nonneg (le_trans zero_le_one (hT i))] - have hpowO : (fun i ↦ T i ^ γ) =O[atTop] X := by - apply Asymptotics.IsBigO.of_bound (1 / c) - filter_upwards [hlower] with i hi - rw [Real.norm_eq_abs, abs_of_nonneg - (Real.rpow_nonneg (zero_le_one.trans (hT i)) _)] - calc - T i ^ γ ≤ ‖X i‖ / c := (le_div_iff₀ hc).2 (by simpa [mul_comm] using hi) - _ = 1 / c * ‖X i‖ := by ring - have hsmall : (fun i ↦ T i ^ (β + ε)) =o[atTop] (fun i ↦ T i ^ γ) := - isLittleO_rpow_comp_tendsto_of_lt hTtop (by dsimp [ε]; linarith) - have hnonzero : ∃ᶠ i in atTop, T i ^ (β + ε) ≠ 0 := - (Filter.Eventually.of_forall fun i ↦ - (Real.rpow_pos_of_pos (zero_lt_one.trans_le (hT i)) _).ne').frequently - exact hsmall.not_isBigO hnonzero (hpowO.trans hO) + sInf (exponentSumBounds α) /-! ## Admissible exponents @@ -378,38 +75,13 @@ The candidate set is upward closed, nonempty, and bounded below. ### Monotonicity -/ -private lemma isPowerBounded_mono - {X : VariableObject ℂ} {T : VariableObject ℝ} {β γ : ℝ} - (hT : ∀ i, 1 ≤ T i) (hβγ : β ≤ γ) - (hX : IsPowerBounded X T β) : - IsPowerBounded X T γ := by - obtain ⟨exponent, hexponent, hX⟩ := hX - let shiftedExponent : VariableObject ℝ := - fun i ↦ exponent i + (γ - β) - refine ⟨shiftedExponent, ?_, hX.trans (Asymptotics.IsBigO.of_bound 1 ?_)⟩ - · have hshift := hexponent.add - (IsEqUpToInfinitesimal.refl (VariableObject.fixed (γ - β))) - convert hshift using 1 - · ext i - dsimp [shiftedExponent] - · ext i - dsimp [shiftedExponent] - ring - exact Filter.Eventually.of_forall fun i ↦ by - have hT0 : 0 ≤ T i := le_trans zero_le_one (hT i) - rw [one_mul, Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg hT0 _), - Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg hT0 _)] - exact Real.rpow_le_rpow_of_exponent_le (hT i) (by - dsimp [shiftedExponent] - linarith) - /-- Admissible exponential-sum bounds are monotone in the exponent. -/ theorem IsExponentSumBound.mono {α : ℝ≥0} {β γ : ℝ} (hβ : IsExponentSumBound α β) (hβγ : β ≤ γ) : IsExponentSumBound α γ := by intro N T F a b hN hT hTunbounded hNT hF hab - exact isPowerBounded_mono hT hβγ - (hβ N T F a b hN hT hTunbounded hNT hF hab) + exact (hβ N T F a b hN hT hTunbounded hNT hF hab).mono + (Filter.Eventually.of_forall hT) hβγ /-! ### Nonemptiness and lower bound -/ @@ -421,10 +93,8 @@ private lemma norm_exponentialSum_le_three_mul (i : ℕ) : ‖exponentialSum F T N a b i‖ ≤ 3 * N i := by calc - ‖exponentialSum F T N a b i‖ ≤ - ∑ n ∈ Finset.Icc (a i) (b i), - ‖(𝐞 (T i * F i ((n : ℝ) / N i)) : ℂ)‖ := norm_sum_le _ _ - _ = ((Finset.Icc (a i) (b i)).card : ℝ) := by simp + ‖exponentialSum F T N a b i‖ ≤ ((Finset.Icc (a i) (b i)).card : ℝ) := + norm_exponentialSumAt_le_card _ _ _ _ _ _ ≤ (b i : ℝ) + 1 := by rw [Nat.card_Icc] exact_mod_cast Nat.sub_le _ _ @@ -446,15 +116,13 @@ theorem isExponentSumBound_self (α : ℝ≥0) : abs_of_nonneg (Real.rpow_nonneg (le_trans zero_le_one (hT i)) _)] private lemma exponentSumBounds_nonempty (α : ℝ≥0) : - {β : ℝ | IsExponentSumBound α β}.Nonempty := + (exponentSumBounds α).Nonempty := ⟨α, isExponentSumBound_self α⟩ /-- Every admissible exponent at a nonnegative scale is nonnegative. -/ theorem IsExponentSumBound.nonneg {α : ℝ≥0} {β : ℝ} (hβ : IsExponentSumBound α β) : 0 ≤ β := by - by_contra hβneg - have hβlt : β < 0 := lt_of_not_ge hβneg let T : VariableObject ℝ := fun i ↦ (i : ℝ) + 2 let N : VariableObject ℝ := fun i ↦ T i ^ (α : ℝ) let a : VariableObject ℕ := fun i ↦ ⌈N i⌉₊ @@ -463,49 +131,28 @@ theorem IsExponentSumBound.nonneg dsimp [T] have hi : (0 : ℝ) ≤ i := Nat.cast_nonneg i linarith - have hTtendsto : Tendsto T atTop atTop := by - exact tendsto_atTop_add_const_right atTop 2 tendsto_natCast_atTop_atTop have hTunbounded : T.IsUnbounded := by - rw [VariableObject.IsUnbounded] - convert hTtendsto using 1 - ext i - rw [Real.norm_eq_abs, abs_of_nonneg (le_trans zero_le_one (hT i))] + apply (VariableObject.isUnbounded_iff_tendsto_atTop + fun i ↦ zero_le_one.trans (hT i)).2 + exact tendsto_atTop_add_const_right atTop 2 tendsto_natCast_atTop_atTop have hN : ∀ i, 1 ≤ N i := fun i ↦ Real.one_le_rpow (hT i) α.property have hNT : IsPowerAsymptotic N T (α : ℝ) := by refine ⟨VariableObject.fixed (α : ℝ), IsEqUpToInfinitesimal.refl _, ?_⟩ exact Filter.Eventually.of_forall fun _ ↦ rfl have ha : ∀ i, N i ≤ (a i : ℝ) ∧ (a i : ℝ) ≤ 2 * N i := by intro i - have hN0 : 0 ≤ N i := le_trans zero_le_one (hN i) + have hN0 : 0 ≤ N i := zero_le_one.trans (hN i) refine ⟨Nat.le_ceil _, ?_⟩ exact (Nat.ceil_lt_add_one hN0).le.trans (by linarith [hN i]) - -- A singleton log-phase sum has norm one, so it cannot have negative power growth. have hbound := hβ N T logPhase a a hN hT hTunbounded hNT isModelPhaseFunction_log ha - have hO := (isPowerBounded_iff_forall_pos - (exponentialSum logPhase T N a a) T β hT hTunbounded).1 - hbound (-β / 2) (by linarith) - have hpower_tendsto : - Tendsto (fun i ↦ T i ^ (β + -β / 2)) atTop (𝓝 0) := by - have hneg : 0 < -(β + -β / 2) := by linarith - apply ((tendsto_rpow_neg_atTop hneg).comp hTtendsto).congr' - exact Filter.Eventually.of_forall fun i ↦ by - change T i ^ (- -(β + -β / 2)) = T i ^ (β + -β / 2) - rw [neg_neg] - have hsum_tendsto : - Tendsto (exponentialSum logPhase T N a a) atTop (𝓝 0) := - hO.trans_tendsto hpower_tendsto - have hsmall := (Metric.tendsto_nhds.1 hsum_tendsto) (1 / 2) (by norm_num) - obtain ⟨i, hi⟩ := hsmall.exists - have hnorm : - ‖exponentialSum logPhase T N a a i‖ = 1 := by - simp [exponentialSum] - rw [dist_zero_right, hnorm] at hi - norm_num at hi + apply exponent_le_of_isPowerBounded_of_eventually_norm_ge_rpow + hT hTunbounded hbound zero_lt_one + exact Filter.Eventually.of_forall fun i ↦ by simp private lemma exponentSumBounds_bddBelow {α : ℝ≥0} : - BddBelow {β : ℝ | IsExponentSumBound α β} := + BddBelow (exponentSumBounds α) := ⟨0, fun _ hβ ↦ hβ.nonneg⟩ /-! ## The least admissible exponent -/ @@ -514,7 +161,7 @@ private lemma exists_isExponentSumBound_lt_add (α : ℝ≥0) {ε : ℝ} (hε : 0 < ε) : ∃ β : ℝ, IsExponentSumBound α β ∧ β < exponentSumGrowthExponent α + ε := by - let S : Set ℝ := {β : ℝ | IsExponentSumBound α β} + let S : Set ℝ := exponentSumBounds α have hS : S.Nonempty := exponentSumBounds_nonempty α have hinf_lt : sInf S < sInf S + ε := by linarith obtain ⟨β, hβ, hβlt⟩ := exists_lt_of_csInf_lt hS hinf_lt @@ -555,21 +202,20 @@ theorem exponentSumGrowthExponent_le_iff {α : ℝ≥0} {β : ℝ} : /-- The exponent sum growth exponent is the least admissible exponent. -/ theorem isLeast_exponentSumGrowthExponent (α : ℝ≥0) : - IsLeast {β : ℝ | IsExponentSumBound α β} + IsLeast (exponentSumBounds α) (exponentSumGrowthExponent α) := ⟨isExponentSumBound_exponentSumGrowthExponent α, fun _ hβ ↦ exponentSumGrowthExponent_le_iff.mpr hβ⟩ /-- At scale `α`, the admissible exponents form the interval `[β(α), ∞)`. -/ theorem exponentSumBounds_eq_Ici (α : ℝ≥0) : - {β : ℝ | IsExponentSumBound α β} = - Set.Ici (exponentSumGrowthExponent α) := by + exponentSumBounds α = Set.Ici (exponentSumGrowthExponent α) := by ext β exact exponentSumGrowthExponent_le_iff.symm /-- The set of admissible exponential-sum exponents at scale `α` is closed. -/ theorem isClosed_exponentSumBounds (α : ℝ≥0) : - IsClosed {β : ℝ | IsExponentSumBound α β} := by + IsClosed (exponentSumBounds α) := by rw [exponentSumBounds_eq_Ici] exact isClosed_Ici @@ -590,4 +236,20 @@ theorem isPowerBounded_logPhase isExponentSumBound_exponentSumGrowthExponent α N T logPhase a b hN hT hTunbounded hNT isModelPhaseFunction_log hab +/-- A lower bound of size `T ^ γ` for logarithmic-phase sums along an admissible family of +scales forces `γ ≤ β(α)`. -/ +theorem le_exponentSumGrowthExponent_of_logPhase_lower_bound + (α : ℝ≥0) + {N T : VariableObject ℝ} {a b : VariableObject ℕ} {c γ : ℝ} + (hN : ∀ i, 1 ≤ N i) + (hT : ∀ i, 1 ≤ T i) + (hTunbounded : T.IsUnbounded) + (hNT : IsPowerAsymptotic N T (α : ℝ)) + (hab : ∀ i, N i ≤ (a i : ℝ) ∧ (b i : ℝ) ≤ 2 * N i) + (hc : 0 < c) + (hlower : ∀ᶠ i in atTop, c * T i ^ γ ≤ ‖exponentialSum logPhase T N a b i‖) : + γ ≤ exponentSumGrowthExponent α := + exponent_le_of_isPowerBounded_of_eventually_norm_ge_rpow hT hTunbounded + (isPowerBounded_logPhase α hN hT hTunbounded hNT hab) hc hlower + end Expdb diff --git a/Expdb/ExponentialSums/ExponentSumGrowthNonAsymptotic.lean b/Expdb/ExponentialSums/ExponentSumGrowthNonAsymptotic.lean index 2b3bf6a..8dd80b6 100644 --- a/Expdb/ExponentialSums/ExponentSumGrowthNonAsymptotic.lean +++ b/Expdb/ExponentialSums/ExponentSumGrowthNonAsymptotic.lean @@ -3,7 +3,6 @@ module public import Expdb.ExponentialSums.ExponentSumGrowth import Expdb.Basic.AutomaticUniformity -import Mathlib.Analysis.Calculus.ContDiff.Bounds import Mathlib.Analysis.SpecialFunctions.Log.Base import Mathlib.Analysis.SpecialFunctions.Pow.Deriv @@ -26,20 +25,21 @@ namespace Expdb /-! ## Fixed-parameter formulation -/ -/-- The exponential sum at fixed parameters. -/ -def exponentialSumAt - (F : ℝ → ℝ) (T N : ℝ) (a b : ℕ) : ℂ := - ∑ n ∈ Finset.Icc a b, - (𝐞 (T * F ((n : ℝ) / N)) : ℂ) - -/-- A fixed phase function whose model-phase errors through order `P` are at most `δ`. -/ -def IsApproximateModelPhaseFunction - (F : ℝ → ℝ) (σ : ℝ) (P : ℕ) (δ : ℝ) : Prop := - ContDiffOn ℝ ∞ F phaseInterval ∧ - ∀ p : ℕ, p ≤ P → - ∀ u : phaseInterval, - ‖iteratedDerivWithin (p + 1) F phaseInterval u - - iteratedDerivWithin p (fun v : ℝ ↦ v ^ (-σ)) phaseInterval u‖ ≤ δ +/-- The fixed data satisfying the hypotheses of the non-asymptotic exponential-sum bound. -/ +structure IsModelPhaseSumSetupAt + (α σ δ : ℝ) (P : ℕ) (C T N : ℝ) (F : ℝ → ℝ) (a b : ℕ) : Prop where + /-- The phase parameter is above the uniform threshold. -/ + threshold_le_param : C ≤ T + /-- The scale is at least the lower power allowed by `δ`. -/ + rpow_sub_le_scale : T ^ (α - δ) ≤ N + /-- The scale is at most the upper power allowed by `δ`. -/ + scale_le_rpow_add : N ≤ T ^ (α + δ) + /-- The phase approximates the model phase through order `P`. -/ + isApproximateModelPhase : IsApproximateModelPhaseFunction F σ P δ + /-- The summation interval begins in the dyadic block. -/ + scale_le_start : N ≤ (a : ℝ) + /-- The summation interval ends in the dyadic block. -/ + end_le_two_mul_scale : (b : ℝ) ≤ 2 * N /-- The fixed-parameter epsilon--delta bound from the blueprint lemma `beta-asymp` (Non-asymptotic definition of `β`). -/ @@ -50,38 +50,9 @@ def IsExponentSumBoundNonAsymptotic (α : ℝ≥0) (β : ℝ) : Prop := ∃ P : ℕ, 1 ≤ P ∧ ∃ C : ℝ, 1 ≤ C ∧ ∀ (T N : ℝ) (F : ℝ → ℝ) (a b : ℕ), - C ≤ T → - T ^ ((α : ℝ) - δ) ≤ N → - N ≤ T ^ ((α : ℝ) + δ) → - IsApproximateModelPhaseFunction F σ P δ → - N ≤ (a : ℝ) → - (b : ℝ) ≤ 2 * N → + IsModelPhaseSumSetupAt (α : ℝ) σ δ P C T N F a b → ‖exponentialSumAt F T N a b‖ ≤ C * T ^ (β + ε) -/-! ## Uniform approximation by fixed phases -/ - -private lemma eventually_isApproximate_of_modelError - {F : VariableFunction (VariableObject.fixed ℝ) ℝ} {σ : ℝ} - (hphase : IsPhaseFunction F) - (herror : ∀ p : ℕ, (modelPhaseError F σ p).IsPointwiseInfinitesimal) - (P : ℕ) {δ : ℝ} (hδ : 0 < δ) : - ∀ᶠ i in atTop, IsApproximateModelPhaseFunction (F i) σ P δ := by - have hp : ∀ p ∈ Finset.range (P + 1), ∀ᶠ i in atTop, - ∀ u : phaseInterval, ‖modelPhaseError F σ p i u‖ < δ := - fun p _ ↦ - (VariableFunction.isPointwiseInfinitesimal_iff_forall_pos_uniform - (VariableObject.fixed phaseInterval) - (fun _ ↦ ⟨1, by simp [phaseInterval]⟩) - (modelPhaseError F σ p)).1 (herror p) δ hδ - have hall : - ∀ᶠ i in atTop, ∀ p ∈ Finset.range (P + 1), - ∀ u : phaseInterval, ‖modelPhaseError F σ p i u‖ < δ := - (Finset.range (P + 1)).eventually_all.mpr hp - filter_upwards [hall] with i hi - refine ⟨hphase i, ?_⟩ - intro p hp' u - exact (hi p (Finset.mem_range.mpr (by omega)) u).le - /-! ## From fixed bounds to asymptotic bounds -/ private lemma isExponentSumBound_of_nonAsymptotic @@ -105,13 +76,13 @@ private lemma isExponentSumBound_of_nonAsymptotic hNT.eventually_between (Filter.Eventually.of_forall hT) hδ have happrox := - eventually_isApproximate_of_modelError hphase herror P hδ + (IsModelPhaseFunctionWith.mk hphase herror).eventually_isApproximate P hδ refine Asymptotics.IsBigO.of_bound C ?_ filter_upwards [hTC, hNT', happrox] with i hiT hiNT hiF - simpa only [exponentialSum, exponentialSumAt, Real.norm_eq_abs, + simpa only [exponentialSum_apply, Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (le_trans zero_le_one (hT i)) _)] using hfixed (T i) (N i) (F i) (a i) (b i) - hiT hiNT.1 hiNT.2 hiF (hab i).1 (hab i).2 + ⟨hiT, hiNT.1, hiNT.2, hiF, (hab i).1, (hab i).2⟩ /-! ## Uniform bounds for approximate model phases -/ @@ -124,26 +95,13 @@ theorem approximate_model_phase_deriv_bounds ∀ {δ : ℝ} {F : ℝ → ℝ}, δ ≤ min ((2 : ℝ) ^ (-σ) / 2) 1 → IsApproximateModelPhaseFunction F σ P δ → - (∀ u ∈ phaseInterval, - (2 : ℝ) ^ (-σ) / 2 ≤ iteratedDerivWithin 1 F phaseInterval u) ∧ - (∀ k : ℕ, 1 ≤ k → k ≤ P + 1 → ∀ u ∈ phaseInterval, - ‖iteratedDerivWithin k F phaseInterval u‖ ≤ K) := by - have href : ContDiffOn ℝ ∞ (fun u : ℝ ↦ u ^ (-σ)) phaseInterval := by - intro u hu - exact (Real.contDiffAt_rpow_const_of_ne (by - exact ne_of_gt (lt_of_lt_of_le zero_lt_one hu.1))).contDiffWithinAt - have hreference (p : ℕ) : - ∃ B : ℝ, 0 ≤ B ∧ ∀ u : phaseInterval, - ‖iteratedDerivWithin p (fun v : ℝ ↦ v ^ (-σ)) phaseInterval u‖ ≤ B := by - have hcont : ContinuousOn - (iteratedDerivWithin p (fun v : ℝ ↦ v ^ (-σ)) phaseInterval) phaseInterval := - href.continuousOn_iteratedDerivWithin - (ENat.natCast_le_of_coe_top_le_withTop le_rfl p) - (uniqueDiffOn_Icc (by norm_num [phaseInterval])) - obtain ⟨B, hB⟩ := bddAbove_def.mp (isCompact_Icc.bddAbove_image hcont.norm) - refine ⟨max B 0, le_max_right _ _, fun u ↦ ?_⟩ - exact (hB _ ⟨u, u.property, rfl⟩).trans (le_max_left _ _) - choose B hBnonneg hB using hreference + HasPhaseFirstDerivLowerBound F ((2 : ℝ) ^ (-σ) / 2) ∧ + HasPhaseDerivBound F (P + 1) K := by + let B : ℕ → ℝ := fun p ↦ ‖(descPochhammer ℝ p).eval (-σ)‖ + have hBnonneg (p : ℕ) : 0 ≤ B p := norm_nonneg _ + have hB (p : ℕ) (u : phaseInterval) : + ‖iteratedDerivWithin p (modelPhase σ) phaseInterval u‖ ≤ B p := + norm_iteratedDerivWithin_modelPhase_le hσ.le p u.property let K : ℝ := 1 + ∑ p ∈ Finset.range (P + 1), B p have hK : 1 ≤ K := by dsimp [K] @@ -159,18 +117,19 @@ theorem approximate_model_phase_deriv_bounds Real.rpow_le_rpow_of_nonpos huPos hu.2 (neg_nonpos.mpr hσ.le) have he := hF.2 0 (Nat.zero_le P) ⟨u, hu⟩ rw [Real.norm_eq_abs, abs_le] at he - simp only [zero_add, iteratedDerivWithin_zero] at he + simp only [modelPhaseErrorAt, modelPhase, zero_add, iteratedDerivWithin_zero] at he linarith · intro k hk hkP u hu obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hk have hpP : p ≤ P := by omega have hpMem : p ∈ Finset.range (P + 1) := Finset.mem_range.mpr (by omega) have he := hF.2 p hpP ⟨u, hu⟩ + rw [modelPhaseErrorAt] at he have htriangle : ‖iteratedDerivWithin (p + 1) F phaseInterval u‖ ≤ ‖iteratedDerivWithin (p + 1) F phaseInterval u - - iteratedDerivWithin p (fun v : ℝ ↦ v ^ (-σ)) phaseInterval u‖ + - ‖iteratedDerivWithin p (fun v : ℝ ↦ v ^ (-σ)) phaseInterval u‖ := + iteratedDerivWithin p (modelPhase σ) phaseInterval u‖ + + ‖iteratedDerivWithin p (modelPhase σ) phaseInterval u‖ := norm_le_norm_sub_add _ _ calc ‖iteratedDerivWithin (1 + p) F phaseInterval u‖ ≤ 1 + B p := by @@ -185,7 +144,7 @@ theorem isApproximateModelPhaseFunction_log (P : ℕ) : IsApproximateModelPhaseFunction Real.log 1 P 0 := by refine ⟨isModelPhaseFunction_log.1 0, ?_⟩ intro p _ u - rw [iteratedDerivWithin_log_eq_rpow_neg_one, sub_self, norm_zero] + rw [modelPhaseErrorAt, iteratedDerivWithin_log_eq_rpow_neg_one, sub_self, norm_zero] /-! ## Building asymptotic counterexamples -/ @@ -194,12 +153,12 @@ private lemma isModelPhaseFunction_of_approximations {σ : ℝ} {P : VariableObject ℕ} {δ : VariableObject ℝ} (hσ : 0 < σ) (hP : ∀ p : ℕ, ∀ᶠ i in atTop, p ≤ P i) - (hδnonneg : ∀ i, 0 ≤ δ i) (hδ : δ.IsInfinitesimal) + (hδ : δ.IsInfinitesimal) (happrox : ∀ i, IsApproximateModelPhaseFunction (F i) σ (P i) (δ i)) : IsModelPhaseFunction F := by refine ⟨fun i ↦ (happrox i).1, σ, hσ, ?_⟩ intro p - apply (VariableFunction.isPointwiseInfinitesimal_iff_forall_pos_uniform + apply (VariableFunction.isChoicewiseInfinitesimal_iff_forall_pos_uniform (VariableObject.fixed phaseInterval) (fun _ ↦ ⟨1, by simp [phaseInterval]⟩) (modelPhaseError F σ p)).2 @@ -209,20 +168,8 @@ private lemma isModelPhaseFunction_of_approximations filter_upwards [hP p, hδsmall] with i hip hiδ intro u have herror := (happrox i).2 p hip u - rw [Real.norm_eq_abs, abs_of_nonneg (hδnonneg i)] at hiδ - exact lt_of_le_of_lt herror hiδ - -private lemma norm_exponentialSumAt_le_add_one - (F : ℝ → ℝ) (T N : ℝ) (a b : ℕ) : - ‖exponentialSumAt F T N a b‖ ≤ (b : ℝ) + 1 := by - calc - ‖exponentialSumAt F T N a b‖ ≤ - ∑ n ∈ Finset.Icc a b, - ‖(𝐞 (T * F ((n : ℝ) / N)) : ℂ)‖ := norm_sum_le _ _ - _ = ((Finset.Icc a b).card : ℝ) := by simp - _ ≤ (b : ℝ) + 1 := by - rw [Nat.card_Icc] - exact_mod_cast Nat.sub_le _ _ + rw [Real.norm_eq_abs] at hiδ + exact lt_of_le_of_lt herror ((le_abs_self (δ i)).trans_lt hiδ) private lemma nonAsymptotic_of_isExponentSumBound {α : ℝ≥0} {β : ℝ} (hbound : IsExponentSumBound α β) : @@ -245,22 +192,23 @@ private lemma nonAsymptotic_of_isExponentSumBound linarith choose T N F a b hdata using fun i ↦ hfailure (δ i) (hδpos i) (P i) (hPone i) (C i) (hCone i) - have hCT : ∀ i, C i ≤ T i := fun i ↦ (hdata i).1 + have hCT : ∀ i, C i ≤ T i := + fun i ↦ (hdata i).1.threshold_le_param have hlower : ∀ i, T i ^ ((α : ℝ) - δ i) ≤ N i := - fun i ↦ (hdata i).2.1 + fun i ↦ (hdata i).1.rpow_sub_le_scale have hupper : ∀ i, N i ≤ T i ^ ((α : ℝ) + δ i) := - fun i ↦ (hdata i).2.2.1 + fun i ↦ (hdata i).1.scale_le_rpow_add have happrox : ∀ i, IsApproximateModelPhaseFunction (F i) σ (P i) (δ i) := - fun i ↦ (hdata i).2.2.2.1 + fun i ↦ (hdata i).1.isApproximateModelPhase have ha : ∀ i, N i ≤ (a i : ℝ) := - fun i ↦ (hdata i).2.2.2.2.1 + fun i ↦ (hdata i).1.scale_le_start have hb : ∀ i, (b i : ℝ) ≤ 2 * N i := - fun i ↦ (hdata i).2.2.2.2.2.1 + fun i ↦ (hdata i).1.end_le_two_mul_scale have hviolate : ∀ i, C i * T i ^ (β + ε) < ‖exponentialSumAt (F i) (T i) (N i) (a i) (b i)‖ := - fun i ↦ (hdata i).2.2.2.2.2.2 + fun i ↦ (hdata i).2 have hTgt : ∀ i, 1 < T i := fun i ↦ by have hCthree : 3 ≤ C i := by dsimp [C] @@ -327,12 +275,12 @@ private lemma nonAsymptotic_of_isExponentSumBound mul_le_mul_of_nonneg_left hpow (le_trans (by norm_num) hCthree) linarith [hviolate i] have hNT : IsPowerAsymptotic N T (α : ℝ) := - isPowerAsymptotic_of_between hTgt hNpos - (fun i ↦ (hδpos i).le) hδinfinitesimal + isPowerAsymptotic_of_between_of_infinitesimal hTgt hNpos + hδinfinitesimal (fun i ↦ ⟨hlower i, hupper i⟩) have hF : IsModelPhaseFunction F := isModelPhaseFunction_of_approximations hσ hPtop - (fun i ↦ (hδpos i).le) hδinfinitesimal happrox + hδinfinitesimal happrox have hasymptotic := hbound N T F a b hNone hTone hTunbounded hNT hF (fun i ↦ ⟨ha i, hb i⟩) @@ -354,7 +302,7 @@ private lemma nonAsymptotic_of_isExponentSumBound have hnorm : ‖exponentialSumAt (F i) (T i) (N i) (a i) (b i)‖ ≤ K * T i ^ (β + ε / 2) := by - simpa only [exponentialSum, exponentialSumAt, Real.norm_eq_abs, + simpa only [exponentialSum_apply, Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (le_trans zero_le_one (hTone i)) _)] using hiK have hdominated : ‖exponentialSumAt (F i) (T i) (N i) (a i) (b i)‖ ≤ diff --git a/Expdb/ExponentialSums/FixedExponentialSum.lean b/Expdb/ExponentialSums/FixedExponentialSum.lean new file mode 100644 index 0000000..8cee21c --- /dev/null +++ b/Expdb/ExponentialSums/FixedExponentialSum.lean @@ -0,0 +1,69 @@ +module + +public import Expdb.ExponentialSums.PhaseFunctions +public import Mathlib.Algebra.Order.BigOperators.Group.Finset +public import Mathlib.Analysis.Calculus.ContDiff.Defs +public import Mathlib.Order.Interval.Finset.Nat + +/-! +# Fixed-parameter exponential sums + +Defines the oscillatory factor `e(T F(x / N))`, the corresponding finite +exponential sum, and basic estimates used by the project's analytic and +asymptotic results. It also packages the scale conditions required for +Euler–Maclaurin estimates. +-/ + +@[expose] public section + +open scoped ContDiff FourierTransform + +noncomputable section + +namespace Expdb + +/-- The oscillatory factor `x ↦ e(T F(x / N))`. -/ +def oscillatory (F : ℝ → ℝ) (T N : ℝ) (x : ℝ) : ℂ := + 𝐞 (T * F (x / N)) + +@[simp] theorem norm_oscillatory (F : ℝ → ℝ) (T N x : ℝ) : + ‖oscillatory F T N x‖ = 1 := by + simp [oscillatory] + +/-- The exponential sum `∑ n ∈ [a, b], e(T F(n / N))` at fixed parameters. -/ +def exponentialSumAt (F : ℝ → ℝ) (T N : ℝ) (a b : ℕ) : ℂ := + ∑ n ∈ Finset.Icc a b, oscillatory F T N n + +/-- An exponential sum has at most as many unit-sized terms as its summation range. -/ +theorem norm_exponentialSumAt_le_card (F : ℝ → ℝ) (T N : ℝ) (a b : ℕ) : + ‖exponentialSumAt F T N a b‖ ≤ ((Finset.Icc a b).card : ℝ) := by + simpa [exponentialSumAt] using norm_sum_le (Finset.Icc a b) fun n ↦ oscillatory F T N n + +/-- Bounding the cardinality by the upper endpoint gives a convenient endpoint-only estimate. -/ +theorem norm_exponentialSumAt_le_add_one (F : ℝ → ℝ) (T N : ℝ) (a b : ℕ) : + ‖exponentialSumAt F T N a b‖ ≤ (b : ℝ) + 1 := by + calc + ‖exponentialSumAt F T N a b‖ ≤ ((Finset.Icc a b).card : ℝ) := + norm_exponentialSumAt_le_card _ _ _ _ _ + _ ≤ (b : ℝ) + 1 := by + rw [Nat.card_Icc] + exact_mod_cast Nat.sub_le _ _ + +@[simp] theorem exponentialSumAt_self (F : ℝ → ℝ) (T N : ℝ) (a : ℕ) : + exponentialSumAt F T N a a = oscillatory F T N a := by + simp [exponentialSumAt] + +theorem exponentialSumAt_of_lt {a b : ℕ} (hab : b < a) (F : ℝ → ℝ) (T N : ℝ) : + exponentialSumAt F T N a b = 0 := by + simp [exponentialSumAt, Finset.Icc_eq_empty (by omega : ¬ a ≤ b)] + +/-- The scale conditions making the Euler–Maclaurin remainder of order `s` negligible. -/ +structure HasSmallEulerMaclaurinRemainder (s : ℕ) (T N K : ℝ) : Prop where + /-- The normalized phase derivative is at most one. -/ + ratio_le_one : K * T / N ≤ 1 + /-- The full remainder of order `s` is at most one. -/ + remainder_le_one : N * (K * T / N) ^ (s + 1) ≤ 1 + +end Expdb + +end diff --git a/Expdb/ExponentialSums/LogPhase.lean b/Expdb/ExponentialSums/LogPhase.lean index 97c68aa..331334b 100644 --- a/Expdb/ExponentialSums/LogPhase.lean +++ b/Expdb/ExponentialSums/LogPhase.lean @@ -6,8 +6,8 @@ public import Mathlib.Order.Interval.Finset.Nat import Mathlib.Analysis.Fourier.FourierTransformDeriv import Mathlib.Analysis.Real.Pi.Bounds +import Mathlib.Analysis.SpecialFunctions.Integrals.Basic import Mathlib.Analysis.SpecialFunctions.Pow.Deriv -import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts /-! # The logarithmic phase @@ -34,8 +34,9 @@ model exponent one. -/ theorem iteratedDerivWithin_log_eq_rpow_neg_one (p : ℕ) (u : phaseInterval) : iteratedDerivWithin (p + 1) Real.log phaseInterval u = - iteratedDerivWithin p (fun v : ℝ ↦ v ^ (-(1 : ℝ))) phaseInterval u := by + iteratedDerivWithin p (modelPhase 1) phaseInterval u := by have hu_pos : 0 < (u : ℝ) := lt_of_lt_of_le zero_lt_one u.property.1 + rw [show modelPhase 1 = fun v : ℝ ↦ v ^ (-(1 : ℝ)) from rfl] have hunique : UniqueDiffOn ℝ phaseInterval := uniqueDiffOn_Icc (by norm_num [phaseInterval]) rw [iteratedDerivWithin_eq_iteratedDeriv hunique @@ -58,8 +59,8 @@ theorem isModelPhaseFunction_log : IsModelPhaseFunction logPhase := by exact ne_of_gt (lt_of_lt_of_le zero_lt_one hu.1) · intro p u rw [VariableObject.IsInfinitesimal] - simp only [modelPhaseError, logPhase, iteratedDerivWithin_log_eq_rpow_neg_one, sub_self, - norm_zero] + simp only [modelPhaseError_apply, modelPhaseErrorAt, logPhase, + iteratedDerivWithin_log_eq_rpow_neg_one, sub_self, norm_zero] exact tendsto_const_nhds /-- On a dyadic interval, `log (n / N)` is `1 / (2 * N)`-separated. -/ @@ -117,64 +118,43 @@ theorem logPhase_integral_eq_mainTerm {N T : ℝ} (hN : 0 < N) : (∫ x in N..2 * N, (𝐞 (T * Real.log (x / N)) : ℂ)) = logPhaseMainTerm N T := by - let τ : ℂ := (2 * Real.pi : ℂ) * Complex.I - let v : ℝ → ℂ := fun x ↦ 𝐞 (T * Real.log (x / N)) - let denom : ℂ := 1 + τ * T - let G : ℝ → ℂ := fun x ↦ x * v x / denom - have hdenom : denom ≠ 0 := by - intro h - have hre := congrArg Complex.re h - simp [denom, τ] at hre - have hv (x : ℝ) (hx : 0 < x) : - HasDerivAt v (τ * T / x * v x) x := by - have hdiv : HasDerivAt (fun y : ℝ ↦ y / N) (1 / N) x := by - simpa using (hasDerivAt_id x).div_const N - have hlog := (Real.hasDerivAt_log (div_pos hx hN).ne').comp x hdiv - have hinner : HasDerivAt (fun y ↦ T * Real.log (y / N)) (T / x) x := by - convert hlog.const_mul T using 1 <;> - first | rfl | field_simp [hN.ne', hx.ne'] - have hchar' := (Real.hasDerivAt_fourierChar (T * Real.log (x / N))).scomp x hinner - dsimp only [v] - change HasDerivAt ((𝐞 · : ℝ → ℂ) ∘ fun y ↦ T * Real.log (y / N)) - (τ * T / x * (𝐞 (T * Real.log (x / N)) : ℂ)) x - rw [show τ * T / x * (𝐞 (T * Real.log (x / N)) : ℂ) = - (T / x) • ((2 * Real.pi : ℂ) * Complex.I * 𝐞 (T * Real.log (x / N))) by - dsimp [τ] - simp only [Complex.ofReal_div] - ring] - exact hchar' - have hG (x : ℝ) (hx : 0 < x) : HasDerivAt G (v x) x := by - have hprod := (hasDerivAt_id x).ofReal_comp.mul (hv x hx) - have hquot := hprod.div_const denom - have hderivEq : - ((1 : ℂ) * v x + x * (τ * T / x * v x)) / denom = v x := by - apply (div_eq_iff hdenom).2 - dsimp [denom, τ] - field_simp [hx.ne'] - rw [← hderivEq] - simpa only [G, Pi.mul_apply, id_eq, Complex.ofReal_one] using hquot - have hvCont : ContinuousOn v (Set.uIcc N (2 * N)) := by - intro x hx - have hxIcc : x ∈ Set.Icc N (2 * N) := by - simpa [Set.uIcc_of_le (by linarith : N ≤ 2 * N)] using hx - exact (hv x (hN.trans_le hxIcc.1)).continuousAt.continuousWithinAt - have hFTC := intervalIntegral.integral_eq_sub_of_hasDerivAt - (a := N) (b := 2 * N) (f := G) (f' := v) - (fun x hx ↦ by - have hxIcc : x ∈ Set.Icc N (2 * N) := by - simpa [Set.uIcc_of_le (by linarith : N ≤ 2 * N)] using hx - exact hG x (hN.trans_le hxIcc.1)) hvCont.intervalIntegrable - have hformula : (∫ x in N..2 * N, v x) = - (N : ℂ) * (2 * 𝐞 (T * Real.log 2) - 1) / denom := by - rw [hFTC] - dsimp [G, v] - rw [show (2 * N) / N = 2 by field_simp [hN.ne'], - show N / N = 1 by field_simp [hN.ne'], Real.log_one] - simp only [mul_zero] - rw [show (𝐞 (0 : ℝ) : ℂ) = 1 by norm_num] + let r : ℂ := (2 * Real.pi : ℂ) * Complex.I * T + have hchar (u : ℝ) (hu : 0 < u) : + (𝐞 (T * Real.log u) : ℂ) = (u : ℂ) ^ r := by + rw [Real.fourierChar_apply, + Complex.cpow_def_of_ne_zero (Complex.ofReal_ne_zero.mpr hu.ne')] + rw [← Complex.ofReal_log hu.le] + congr 1 + dsimp [r] push_cast - field_simp [hdenom] - simpa only [v, logPhaseMainTerm, denom, τ, mul_assoc] using hformula + ring + have hscale : + (∫ x in N..2 * N, (𝐞 (T * Real.log (x / N)) : ℂ)) = + (N : ℂ) * ∫ u in (1 : ℝ)..2, (𝐞 (T * Real.log u) : ℂ) := by + have h := intervalIntegral.smul_integral_comp_mul_left + (f := fun x : ℝ ↦ (𝐞 (T * Real.log (x / N)) : ℂ)) + (a := (1 : ℝ)) (b := 2) N + rw [show N * (1 : ℝ) = N by ring, show N * 2 = 2 * N by ring] at h + rw [← h, Complex.real_smul] + refine congrArg (fun z : ℂ ↦ (N : ℂ) * z) ?_ + apply intervalIntegral.integral_congr + intro u _ + exact congrArg (fun y : ℝ ↦ (𝐞 (T * Real.log y) : ℂ)) + (by field_simp [hN.ne'] : N * u / N = u) + rw [hscale] + have hint : + (∫ u in (1 : ℝ)..2, (𝐞 (T * Real.log u) : ℂ)) = + ((2 : ℂ) ^ (r + 1) - (1 : ℂ) ^ (r + 1)) / (r + 1) := by + rw [intervalIntegral.integral_congr_Ioo_of_le (by norm_num) + (fun u hu ↦ hchar u (by linarith [hu.1]))] + exact integral_cpow (Or.inl (by simp [r])) + rw [hint, Complex.one_cpow] + rw [Complex.cpow_add _ _ (by norm_num : (2 : ℂ) ≠ 0), Complex.cpow_one] + have htwo : (2 : ℂ) ^ r = (𝐞 (T * Real.log 2) : ℂ) := + (hchar 2 (by norm_num)).symm + simp only [htwo] + dsimp [logPhaseMainTerm, r] + ring /-- The logarithmic main term has size comparable to `N / T`. -/ theorem norm_logPhaseMainTerm_bounds diff --git a/Expdb/ExponentialSums/OscillatoryBounds.lean b/Expdb/ExponentialSums/OscillatoryBounds.lean index bdaa5a7..1bce113 100644 --- a/Expdb/ExponentialSums/OscillatoryBounds.lean +++ b/Expdb/ExponentialSums/OscillatoryBounds.lean @@ -1,10 +1,11 @@ module -public import Expdb.ExponentialSums.PhaseFunctions +public import Expdb.ExponentialSums.FixedExponentialSum public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic public import Mathlib.Order.Interval.Finset.Nat import Expdb.Mathlib.EulerMaclaurin +import Expdb.Mathlib.IteratedDeriv import Mathlib.Analysis.Calculus.ContDiff.Bounds import Mathlib.Analysis.Fourier.FourierTransformDeriv import Mathlib.Analysis.Real.Pi.Bounds @@ -13,9 +14,9 @@ import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts /-! # Oscillatory integral and exponential-sum bounds -Calculus for the Fourier character and uniform estimates for functions of the form -`x ↦ 𝐞 (T * F (x / N))`, including a first-derivative integral bound and -Euler–Maclaurin comparisons between oscillatory sums and integrals. +Calculus for the Fourier character and uniform estimates for `oscillatory F T N`, including a +first-derivative integral bound and Euler–Maclaurin comparisons between oscillatory sums and +integrals. -/ @[expose] public section @@ -56,45 +57,19 @@ theorem iteratedDeriv_fourierChar (n : ℕ) (x : ℝ) : (ENat.natCast_le_of_coe_top_le_withTop le_rfl n)), ih] ring +/-- The norm of the `n`th derivative of the real Fourier character is exactly `(2π)ⁿ`. -/ +@[simp] theorem norm_iteratedDeriv_fourierChar (n : ℕ) (x : ℝ) : + ‖iteratedDeriv n (𝐞 · : ℝ → ℂ) x‖ = (2 * Real.pi) ^ n := by + rw [iteratedDeriv_fourierChar, norm_mul, norm_pow] + simp [Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg Real.pi_pos.le] + private lemma norm_iteratedDeriv_fourierChar_le {n k : ℕ} (hk : k ≤ n) (x : ℝ) : ‖iteratedDeriv k (𝐞 · : ℝ → ℂ) x‖ ≤ (2 * Real.pi + 1) ^ n := by - rw [iteratedDeriv_fourierChar, norm_mul, norm_pow] - have hcoeff : ‖(2 * Real.pi : ℂ) * Complex.I‖ = 2 * Real.pi := by - simp [Complex.norm_real, Real.norm_eq_abs, Real.pi_pos.le] - have hchar : ‖(𝐞 x : ℂ)‖ = 1 := by simp - rw [hcoeff, hchar, mul_one] + rw [norm_iteratedDeriv_fourierChar] exact (pow_le_pow_left₀ (by positivity) (by linarith) k).trans (pow_le_pow_right₀ (by linarith [Real.pi_pos]) hk) -private lemma iteratedDerivWithin_comp_const_mul_of_mapsTo - {f : ℝ → ℝ} {s t : Set ℝ} {x c : ℝ} {n : ℕ} - (hf : ContDiffOn ℝ n f t) (hs : UniqueDiffOn ℝ s) (ht : UniqueDiffOn ℝ t) - (hx : x ∈ s) (hst : Set.MapsTo (c * ·) s t) : - iteratedDerivWithin n (fun y ↦ f (c * y)) s x = - c ^ n * iteratedDerivWithin n f t (c * x) := by - induction n generalizing x with - | zero => simp - | succ n ih => - have hcx : c * x ∈ t := hst hx - have heq : Set.EqOn - (iteratedDerivWithin n (fun y ↦ f (c * y)) s) - (fun y ↦ c ^ n * iteratedDerivWithin n f t (c * y)) s := - fun y hy ↦ ih hf.of_succ hy - have houter : DifferentiableWithinAt ℝ (iteratedDerivWithin n f t) t (c * x) := - hf.differentiableOn_iteratedDerivWithin (Nat.cast_lt.mpr n.lt_succ_self) ht _ hcx - have hcomp : DifferentiableWithinAt ℝ - (fun y ↦ iteratedDerivWithin n f t (c * y)) s x := - houter.comp x (by fun_prop) hst - rw [iteratedDerivWithin_succ, - derivWithin_congr heq (ih hf.of_succ hx), - derivWithin_const_mul _ hcomp, iteratedDerivWithin_succ, - ← Function.comp_def, derivWithin.scomp x houter (by fun_prop) hst, - derivWithin_const_mul _ differentiableWithinAt_id, - derivWithin_id' _ _ (hs.uniqueDiffWithinAt hx)] - simp only [smul_eq_mul, mul_one, pow_succ] - ring - /-! ## Derivative bounds for oscillatory phases -/ /-- Uniform derivative control for a rescaled oscillatory phase. -/ @@ -103,9 +78,8 @@ theorem norm_iteratedDerivWithin_oscillatory_le (hF : ContDiffOn ℝ n F phaseInterval) (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) (hmap : Set.MapsTo (N⁻¹ * ·) s phaseInterval) (hT : 1 ≤ T) (hN : 1 ≤ N) (hK : 1 ≤ K) - (hderiv : ∀ k : ℕ, 1 ≤ k → k ≤ n → - ∀ u ∈ phaseInterval, ‖iteratedDerivWithin k F phaseInterval u‖ ≤ K) : - ‖iteratedDerivWithin n (fun y ↦ (𝐞 (T * F (y / N)) : ℂ)) s x‖ ≤ + (hderiv : HasPhaseDerivBound F n K) : + ‖iteratedDerivWithin n (oscillatory F T N) s x‖ ≤ (n.factorial : ℝ) * (2 * Real.pi + 1) ^ n * (K * T / N) ^ n := by let q : ℝ → ℝ := fun y ↦ T * F (N⁻¹ * y) have hscale : ContDiffOn ℝ n (N⁻¹ * ·) s := by fun_prop @@ -132,10 +106,13 @@ theorem norm_iteratedDerivWithin_oscillatory_le ‖iteratedFDerivWithin ℝ k q s x‖ ≤ (K * T / N) ^ k := by intro k hk hkn rw [norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin] - have hrescale := iteratedDerivWithin_comp_const_mul_of_mapsTo - (f := F) (c := N⁻¹) (n := k) - (hF.of_le (Nat.cast_le.mpr hkn)) hs - (uniqueDiffOn_Icc (by norm_num [phaseInterval])) hx hmap + have hrescale : iteratedDerivWithin k (fun y ↦ F (N⁻¹ * y)) s x = + N⁻¹ ^ k * iteratedDerivWithin k F phaseInterval (N⁻¹ * x) := by + simpa only [add_zero] using iteratedDerivWithin_comp_affine_of_mapsTo + (f := F) (c := N⁻¹) (d := 0) (n := k) + (hF.of_le (Nat.cast_le.mpr hkn)) hs + (uniqueDiffOn_Icc (by norm_num [phaseInterval])) hx + (by simpa only [add_zero] using hmap) have hqderiv : iteratedDerivWithin k q s x = T * N⁻¹ ^ k * iteratedDerivWithin k F phaseInterval (N⁻¹ * x) := by rw [show q = fun y ↦ T * F (N⁻¹ * y) by rfl, @@ -159,6 +136,7 @@ theorem norm_iteratedDerivWithin_oscillatory_le rw [norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin] at hcomp change ‖iteratedDerivWithin n (fun y ↦ (𝐞 (q y) : ℂ)) s x‖ ≤ (n.factorial : ℝ) * (2 * Real.pi + 1) ^ n * (K * T / N) ^ n at hcomp + rw [show oscillatory F T N = fun y ↦ (𝐞 (T * F (y / N)) : ℂ) from rfl] simpa only [q, div_eq_mul_inv, mul_comm N⁻¹] using hcomp /-- A smooth phase remains smooth after rescaling and composition with the Fourier character. -/ @@ -166,17 +144,17 @@ theorem contDiffOn_oscillatory {F : ℝ → ℝ} {s : Set ℝ} {T N : ℝ} {n : ℕ} (hF : ContDiffOn ℝ n F phaseInterval) (hmap : Set.MapsTo (N⁻¹ * ·) s phaseInterval) : - ContDiffOn ℝ n (fun x ↦ (𝐞 (T * F (x / N)) : ℂ)) s := by + ContDiffOn ℝ n (oscillatory F T N) s := by have hscale : ContDiffOn ℝ n (N⁻¹ * ·) s := by fun_prop have hFscale : ContDiffOn ℝ n (fun x ↦ F (N⁻¹ * x)) s := by change ContDiffOn ℝ n (F ∘ fun x ↦ N⁻¹ * x) s exact hF.comp hscale hmap have hinner : ContDiffOn ℝ n (fun x ↦ T * F (N⁻¹ * x)) s := contDiffOn_const.mul hFscale - have heq : (fun x ↦ (𝐞 (T * F (x / N)) : ℂ)) = + have heq : oscillatory F T N = (𝐞 · : ℝ → ℂ) ∘ fun x ↦ T * F (N⁻¹ * x) := by funext x - simp only [Function.comp_apply, div_eq_mul_inv] + simp only [oscillatory, Function.comp_apply, div_eq_mul_inv] rw [mul_comm x N⁻¹] rw [heq] exact (contDiff_fourierChar.of_le @@ -409,14 +387,14 @@ private lemma norm_oscillatory_sum_sub_integral_le (s : ℕ) {F : ℝ → ℝ} {T N K : ℝ} {a b : ℕ} (hab : a < b) (hN : 1 ≤ N) (hT : 1 ≤ T) (hK : 1 ≤ K) (hF : ContDiffOn ℝ ∞ F phaseInterval) - (hderiv : ∀ k : ℕ, 1 ≤ k → k ≤ s + 1 → ∀ u ∈ phaseInterval, - ‖iteratedDerivWithin k F phaseInterval u‖ ≤ K) + (hderiv : HasPhaseDerivBound F (s + 1) K) (ha : N ≤ a) (hb : (b : ℝ) ≤ 2 * N) - (hratio : K * T / N ≤ 1) - (hremainder : N * (K * T / N) ^ (s + 1) ≤ 1) : - ‖(∑ n ∈ Finset.Icc a b, (𝐞 (T * F ((n : ℝ) / N)) : ℂ)) - - ∫ x in (a : ℝ)..b, (𝐞 (T * F (x / N)) : ℂ)‖ ≤ + (hscale : HasSmallEulerMaclaurinRemainder s T N K) : + ‖exponentialSumAt F T N a b - + ∫ x in (a : ℝ)..b, oscillatory F T N x‖ ≤ oscillatoryErrorConstant s := by + obtain ⟨hratio, hremainder⟩ := hscale + rw [exponentialSumAt] have hNpos : 0 < N := zero_lt_one.trans_le hN have hrnonneg : 0 ≤ K * T / N := by positivity let interval : Set ℝ := Set.Icc (a : ℝ) (b : ℝ) @@ -432,14 +410,14 @@ private lemma norm_oscillatory_sum_sub_integral_le let A : ℕ → ℝ := fun k ↦ (k.factorial : ℝ) * (2 * Real.pi + 1) ^ k have hosc (k : ℕ) (hk : 1 ≤ k) (hkS : k ≤ s + 1) (x : ℝ) (hx : x ∈ interval) : - ‖iteratedDerivWithin k (fun y ↦ (𝐞 (T * F (y / N)) : ℂ)) interval x‖ ≤ + ‖iteratedDerivWithin k (oscillatory F T N) interval x‖ ≤ A k * (K * T / N) ^ k := by simpa only [A] using norm_iteratedDerivWithin_oscillatory_le (hF.of_le (ENat.natCast_le_of_coe_top_le_withTop le_rfl k)) hunique hx hmap hT hN hK (fun q hq hqk u hu ↦ hderiv q hq (hqk.trans hkS) u hu) have hraw := EulerMaclaurin.norm_sum_Icc_nat_sub_integral_le - (f := fun y ↦ (𝐞 (T * F (y / N)) : ℂ)) (t := interval) + (f := oscillatory F T N) (t := interval) hab.le (contDiffOn_oscillatory (hF.of_le (ENat.natCast_le_of_coe_top_le_withTop le_rfl (s + 1))) hmap) @@ -496,16 +474,15 @@ theorem exists_norm_oscillatory_sum_sub_integral_le (s : ℕ) : ∀ {F : ℝ → ℝ} {T N K : ℝ} {a b : ℕ}, a < b → 1 ≤ N → 1 ≤ T → 1 ≤ K → ContDiffOn ℝ ∞ F phaseInterval → - (∀ k : ℕ, 1 ≤ k → k ≤ s + 1 → ∀ u ∈ phaseInterval, - ‖iteratedDerivWithin k F phaseInterval u‖ ≤ K) → + HasPhaseDerivBound F (s + 1) K → N ≤ a → (b : ℝ) ≤ 2 * N → - K * T / N ≤ 1 → N * (K * T / N) ^ (s + 1) ≤ 1 → - ‖(∑ n ∈ Finset.Icc a b, (𝐞 (T * F ((n : ℝ) / N)) : ℂ)) - - ∫ x in (a : ℝ)..b, (𝐞 (T * F (x / N)) : ℂ)‖ ≤ C := by + HasSmallEulerMaclaurinRemainder s T N K → + ‖exponentialSumAt F T N a b - + ∫ x in (a : ℝ)..b, oscillatory F T N x‖ ≤ C := by refine ⟨oscillatoryErrorConstant s, one_le_oscillatoryErrorConstant s, ?_⟩ - intro F T N K a b hab hN hT hK hF hderiv ha hb hratio hremainder + intro F T N K a b hab hN hT hK hF hderiv ha hb hscale exact norm_oscillatory_sum_sub_integral_le s hab hN hT hK hF hderiv - ha hb hratio hremainder + ha hb hscale private def oscillatorySumConstant (s : ℕ) (K c : ℝ) : ℝ := oscillatoryErrorConstant s + (2 / c + K / c ^ 2) @@ -522,21 +499,17 @@ private lemma norm_oscillatory_sum_le (s : ℕ) {F : ℝ → ℝ} {T N K c : ℝ} {a b : ℕ} (hs : 1 ≤ s) (hab : a ≤ b) (hN : 1 ≤ N) (hT : 1 ≤ T) (hK : 1 ≤ K) (hc : 0 < c) (hF : ContDiffOn ℝ ∞ F phaseInterval) - (hfirst : ∀ u ∈ phaseInterval, - c ≤ iteratedDerivWithin 1 F phaseInterval u) - (hderiv : ∀ k : ℕ, 1 ≤ k → k ≤ s + 1 → ∀ u ∈ phaseInterval, - ‖iteratedDerivWithin k F phaseInterval u‖ ≤ K) + (hfirst : HasPhaseFirstDerivLowerBound F c) + (hderiv : HasPhaseDerivBound F (s + 1) K) (ha : N ≤ a) (hb : (b : ℝ) ≤ 2 * N) - (hratio : K * T / N ≤ 1) - (hremainder : N * (K * T / N) ^ (s + 1) ≤ 1) : - ‖∑ n ∈ Finset.Icc a b, (𝐞 (T * F ((n : ℝ) / N)) : ℂ)‖ ≤ + (hscale : HasSmallEulerMaclaurinRemainder s T N K) : + ‖exponentialSumAt F T N a b‖ ≤ oscillatorySumConstant s K c * (1 + N / T) := by have hNpos : 0 < N := zero_lt_one.trans_le hN have hTpos : 0 < T := zero_lt_one.trans_le hT by_cases heq : a = b · subst b - simp only [Finset.Icc_self, Finset.sum_singleton] - rw [show ‖(𝐞 (T * F ((a : ℝ) / N)) : ℂ)‖ = 1 by simp] + rw [exponentialSumAt_self, norm_oscillatory] have hconst : 1 ≤ oscillatorySumConstant s K c := by dsimp only [oscillatorySumConstant] have hE := one_le_oscillatoryErrorConstant s @@ -546,7 +519,7 @@ private lemma norm_oscillatory_sum_le nlinarith have hablt : a < b := hab.lt_of_ne heq have herr := norm_oscillatory_sum_sub_integral_le s hablt hN hT hK hF hderiv - ha hb hratio hremainder + ha hb hscale have hAB : (a : ℝ) / N ≤ (b : ℝ) / N := div_le_div_of_nonneg_right (by exact_mod_cast hab) hNpos.le have hsub : Set.Icc ((a : ℝ) / N) ((b : ℝ) / N) ⊆ phaseInterval := by @@ -558,21 +531,23 @@ private lemma norm_oscillatory_sum_le (hF.of_le (ENat.natCast_le_of_coe_top_le_withTop le_rfl 2)) hTpos hc (fun x hx ↦ hfirst x (hsub hx)) (fun x hx ↦ hderiv 2 (by norm_num) (by omega) x (hsub hx)) - have hscale := intervalIntegral.integral_comp_div + have hcomp := intervalIntegral.integral_comp_div (fun y : ℝ ↦ (𝐞 (T * F y) : ℂ)) (a := (a : ℝ)) (b := (b : ℝ)) hNpos.ne' have hint : - ‖∫ x in (a : ℝ)..b, (𝐞 (T * F (x / N)) : ℂ)‖ ≤ + ‖∫ x in (a : ℝ)..b, oscillatory F T N x‖ ≤ (2 / c + K / c ^ 2) * (N / T) := by - rw [hscale, norm_smul, Real.norm_eq_abs, abs_of_pos hNpos] + rw [show (fun x ↦ oscillatory F T N x) = + fun x ↦ (𝐞 (T * F (x / N)) : ℂ) from rfl, + hcomp, norm_smul, Real.norm_eq_abs, abs_of_pos hNpos] calc N * ‖∫ x in (a : ℝ) / N..(b : ℝ) / N, (𝐞 (T * F x) : ℂ)‖ ≤ N * ((2 / c + K / c ^ 2) / T) := by gcongr _ = (2 / c + K / c ^ 2) * (N / T) := by ring calc - ‖∑ n ∈ Finset.Icc a b, (𝐞 (T * F ((n : ℝ) / N)) : ℂ)‖ ≤ - ‖(∑ n ∈ Finset.Icc a b, (𝐞 (T * F ((n : ℝ) / N)) : ℂ)) - - ∫ x in (a : ℝ)..b, (𝐞 (T * F (x / N)) : ℂ)‖ + - ‖∫ x in (a : ℝ)..b, (𝐞 (T * F (x / N)) : ℂ)‖ := + ‖exponentialSumAt F T N a b‖ ≤ + ‖exponentialSumAt F T N a b - + ∫ x in (a : ℝ)..b, oscillatory F T N x‖ + + ‖∫ x in (a : ℝ)..b, oscillatory F T N x‖ := norm_le_norm_sub_add _ _ _ ≤ oscillatoryErrorConstant s + (2 / c + K / c ^ 2) * (N / T) := by gcongr @@ -591,18 +566,17 @@ theorem exists_norm_oscillatory_sum_le ∀ {F : ℝ → ℝ} {T N : ℝ} {a b : ℕ}, a ≤ b → 1 ≤ N → 1 ≤ T → ContDiffOn ℝ ∞ F phaseInterval → - (∀ u ∈ phaseInterval, c ≤ iteratedDerivWithin 1 F phaseInterval u) → - (∀ k : ℕ, 1 ≤ k → k ≤ s + 1 → ∀ u ∈ phaseInterval, - ‖iteratedDerivWithin k F phaseInterval u‖ ≤ K) → + HasPhaseFirstDerivLowerBound F c → + HasPhaseDerivBound F (s + 1) K → N ≤ a → (b : ℝ) ≤ 2 * N → - K * T / N ≤ 1 → N * (K * T / N) ^ (s + 1) ≤ 1 → - ‖∑ n ∈ Finset.Icc a b, (𝐞 (T * F ((n : ℝ) / N)) : ℂ)‖ ≤ + HasSmallEulerMaclaurinRemainder s T N K → + ‖exponentialSumAt F T N a b‖ ≤ C * (1 + N / T) := by refine ⟨oscillatorySumConstant s K c, one_le_oscillatorySumConstant s hK hc, ?_⟩ - intro F T N a b hab hN hT hF hfirst hderiv ha hb hratio hremainder + intro F T N a b hab hN hT hF hfirst hderiv ha hb hscale exact norm_oscillatory_sum_le s hs hab hN hT hK hc hF hfirst hderiv - ha hb hratio hremainder + ha hb hscale end Expdb diff --git a/Expdb/ExponentialSums/PhaseFunctions.lean b/Expdb/ExponentialSums/PhaseFunctions.lean index 275a012..4b15df1 100644 --- a/Expdb/ExponentialSums/PhaseFunctions.lean +++ b/Expdb/ExponentialSums/PhaseFunctions.lean @@ -4,6 +4,7 @@ public import Expdb.Basic.Asymptotics public import Mathlib.Analysis.Calculus.IteratedDeriv.Defs public import Mathlib.Analysis.SpecialFunctions.Pow.Real import Expdb.Basic.AutomaticUniformity +import Expdb.Mathlib.IteratedDeriv import Mathlib.Analysis.SpecialFunctions.Pow.Deriv /-! @@ -33,27 +34,332 @@ ambient index. -/ def IsPhaseFunction (F : VariableFunction (VariableObject.fixed ℝ) ℝ) : Prop := ∀ i : ℕ, ContDiffOn ℝ ∞ (F i) phaseInterval +/-- The reference phase `u ↦ u ^ (-σ)` whose derivatives a model phase follows. -/ +def modelPhase (σ : ℝ) : ℝ → ℝ := fun u ↦ u ^ (-σ) + +/-- The fixed-data model-phase error at derivative order `p`. -/ +def modelPhaseErrorAt (F : ℝ → ℝ) (σ : ℝ) (p : ℕ) (u : ℝ) : ℝ := + iteratedDerivWithin (p + 1) F phaseInterval u - + iteratedDerivWithin p (modelPhase σ) phaseInterval u + /-- The variable error function in the model phase condition at derivative order `p`. -/ def modelPhaseError (F : VariableFunction (VariableObject.fixed ℝ) ℝ) (σ : ℝ) (p : ℕ) : VariableFunction (VariableObject.fixed phaseInterval) ℝ := - fun i u ↦ - iteratedDerivWithin (p + 1) (F i) phaseInterval u - - iteratedDerivWithin p (fun v : ℝ => v ^ (-σ)) phaseInterval u + fun i u ↦ modelPhaseErrorAt (F i) σ p u + +@[simp] theorem modelPhaseError_apply + (F : VariableFunction (VariableObject.fixed ℝ) ℝ) (σ : ℝ) (p i : ℕ) + (u : phaseInterval) : + modelPhaseError F σ p i u = modelPhaseErrorAt (F i) σ p u := + rfl + +/-- The phase interval has unique derivatives. -/ +theorem uniqueDiffOn_phaseInterval : UniqueDiffOn ℝ phaseInterval := + uniqueDiffOn_Icc (by norm_num [phaseInterval]) + +/-- Every reference model phase is smooth on the phase interval. -/ +theorem contDiffOn_modelPhase (σ : ℝ) : + ContDiffOn ℝ ∞ (modelPhase σ) phaseInterval := by + intro u hu + exact (Real.contDiffAt_rpow_const_of_ne + (ne_of_gt (zero_lt_one.trans_le hu.1))).contDiffWithinAt + +/-- The derivatives of the reference model phase have the expected falling-factorial +formula on the phase interval. -/ +theorem iteratedDerivWithin_modelPhase (σ : ℝ) (p : ℕ) {u : ℝ} + (hu : u ∈ phaseInterval) : + iteratedDerivWithin p (modelPhase σ) phaseInterval u = + (descPochhammer ℝ p).eval (-σ) * u ^ (-σ - p) := by + have hu0 : u ≠ 0 := ne_of_gt (zero_lt_one.trans_le hu.1) + have hsmooth : ContDiffAt ℝ p (modelPhase σ) u := by + change ContDiffAt ℝ p (fun x : ℝ ↦ x ^ (-σ)) u + exact Real.contDiffAt_rpow_const_of_ne hu0 + rw [iteratedDerivWithin_eq_iteratedDeriv uniqueDiffOn_phaseInterval hsmooth hu, + iteratedDeriv_eq_iterate] + exact Real.iter_deriv_rpow_const (-σ) u p + +/-- On `[1, 2]`, the falling-factorial coefficient bounds the corresponding derivative +of a model phase with nonnegative exponent. -/ +theorem norm_iteratedDerivWithin_modelPhase_le {σ : ℝ} (hσ : 0 ≤ σ) (p : ℕ) + {u : ℝ} (hu : u ∈ phaseInterval) : + ‖iteratedDerivWithin p (modelPhase σ) phaseInterval u‖ ≤ + ‖(descPochhammer ℝ p).eval (-σ)‖ := by + rw [iteratedDerivWithin_modelPhase σ p hu, norm_mul, + Real.norm_of_nonneg (Real.rpow_nonneg (zero_le_one.trans hu.1) _)] + simpa only [mul_one] using mul_le_mul_of_nonneg_left + (Real.rpow_le_one_of_one_le_of_nonpos hu.1 (by + have hp : 0 ≤ (p : ℝ) := Nat.cast_nonneg p + linarith)) + (norm_nonneg ((descPochhammer ℝ p).eval (-σ))) + +/-- The iterated derivatives of a reference model phase vary continuously on the phase +interval. -/ +theorem continuousOn_iteratedDerivWithin_modelPhase (σ : ℝ) (p : ℕ) : + ContinuousOn (iteratedDerivWithin p (modelPhase σ) phaseInterval) phaseInterval := + (contDiffOn_modelPhase σ).continuousOn_iteratedDerivWithin + (ENat.natCast_le_of_coe_top_le_withTop le_rfl p) uniqueDiffOn_phaseInterval + +/-- A fixed phase function whose model-phase errors through order `P` are at most `δ`. -/ +def IsApproximateModelPhaseFunction + (F : ℝ → ℝ) (σ : ℝ) (P : ℕ) (δ : ℝ) : Prop := + ContDiffOn ℝ ∞ F phaseInterval ∧ + ∀ p : ℕ, p ≤ P → ∀ u : phaseInterval, + ‖modelPhaseErrorAt F σ p u‖ ≤ δ + +/-- The derivatives of orders `1, …, n` of `F` are bounded by `K` on the phase interval. -/ +def HasPhaseDerivBound (F : ℝ → ℝ) (n : ℕ) (K : ℝ) : Prop := + ∀ k : ℕ, 1 ≤ k → k ≤ n → ∀ u ∈ phaseInterval, + ‖iteratedDerivWithin k F phaseInterval u‖ ≤ K + +/-- The first derivative of `F` is at least `c` on the phase interval. -/ +def HasPhaseFirstDerivLowerBound (F : ℝ → ℝ) (c : ℝ) : Prop := + ∀ u ∈ phaseInterval, c ≤ iteratedDerivWithin 1 F phaseInterval u + +/-- A derivative bound may be restricted to a smaller order. -/ +theorem HasPhaseDerivBound.of_le {F : ℝ → ℝ} {m n : ℕ} {K : ℝ} + (hF : HasPhaseDerivBound F n K) (hmn : m ≤ n) : + HasPhaseDerivBound F m K := + fun k hk hkm u hu ↦ hF k hk (hkm.trans hmn) u hu + +/-- The data defining a model phase when its reference exponent `σ` has already been fixed. -/ +structure IsModelPhaseFunctionWith + (F : VariableFunction (VariableObject.fixed ℝ) ℝ) (σ : ℝ) : Prop where + /-- Every member of the family is smooth on the phase interval. -/ + isPhaseFunction : IsPhaseFunction F + /-- Every fixed-order model-phase error is choicewise infinitesimal. -/ + error_isChoicewiseInfinitesimal : + ∀ p : ℕ, (modelPhaseError F σ p).IsChoicewiseInfinitesimal /-- A variable phase function is a model phase function when, for some fixed `σ > 0`, the error between its `(p + 1)`st derivative and the `p`th derivative of `u ↦ u ^ (-σ)` is -pointwise infinitesimal for every fixed derivative order `p`. -/ +choicewise infinitesimal for every fixed derivative order `p`. -/ def IsModelPhaseFunction (F : VariableFunction (VariableObject.fixed ℝ) ℝ) : Prop := IsPhaseFunction F ∧ ∃ σ : ℝ, 0 < σ ∧ - ∀ p : ℕ, (modelPhaseError F σ p).IsPointwiseInfinitesimal + ∀ p : ℕ, (modelPhaseError F σ p).IsChoicewiseInfinitesimal + +/-- Fixed model-phase data with a positive reference exponent gives a model phase function. -/ +theorem IsModelPhaseFunctionWith.isModelPhaseFunction + {F : VariableFunction (VariableObject.fixed ℝ) ℝ} {σ : ℝ} + (hF : IsModelPhaseFunctionWith F σ) (hσ : 0 < σ) : + IsModelPhaseFunction F := + ⟨hF.isPhaseFunction, σ, hσ, hF.error_isChoicewiseInfinitesimal⟩ + +/-- A model phase function admits fixed-exponent model-phase data. -/ +theorem IsModelPhaseFunction.exists_with + {F : VariableFunction (VariableObject.fixed ℝ) ℝ} + (hF : IsModelPhaseFunction F) : + ∃ σ : ℝ, 0 < σ ∧ IsModelPhaseFunctionWith F σ := by + rcases hF with ⟨hphase, σ, hσ, herror⟩ + exact ⟨σ, hσ, ⟨hphase, herror⟩⟩ + +/-- Adding a linear function changes only the zeroth model-phase error. -/ +theorem modelPhaseErrorAt_add_linear + {F : ℝ → ℝ} {σ c u : ℝ} {p : ℕ} + (hF : ContDiffOn ℝ ∞ F phaseInterval) (hu : u ∈ phaseInterval) : + modelPhaseErrorAt (fun x ↦ F x + c * x) σ p u = + modelPhaseErrorAt F σ p u + if p = 0 then c else 0 := by + change modelPhaseErrorAt (F + fun x ↦ c * x) σ p u = _ + rw [modelPhaseErrorAt, modelPhaseErrorAt, + iteratedDerivWithin_add hu uniqueDiffOn_phaseInterval + ((hF u hu).of_le + (ENat.natCast_le_of_coe_top_le_withTop le_rfl (p + 1))) + ((show ContDiffOn ℝ ∞ (fun x : ℝ ↦ c * x) phaseInterval by fun_prop) + u hu |>.of_le + (ENat.natCast_le_of_coe_top_le_withTop le_rfl (p + 1)))] + rw [iteratedDerivWithin_const_mul_field, + iteratedDerivWithin_fun_id hu uniqueDiffOn_phaseInterval] + by_cases hp : p = 0 + · subst p + simp + ring + · simp only [if_neg (by omega : p + 1 ≠ 0), if_neg (by omega : p + 1 ≠ 1), + mul_zero, add_zero, hp] + simp + +/-- Adding a controlled linear term increases the model-phase error by at most the norm of its +coefficient. -/ +theorem IsApproximateModelPhaseFunction.add_linear + {F : ℝ → ℝ} {σ δ η c : ℝ} {P : ℕ} + (hF : IsApproximateModelPhaseFunction F σ P δ) (hc : ‖c‖ ≤ η) : + IsApproximateModelPhaseFunction (fun u ↦ F u + c * u) σ P (δ + η) := by + refine ⟨hF.1.add (by fun_prop), ?_⟩ + intro p hp u + have hη : 0 ≤ η := (norm_nonneg c).trans hc + rw [modelPhaseErrorAt_add_linear hF.1 u.property] + calc + ‖modelPhaseErrorAt F σ p u + if p = 0 then c else 0‖ ≤ + ‖modelPhaseErrorAt F σ p u‖ + ‖if p = 0 then c else 0‖ := + norm_add_le _ _ + _ ≤ δ + η := add_le_add (hF.2 p hp u) (by + by_cases h : p = 0 + · simpa [h] using hc + · simp [h, hη]) + +/-- Model-phase data is stable under addition of an infinitesimal linear term. -/ +theorem IsModelPhaseFunctionWith.add_infinitesimal_linear + {F : VariableFunction (VariableObject.fixed ℝ) ℝ} {σ : ℝ} + (hF : IsModelPhaseFunctionWith F σ) + {c : VariableObject ℝ} (hc : c.IsInfinitesimal) : + IsModelPhaseFunctionWith (fun i u ↦ F i u + c i * u) σ := by + refine ⟨fun i ↦ (hF.isPhaseFunction i).add (by fun_prop), ?_⟩ + intro p u + rw [VariableObject.IsInfinitesimal] + have herr := hF.error_isChoicewiseInfinitesimal p u + rw [VariableObject.IsInfinitesimal] at herr + have hc' : Tendsto (fun i ↦ ‖c i‖) atTop (𝓝 0) := hc + apply squeeze_zero' (g := fun i ↦ + ‖modelPhaseErrorAt (F i) σ p (u i)‖ + ‖c i‖) + · exact Filter.Eventually.of_forall fun _ ↦ norm_nonneg _ + · filter_upwards [] with i + rw [modelPhaseError_apply, + modelPhaseErrorAt_add_linear (hF.isPhaseFunction i) (u i).property] + split_ifs + · exact norm_add_le _ _ + · simp + · simpa [modelPhaseError] using herr.add hc' + +/-- Model-phase data is stable under affine reparametrizations that tend to the identity and map +the phase interval to itself. -/ +theorem IsModelPhaseFunctionWith.comp_affine_tendsto_id + {F : VariableFunction (VariableObject.fixed ℝ) ℝ} {σ : ℝ} + (hF : IsModelPhaseFunctionWith F σ) {c d : VariableObject ℝ} + (hc : Tendsto c atTop (𝓝 1)) (hd : Tendsto d atTop (𝓝 0)) + (hmap : ∀ i, Set.MapsTo (fun u ↦ c i * u + d i) phaseInterval phaseInterval) : + IsModelPhaseFunctionWith (fun i u ↦ F i (c i * u + d i)) σ := by + refine ⟨fun i ↦ (hF.isPhaseFunction i).comp (by fun_prop) (hmap i), ?_⟩ + intro p u + rw [VariableObject.IsInfinitesimal] + let v : ∀ i, phaseInterval := + fun i ↦ ⟨c i * (u i : ℝ) + d i, hmap i (u i).property⟩ + have herr := hF.error_isChoicewiseInfinitesimal p v + rw [VariableObject.IsInfinitesimal] at herr + have hcsub : Tendsto (fun i ↦ c i - 1) atTop (𝓝 0) := by + simpa using hc.sub + (tendsto_const_nhds : Tendsto (fun _ : ℕ ↦ (1 : ℝ)) atTop (𝓝 1)) + have huBounded : IsBoundedUnder (· ≤ ·) atTop + ((‖·‖) ∘ fun i ↦ (u i : ℝ)) := + Filter.isBoundedUnder_of_eventually_le <| Filter.Eventually.of_forall fun i ↦ by + rw [Function.comp_apply, Real.norm_eq_abs, abs_of_nonneg + (zero_le_one.trans (u i).property.1)] + exact (u i).property.2 + have hmul : Tendsto (fun i ↦ (c i - 1) * (u i : ℝ)) atTop (𝓝 0) := + hcsub.zero_mul_isBoundedUnder_le huBounded + have hvsub : Tendsto (fun i ↦ (v i : ℝ) - (u i : ℝ)) atTop (𝓝 0) := by + convert hmul.add hd using 1 + · ext i + dsimp [v] + ring_nf + · ring_nf + have hcpow : Tendsto (fun i ↦ c i ^ (p + 1)) atTop (𝓝 1) := by + simpa using hc.pow (p + 1) + have href := continuousOn_iteratedDerivWithin_modelPhase σ p + have hrefUniform := isCompact_Icc.uniformContinuousOn_of_continuous href + have hrefclose : Tendsto (fun i ↦ + iteratedDerivWithin p (modelPhase σ) phaseInterval (v i) - + iteratedDerivWithin p (modelPhase σ) phaseInterval (u i)) atTop (𝓝 0) := by + rw [Metric.uniformContinuousOn_iff] at hrefUniform + rw [Metric.tendsto_nhds] + intro ε hε + obtain ⟨δ, hδ, hclose⟩ := hrefUniform ε hε + have hevent : ∀ᶠ i in atTop, ‖(v i : ℝ) - (u i : ℝ)‖ < δ := by + simpa [Real.dist_eq] using (Metric.tendsto_nhds.1 hvsub) δ hδ + filter_upwards [hevent] with i hi + simpa [dist_eq_norm] using + hclose (v i) (v i).property (u i) (u i).property + (by simpa [Real.dist_eq] using hi) + have hzero : Tendsto (fun i ↦ c i ^ (p + 1) - 1) atTop (𝓝 0) := by + simpa using hcpow.sub + (tendsto_const_nhds : Tendsto (fun _ : ℕ ↦ (1 : ℝ)) atTop (𝓝 1)) + obtain ⟨D, hD⟩ := isCompact_Icc.exists_bound_of_continuousOn href + have hrefBounded : IsBoundedUnder (· ≤ ·) atTop + ((‖·‖) ∘ fun i ↦ + iteratedDerivWithin p (modelPhase σ) phaseInterval (v i)) := + Filter.isBoundedUnder_of_eventually_le <| Filter.Eventually.of_forall fun i ↦ + hD (v i) (v i).property + have hscale : Tendsto (fun i ↦ + (c i ^ (p + 1) - 1) * + iteratedDerivWithin p (modelPhase σ) phaseInterval (v i)) atTop (𝓝 0) := + hzero.zero_mul_isBoundedUnder_le hrefBounded + have hmajor : Tendsto (fun i ↦ + ‖c i ^ (p + 1)‖ * ‖modelPhaseErrorAt (F i) σ p (v i)‖ + + ‖(c i ^ (p + 1) - 1) * + iteratedDerivWithin p (modelPhase σ) phaseInterval (v i) + + (iteratedDerivWithin p (modelPhase σ) phaseInterval (v i) - + iteratedDerivWithin p (modelPhase σ) phaseInterval (u i))‖) + atTop (𝓝 0) := by + simpa using (hcpow.norm.mul herr).add (hscale.add hrefclose).norm + apply squeeze_zero' (g := fun i ↦ + ‖c i ^ (p + 1)‖ * ‖modelPhaseErrorAt (F i) σ p (v i)‖ + + ‖(c i ^ (p + 1) - 1) * + iteratedDerivWithin p (modelPhase σ) phaseInterval (v i) + + (iteratedDerivWithin p (modelPhase σ) phaseInterval (v i) - + iteratedDerivWithin p (modelPhase σ) phaseInterval (u i))‖) + · exact Filter.Eventually.of_forall fun _ ↦ norm_nonneg _ + · filter_upwards [] with i + change ‖modelPhaseErrorAt (fun x ↦ F i (c i * x + d i)) σ p (u i)‖ ≤ _ + rw [modelPhaseErrorAt, + iteratedDerivWithin_comp_affine_of_mapsTo (s := phaseInterval) (t := phaseInterval) + ((hF.isPhaseFunction i).of_le + (ENat.natCast_le_of_coe_top_le_withTop le_rfl (p + 1))) + uniqueDiffOn_phaseInterval uniqueDiffOn_phaseInterval (u i).property (hmap i)] + change ‖c i ^ (p + 1) * + iteratedDerivWithin (p + 1) (F i) phaseInterval (v i) - _‖ ≤ _ + rw [show iteratedDerivWithin (p + 1) (F i) phaseInterval (v i) = + modelPhaseErrorAt (F i) σ p (v i) + + iteratedDerivWithin p (modelPhase σ) phaseInterval (v i) by + simp [modelPhaseErrorAt]] + calc + _ = ‖c i ^ (p + 1) * modelPhaseErrorAt (F i) σ p (v i) + + ((c i ^ (p + 1) - 1) * + iteratedDerivWithin p (modelPhase σ) phaseInterval (v i) + + (iteratedDerivWithin p (modelPhase σ) phaseInterval (v i) - + iteratedDerivWithin p (modelPhase σ) phaseInterval (u i)))‖ := by + congr 1 + ring + _ ≤ ‖c i ^ (p + 1)‖ * ‖modelPhaseErrorAt (F i) σ p (v i)‖ + + ‖(c i ^ (p + 1) - 1) * + iteratedDerivWithin p (modelPhase σ) phaseInterval (v i) + + (iteratedDerivWithin p (modelPhase σ) phaseInterval (v i) - + iteratedDerivWithin p (modelPhase σ) phaseInterval (u i))‖ := by + simpa only [norm_mul] using norm_add_le + (c i ^ (p + 1) * modelPhaseErrorAt (F i) σ p (v i)) + ((c i ^ (p + 1) - 1) * + iteratedDerivWithin p (modelPhase σ) phaseInterval (v i) + + (iteratedDerivWithin p (modelPhase σ) phaseInterval (v i) - + iteratedDerivWithin p (modelPhase σ) phaseInterval (u i))) + _ = _ := by rfl + · exact hmajor + +/-- At every fixed finite order, fixed-exponent model-phase data is eventually a uniformly +approximate model phase. -/ +theorem IsModelPhaseFunctionWith.eventually_isApproximate + {F : VariableFunction (VariableObject.fixed ℝ) ℝ} {σ : ℝ} + (hF : IsModelPhaseFunctionWith F σ) (P : ℕ) {δ : ℝ} (hδ : 0 < δ) : + ∀ᶠ i in atTop, IsApproximateModelPhaseFunction (F i) σ P δ := by + have hp : ∀ p ∈ Finset.range (P + 1), ∀ᶠ i in atTop, + ∀ u : phaseInterval, ‖modelPhaseError F σ p i u‖ < δ := + fun p _ ↦ + (VariableFunction.isChoicewiseInfinitesimal_iff_forall_pos_uniform + (VariableObject.fixed phaseInterval) + (fun _ ↦ ⟨1, by simp [phaseInterval]⟩) + (modelPhaseError F σ p)).1 + (hF.error_isChoicewiseInfinitesimal p) δ hδ + have hall : + ∀ᶠ i in atTop, ∀ p ∈ Finset.range (P + 1), + ∀ u : phaseInterval, ‖modelPhaseError F σ p i u‖ < δ := + (Finset.range (P + 1)).eventually_all.mpr hp + filter_upwards [hall] with i hi + refine ⟨hF.isPhaseFunction i, ?_⟩ + intro p hp' u + exact (hi p (Finset.mem_range.mpr (by omega)) u).le -private lemma modelPhaseError_sum_isPointwiseInfinitesimal +private lemma modelPhaseError_sum_isChoicewiseInfinitesimal {F : VariableFunction (VariableObject.fixed ℝ) ℝ} {σ : ℝ} - (herror : ∀ p : ℕ, (modelPhaseError F σ p).IsPointwiseInfinitesimal) + (herror : ∀ p : ℕ, (modelPhaseError F σ p).IsChoicewiseInfinitesimal) (P : ℕ) : - VariableFunction.IsPointwiseInfinitesimal + VariableFunction.IsChoicewiseInfinitesimal ((fun i (u : phaseInterval) ↦ ∑ p ∈ Finset.range (P + 1), ‖modelPhaseError F σ p i u‖) : VariableFunction (VariableObject.fixed phaseInterval) ℝ) := by @@ -80,10 +386,10 @@ theorem IsModelPhaseFunction.exists_subsequence_uniform_error rcases hF with ⟨_, σ, hσ, herror⟩ let g : VariableFunction (VariableObject.fixed phaseInterval) ℝ := fun i u ↦ ∑ p ∈ Finset.range (P + 1), ‖modelPhaseError F σ p i u‖ - have hg : g.IsPointwiseInfinitesimal := - modelPhaseError_sum_isPointwiseInfinitesimal herror P + have hg : g.IsChoicewiseInfinitesimal := + modelPhaseError_sum_isChoicewiseInfinitesimal herror P obtain ⟨φ, hφ, c, hc, hbound⟩ := - automatic_uniformity_of_pointwise_infinitesimal + automatic_uniformity_of_choicewise_infinitesimal (E := VariableObject.fixed phaseInterval) (fun _ ↦ ⟨1, by simp [phaseInterval]⟩) g hg refine ⟨σ, hσ, φ, hφ, c, hc, ?_⟩ diff --git a/Expdb/ExponentialSums/ScaleTransfer.lean b/Expdb/ExponentialSums/ScaleTransfer.lean new file mode 100644 index 0000000..cc19b0c --- /dev/null +++ b/Expdb/ExponentialSums/ScaleTransfer.lean @@ -0,0 +1,305 @@ +module + +public import Expdb.ExponentialSums.FixedExponentialSum +public import Mathlib.Algebra.Order.Floor.Div +public import Mathlib.Analysis.Fourier.ZMod + +import Mathlib.Data.Nat.Cast.Order.Field + +/-! +# Finite scale transfer for exponential sums + +This module gives two ways to rewrite an exponential sum at a different length scale. Finite +Fourier inversion dilates a sum from scale `N` to `q * N`, while decomposition into residue +classes produces sums at scales approximately `N / q`. These identities are used to compare +the exponential-sum growth exponent at different values of `α`. +-/ + +@[expose] public section + +open scoped Expdb FourierTransform + +noncomputable section + +namespace Expdb + +/-! ## Finite Fourier orthogonality -/ + +private lemma sum_stdAddChar_mul_eq_ite (q m : ℕ) [NeZero q] : + (∑ h : ZMod q, ZMod.stdAddChar (h * (m : ZMod q))) = + if q ∣ m then (q : ℂ) else 0 := by + rw [AddChar.sum_mulShift (m : ZMod q) (ZMod.isPrimitive_stdAddChar q)] + simp only [ZMod.natCast_eq_zero_iff m q, ZMod.card] + split_ifs <;> norm_num + +private lemma stdAddChar_mul_nat_eq_fourierChar (q m : ℕ) [NeZero q] (h : ZMod q) : + ZMod.stdAddChar (h * (m : ZMod q)) = + (𝐞 ((h.val : ℝ) * (m : ℝ) / q) : ℂ) := by + rw [← h.natCast_zmod_val, ← Nat.cast_mul, ZMod.stdAddChar_apply, + ZMod.toCircle_natCast, Real.fourierChar_apply] + push_cast + rw [ZMod.val_natCast_of_lt h.val_lt] + congr 1 + ring_nf + +/-! ## Reindexing exponential sums -/ + +/-- Finite Fourier inversion expresses a sum at scale `N` as an average of sums dilated by `q`. -/ +lemma exponentialSumAt_dilate (F : ℝ → ℝ) (T N : ℝ) (a b q : ℕ) [NeZero q] + (hq : 0 < q) (hT : T ≠ 0) (hN : N ≠ 0) : + exponentialSumAt F T N a b = + (q : ℂ)⁻¹ * ∑ h : ZMod q, + exponentialSumAt (fun u ↦ F u + (h.val : ℝ) * N / T * u) + T (q * N) (q * a) (q * b) := by + rw [exponentialSumAt] + simp_rw [exponentialSumAt, oscillatory] + rw [Finset.sum_comm] + classical + symm + calc + (q : ℂ)⁻¹ * ∑ m ∈ Finset.Icc (q * a) (q * b), ∑ h : ZMod q, + (𝐞 (T * (F ((m : ℝ) / (q * N)) + + (h.val : ℝ) * N / T * ((m : ℝ) / (q * N)))) : ℂ) = + ∑ m ∈ Finset.Icc (q * a) (q * b), + (q : ℂ)⁻¹ * ((𝐞 (T * F ((m : ℝ) / (q * N))) : ℂ) * + ∑ h : ZMod q, ZMod.stdAddChar (h * (m : ZMod q))) := by + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro m hm + apply congrArg (fun z : ℂ ↦ (q : ℂ)⁻¹ * z) + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro h _ + have harg : + T * (F ((m : ℝ) / (q * N)) + + (h.val : ℝ) * N / T * ((m : ℝ) / (q * N))) = + T * F ((m : ℝ) / (q * N)) + (h.val : ℝ) * m / q := by + field_simp [show (q : ℝ) ≠ 0 by exact_mod_cast hq.ne', hT, hN] + rw [harg, AddChar.map_add_eq_mul, stdAddChar_mul_nat_eq_fourierChar] + exact Circle.coe_mul _ _ + _ = ∑ m ∈ Finset.Icc (q * a) (q * b), + if q ∣ m then (𝐞 (T * F ((m : ℝ) / (q * N))) : ℂ) else 0 := by + apply Finset.sum_congr rfl + intro m hm + rw [sum_stdAddChar_mul_eq_ite] + split_ifs with hdiv + · field_simp [show (q : ℂ) ≠ 0 by exact_mod_cast hq.ne'] + · simp + _ = ∑ n ∈ Finset.Icc a b, (𝐞 (T * F ((n : ℝ) / N)) : ℂ) := by + symm + rw [← Finset.sum_filter] + apply Finset.sum_bij (fun n _ ↦ q * n) + · intro n hn + simp only [Finset.mem_Icc] at hn + simp only [Finset.mem_filter, Finset.mem_Icc] + exact ⟨⟨Nat.mul_le_mul_left q hn.1, Nat.mul_le_mul_left q hn.2⟩, + dvd_mul_right q n⟩ + · intro n₁ hn₁ n₂ hn₂ heq + exact Nat.eq_of_mul_eq_mul_left hq heq + · intro m hm + simp only [Finset.mem_filter, Finset.mem_Icc] at hm + obtain ⟨n, rfl⟩ := hm.2 + refine ⟨n, ?_, rfl⟩ + simp only [Finset.mem_Icc] + constructor + · exact Nat.le_of_mul_le_mul_left hm.1.1 hq + · exact Nat.le_of_mul_le_mul_left hm.1.2 hq + · intro n hn + push_cast + congr 3 + field_simp [show (q : ℝ) ≠ 0 by exact_mod_cast hq.ne'] + +/-- Triangle-inequality form of `exponentialSumAt_dilate`. -/ +lemma norm_exponentialSumAt_dilate_le (F : ℝ → ℝ) (T N : ℝ) (a b q : ℕ) + [NeZero q] + (hq : 0 < q) (hT : T ≠ 0) (hN : N ≠ 0) : + ‖exponentialSumAt F T N a b‖ ≤ + ∑ h : ZMod q, + ‖exponentialSumAt (fun u ↦ F u + (h.val : ℝ) * N / T * u) + T (q * N) (q * a) (q * b)‖ / q := by + rw [exponentialSumAt_dilate F T N a b q hq hT hN, norm_mul, norm_inv, + Complex.norm_natCast] + calc + (q : ℝ)⁻¹ * ‖∑ h : ZMod q, + exponentialSumAt (fun u ↦ F u + (h.val : ℝ) * N / T * u) + T (q * N) (q * a) (q * b)‖ ≤ + (q : ℝ)⁻¹ * ∑ h : ZMod q, + ‖exponentialSumAt (fun u ↦ F u + (h.val : ℝ) * N / T * u) + T (q * N) (q * a) (q * b)‖ := + mul_le_mul_of_nonneg_left (norm_sum_le _ _) (by positivity) + _ = _ := by + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro h _ + simp only [div_eq_mul_inv] + ring + +/-- The scale induced by restricting a sum to the residue class `r mod q`. -/ +def residueScale (N : ℝ) (q r : ℕ) : ℝ := (N - r) / q + +/-- The affine phase induced by restricting a sum to the residue class `r mod q`. -/ +def residuePhase (F : ℝ → ℝ) (N : ℝ) (r : ℕ) : ℝ → ℝ := + fun u ↦ F ((1 - (r : ℝ) / N) * u + (r : ℝ) / N) + +/-- Evaluation of the residue-class phase at its rescaled integer arguments. -/ +lemma residuePhase_identity (F : ℝ → ℝ) (N : ℝ) (q r m : ℕ) + (hN : N ≠ 0) (hrN : (r : ℝ) < N) : + residuePhase F N r ((m : ℝ) / residueScale N q r) = + F (((q * m + r : ℕ) : ℝ) / N) := by + simp only [residuePhase, residueScale] + push_cast + field_simp [sub_ne_zero.mpr (ne_of_gt hrN)] + +/-- Reindex one residue class as an exponential sum with `residuePhase` and `residueScale`. -/ +lemma exponentialSumAt_residue (F : ℝ → ℝ) (T N : ℝ) (a b q r : ℕ) + (hq : 0 < q) (hr : r < q) (hra : r ≤ a) (hab : a ≤ b) + (hN : N ≠ 0) (hrN : (r : ℝ) < N) : + (∑ n ∈ Finset.Icc a b with n % q = r, oscillatory F T N n) = + exponentialSumAt (residuePhase F N r) T (residueScale N q r) + ((a - r) ⌈/⌉ q) ((b - r) / q) := by + rw [exponentialSumAt] + classical + symm + apply Finset.sum_bij (fun m _ ↦ q * m + r) + · intro m hm + simp only [Finset.mem_Icc] at hm + simp only [Finset.mem_filter, Finset.mem_Icc] + constructor + · constructor + · have ha : a - r ≤ q * m := + (ceilDiv_le_iff_le_mul hq).mp hm.1 + omega + · have hb : q * m ≤ b - r := by + simpa [Nat.mul_comm] using (Nat.le_div_iff_mul_le hq).mp hm.2 + omega + · simp [Nat.add_mod, Nat.mod_eq_of_lt hr] + · intro m₁ hm₁ m₂ hm₂ heq + exact Nat.eq_of_mul_eq_mul_left hq (Nat.add_right_cancel heq) + · intro n hn + simp only [Finset.mem_filter, Finset.mem_Icc] at hn + have hnrepr : n = q * (n / q) + r := by + have hnmod := hn.2 + have hdecomp := Nat.mod_add_div n q + omega + refine ⟨n / q, ?_, ?_⟩ + · simp only [Finset.mem_Icc] + constructor + · apply (ceilDiv_le_iff_le_mul hq).mpr + omega + · apply (Nat.le_div_iff_mul_le hq).mpr + rw [Nat.mul_comm] + omega + · exact hnrepr.symm + · intro m hm + simp only [oscillatory] + rw [residuePhase_identity F N q r m hN hrN] + +private lemma residue_upper_endpoint_le (N : ℝ) (b q r : ℕ) + (hq : 0 < q) (hr : r < q) (hb : (b : ℝ) ≤ 2 * N) : + (b - r) / q ≤ ⌊2 * residueScale N q r⌋₊ + 1 := by + by_cases hrb : r ≤ b + · have hdiv : (((b - r) / q : ℕ) : ℝ) < (2 * residueScale N q r) + 1 := by + have hnatdiv : (((b - r) / q : ℕ) : ℝ) ≤ ((b - r : ℕ) : ℝ) / q := + Nat.cast_div_le + refine lt_of_le_of_lt hnatdiv ?_ + simp only [residueScale] + rw [Nat.cast_sub hrb] + have hqR : (0 : ℝ) < q := by exact_mod_cast hq + have hrR : (r : ℝ) < q := by exact_mod_cast hr + rw [div_lt_iff₀ hqR] + field_simp [show (q : ℝ) ≠ 0 by positivity] + nlinarith + have hfloor := Nat.lt_floor_add_one (2 * residueScale N q r) + have hcast : (((b - r) / q : ℕ) : ℝ) < + ((⌊2 * residueScale N q r⌋₊ + 2 : ℕ) : ℝ) := by + push_cast + linarith + have hnat : (b - r) / q < ⌊2 * residueScale N q r⌋₊ + 2 := by + exact_mod_cast hcast + omega + · have hbr : b ≤ r := by omega + simp [Nat.sub_eq_zero_of_le hbr] + +/-- Split an exponential sum into residue classes, trimming each upper endpoint at a cost of at +most one term. -/ +lemma norm_exponentialSumAt_le_sum_residues + (F : ℝ → ℝ) (T N : ℝ) (a b q : ℕ) + (hq : 0 < q) (hqN : (q : ℝ) ≤ N) (hN : N ≠ 0) + (ha : N ≤ (a : ℝ)) (hb : (b : ℝ) ≤ 2 * N) : + ‖exponentialSumAt F T N a b‖ ≤ + ∑ r ∈ Finset.range q, + (‖exponentialSumAt (residuePhase F N r) T (residueScale N q r) + ((a - r) ⌈/⌉ q) + (min ((b - r) / q) ⌊2 * residueScale N q r⌋₊)‖ + 1) := by + by_cases hab : a ≤ b + swap + · rw [exponentialSumAt, Finset.Icc_eq_empty hab] + simp only [Finset.sum_empty, norm_zero] + apply Finset.sum_nonneg + intro r _ + exact add_nonneg (norm_nonneg (exponentialSumAt + (residuePhase F N r) T (residueScale N q r) + ((a - r) ⌈/⌉ q) (min ((b - r) / q) ⌊2 * residueScale N q r⌋₊))) zero_le_one + rw [exponentialSumAt] + classical + have hpartition : + ∑ n ∈ Finset.Icc a b, oscillatory F T N n = + ∑ r ∈ Finset.range q, + ∑ n ∈ Finset.Icc a b with n % q = r, oscillatory F T N n := by + rw [Finset.sum_fiberwise_of_maps_to] + intro n hn + exact Finset.mem_range.mpr (Nat.mod_lt n hq) + rw [hpartition] + calc + ‖∑ r ∈ Finset.range q, ∑ n ∈ Finset.Icc a b with n % q = r, + oscillatory F T N n‖ ≤ + ∑ r ∈ Finset.range q, + ‖∑ n ∈ Finset.Icc a b with n % q = r, oscillatory F T N n‖ := + norm_sum_le _ _ + _ ≤ _ := by + apply Finset.sum_le_sum + intro r hr + have hrq := Finset.mem_range.mp hr + have hrN : (r : ℝ) < N := lt_of_lt_of_le (by exact_mod_cast hrq) hqN + have hra : r ≤ a := by + have : (r : ℝ) < a := hrN.trans_le ha + exact_mod_cast this.le + rw [exponentialSumAt_residue F T N a b q r hq hrq hra hab hN hrN] + let A := (a - r) ⌈/⌉ q + let B := (b - r) / q + let B' := min B ⌊2 * residueScale N q r⌋₊ + have hBB' : B ≤ B' + 1 := by + dsimp [B, B'] + have hend := residue_upper_endpoint_le N b q r hq hrq hb + rw [min_def] + split_ifs <;> omega + rw [exponentialSumAt] + change ‖∑ n ∈ Finset.Icc A B, + oscillatory (residuePhase F N r) T (residueScale N q r) n‖ ≤ + ‖∑ n ∈ Finset.Icc A B', + oscillatory (residuePhase F N r) T (residueScale N q r) n‖ + 1 + by_cases hAB0 : A ≤ B + swap + · rw [Finset.Icc_eq_empty hAB0] + simp only [Finset.sum_empty, norm_zero] + positivity + by_cases hle : B ≤ B' + · have : B = B' := le_antisymm hle (min_le_left _ _) + rw [this] + exact le_add_of_nonneg_right (by norm_num) + · have hsucc : B = B' + 1 := by omega + by_cases hAB : A ≤ B' + · rw [hsucc, Finset.sum_Icc_succ_top (hAB.trans (Nat.le_succ _))] + calc + _ ≤ ‖∑ n ∈ Finset.Icc A B', + oscillatory (residuePhase F N r) T (residueScale N q r) n‖ + + ‖oscillatory (residuePhase F N r) T (residueScale N q r) + ((B' + 1 : ℕ) : ℝ)‖ := + norm_add_le _ _ + _ = _ := by + rw [norm_oscillatory] + · have hAeq : A = B' + 1 := by omega + rw [hAeq, hsucc] + simp [norm_oscillatory] + +end Expdb diff --git a/Expdb/ExponentialSums/TrivialBounds.lean b/Expdb/ExponentialSums/TrivialBounds.lean index eecd983..77d0dca 100644 --- a/Expdb/ExponentialSums/TrivialBounds.lean +++ b/Expdb/ExponentialSums/TrivialBounds.lean @@ -38,18 +38,27 @@ namespace Expdb /-! ## Choosing the Euler–Maclaurin order -/ -private lemma exists_oscillatory_scale_parameters - {δ : ℝ} (hδ : 0 < δ) : - ∃ s : ℕ, ∃ q : ℝ, - 1 ≤ s ∧ 0 < q ∧ q ≤ δ ∧ - q * (s + 1 : ℕ) = δ / 2 ∧ - 1 + δ / 2 ≤ (s : ℝ) * δ := by - obtain ⟨s, hs⟩ := exists_nat_ge ((1 + δ / 2) / δ) +/-- Parameters making the two Euler–Maclaurin remainder terms small at a power scale. -/ +private structure OscillatoryScaleParameters (δ : ℝ) where + order : ℕ + exponent : ℝ + one_le_order : 1 ≤ order + exponent_pos : 0 < exponent + exponent_le : exponent ≤ δ + exponent_mul_order_succ : exponent * (order + 1 : ℕ) = δ / 2 + one_add_half_le_order_mul : 1 + δ / 2 ≤ (order : ℝ) * δ + +private noncomputable def oscillatoryScaleParameters + {δ : ℝ} (hδ : 0 < δ) : OscillatoryScaleParameters δ := by + let hs_exists := exists_nat_ge ((1 + δ / 2) / δ) + let s : ℕ := Classical.choose hs_exists + have hs : (1 + δ / 2) / δ ≤ s := + Classical.choose_spec hs_exists have hsone : 1 ≤ s := by by_contra hs0 - have : s = 0 := by omega - subst s - norm_num at hs + have hs_eq : s = 0 := by omega + have hs_cast : (s : ℝ) = 0 := by exact_mod_cast hs_eq + rw [hs_cast] at hs have : 0 < (1 + δ / 2) / δ := by positivity linarith let q : ℝ := δ / (2 * (s + 1 : ℕ)) @@ -65,16 +74,21 @@ private lemma exists_oscillatory_scale_parameters field_simp have hsδ : 1 + δ / 2 ≤ (s : ℝ) * δ := (div_le_iff₀ hδ).1 (by simpa [mul_comm] using hs) - exact ⟨s, q, hsone, hq, hqδ, hqmul, hsδ⟩ + exact + { order := s + exponent := q + one_le_order := hsone + exponent_pos := hq + exponent_le := hqδ + exponent_mul_order_succ := hqmul + one_add_half_le_order_mul := hsδ } -private lemma oscillatory_scale_bounds - {s : ℕ} {δ q K T N : ℝ} +private lemma OscillatoryScaleParameters.hasSmallEulerMaclaurinRemainder + {δ K T N : ℝ} (params : OscillatoryScaleParameters δ) (hT : 1 ≤ T) (hN : 1 ≤ N) (hK : 1 ≤ K) - (hqδ : q ≤ δ) - (hqmul : q * (s + 1 : ℕ) = δ / 2) - (hsδ : 1 + δ / 2 ≤ (s : ℝ) * δ) - (hKpower : K ≤ T ^ q) (hNlower : T ^ (δ + 1) ≤ N) : - K * T / N ≤ 1 ∧ N * (K * T / N) ^ (s + 1) ≤ 1 := by + (hKpower : K ≤ T ^ params.exponent) (hNlower : T ^ (δ + 1) ≤ N) : + HasSmallEulerMaclaurinRemainder params.order T N K := by + rcases params with ⟨s, q, hs, hq, hqδ, hqmul, hsδ⟩ have hTpos : 0 < T := zero_lt_one.trans_le hT have hNpos : 0 < N := zero_lt_one.trans_le hN have hKpow : K ^ (s + 1) ≤ T ^ (δ / 2) := by @@ -134,36 +148,40 @@ private theorem exponentSumGrowthExponent_le_sub_one have hηc : η ≤ min c 1 := (min_le_right _ _).trans (min_le_right _ _) let δ : ℝ := (α : ℝ) - η - 1 have hδ : 0 < δ := by dsimp [δ]; linarith - obtain ⟨s, q, hs, hq, hqδ, hqmul, hsδ⟩ := - exists_oscillatory_scale_parameters hδ - obtain ⟨K, hK, hphaseBounds⟩ := approximate_model_phase_deriv_bounds hσ s - obtain ⟨M, hMone, hsumBound⟩ := exists_norm_oscillatory_sum_le s hs hK hc + let params := oscillatoryScaleParameters hδ + obtain ⟨K, hK, hphaseBounds⟩ := + approximate_model_phase_deriv_bounds hσ params.order + obtain ⟨M, hMone, hsumBound⟩ := + exists_norm_oscillatory_sum_le params.order params.one_le_order hK hc have hM : 0 ≤ M := zero_le_one.trans hMone - let C : ℝ := max 1 (max (2 * M) (K ^ q⁻¹)) + let C : ℝ := max 1 (max (2 * M) (K ^ params.exponent⁻¹)) have hC : 1 ≤ C := le_max_left _ _ - refine ⟨η, hη, s, hs, C, hC, ?_⟩ - intro T N F a b hTC hNlower hNupper hF ha hb + refine ⟨η, hη, params.order, params.one_le_order, C, hC, ?_⟩ + intro T N F a b hsetup + obtain ⟨hTC, hNlower, hNupper, hF, ha, hb⟩ := hsetup have hTone : 1 ≤ T := hC.trans hTC have hTpos : 0 < T := zero_lt_one.trans_le hTone have hNone : 1 ≤ N := by calc 1 ≤ T ^ ((α : ℝ) - η) := Real.one_le_rpow hTone (by linarith) _ ≤ N := hNlower - have hKbase : K ^ q⁻¹ ≤ T := by + have hKbase : K ^ params.exponent⁻¹ ≤ T := by calc - K ^ q⁻¹ ≤ max (2 * M) (K ^ q⁻¹) := le_max_right _ _ + K ^ params.exponent⁻¹ ≤ max (2 * M) (K ^ params.exponent⁻¹) := le_max_right _ _ _ ≤ C := le_max_right _ _ _ ≤ T := hTC - have hKpower : K ≤ T ^ q := by + have hKpower : K ≤ T ^ params.exponent := by calc - K = (K ^ q⁻¹) ^ q := by - rw [← Real.rpow_mul (zero_le_one.trans hK), inv_mul_cancel₀ hq.ne', Real.rpow_one] - _ ≤ T ^ q := Real.rpow_le_rpow (Real.rpow_nonneg (zero_le_one.trans hK) _) - hKbase hq.le + K = (K ^ params.exponent⁻¹) ^ params.exponent := by + rw [← Real.rpow_mul (zero_le_one.trans hK), + inv_mul_cancel₀ params.exponent_pos.ne', Real.rpow_one] + _ ≤ T ^ params.exponent := + Real.rpow_le_rpow (Real.rpow_nonneg (zero_le_one.trans hK) _) + hKbase params.exponent_pos.le have hNscale : T ^ (δ + 1) ≤ N := by simpa only [δ, sub_add_cancel] using hNlower - obtain ⟨hratio, hremainder⟩ := oscillatory_scale_bounds - hTone hNone hK hqδ hqmul hsδ hKpower hNscale + have hscale := params.hasSmallEulerMaclaurinRemainder + hTone hNone hK hKpower hNscale obtain ⟨hfirst, hderiv⟩ := hphaseBounds hηc hF have htargetNonneg : 0 ≤ (α : ℝ) - 1 + ε := by linarith have hNTdiv : N / T ≤ T ^ ((α : ℝ) - 1 + ε) := by @@ -178,18 +196,17 @@ private theorem exponentSumGrowthExponent_le_sub_one have hone : 1 ≤ T ^ ((α : ℝ) - 1 + ε) := Real.one_le_rpow hTone htargetNonneg have hCM : 2 * M ≤ C := (le_max_left _ _).trans (le_max_right _ _) by_cases hab : a ≤ b - · have hsum := hsumBound hab hNone hTone hF.1 - (fun u hu ↦ hfirst u hu) hderiv ha hb hratio hremainder + · have hsum := hsumBound hab hNone hTone hF.1 hfirst hderiv ha hb hscale change ‖exponentialSumAt F T N a b‖ ≤ C * T ^ ((α : ℝ) - 1 + ε) calc ‖exponentialSumAt F T N a b‖ ≤ M * (1 + N / T) := by - simpa only [exponentialSumAt] using hsum + exact hsum _ ≤ M * (2 * T ^ ((α : ℝ) - 1 + ε)) := by gcongr linarith _ = (2 * M) * T ^ ((α : ℝ) - 1 + ε) := by ring _ ≤ C * T ^ ((α : ℝ) - 1 + ε) := by gcongr - · rw [exponentialSumAt, Finset.Icc_eq_empty hab, Finset.sum_empty, norm_zero] + · rw [exponentialSumAt_of_lt (lt_of_not_ge hab), norm_zero] exact mul_nonneg (zero_le_one.trans hC) (Real.rpow_nonneg hTpos.le _) /-! ## The matching logarithmic lower bound for `α > 1` -/ @@ -203,21 +220,21 @@ theorem exists_norm_logPhase_sum_sub_mainTerm_le (s : ℕ) : ∀ {N T : ℝ} {a b : ℕ}, a < b → 1 ≤ N → 1 ≤ T → (a : ℝ) = N → (b : ℝ) = 2 * N → - K * T / N ≤ 1 → N * (K * T / N) ^ (s + 1) ≤ 1 → - ‖(∑ n ∈ Finset.Icc a b, (𝐞 (T * Real.log ((n : ℝ) / N)) : ℂ)) - - logPhaseMainTerm N T‖ ≤ C := by + HasSmallEulerMaclaurinRemainder s T N K → + ‖exponentialSumAt Real.log T N a b - logPhaseMainTerm N T‖ ≤ C := by obtain ⟨K, hK, hphaseBounds⟩ := approximate_model_phase_deriv_bounds zero_lt_one s obtain ⟨_, hderiv⟩ := hphaseBounds (δ := 0) (F := Real.log) (by norm_num) (isApproximateModelPhaseFunction_log s) obtain ⟨C, hC, herror⟩ := exists_norm_oscillatory_sum_sub_integral_le s refine ⟨K, C, hK, hC, ?_⟩ - intro N T a b hab hN hT ha hb hratio hremainder + intro N T a b hab hN hT ha hb hscale have herr := herror hab hN hT hK (isModelPhaseFunction_log.1 0) hderiv (by exact_mod_cast ha.ge) - (by exact_mod_cast hb.le) hratio hremainder - have hint : (∫ x in (a : ℝ)..b, - (𝐞 (T * Real.log (x / N)) : ℂ)) = logPhaseMainTerm N T := by - rw [ha, hb] + (by exact_mod_cast hb.le) hscale + have hint : (∫ x in (a : ℝ)..b, oscillatory Real.log T N x) = + logPhaseMainTerm N T := by + rw [show (fun x ↦ oscillatory Real.log T N x) = + fun x ↦ (𝐞 (T * Real.log (x / N)) : ℂ) from rfl, ha, hb] exact logPhase_integral_eq_mainTerm (zero_lt_one.trans_le hN) simp only [logPhase] at herr rw [hint] at herr @@ -229,8 +246,7 @@ private theorem sub_one_le_exponentSumGrowthExponent have hαR : (1 : ℝ) < α := by exact_mod_cast hα let δ : ℝ := (α : ℝ) - 1 have hδ : 0 < δ := by dsimp [δ]; linarith - obtain ⟨s, q, hsone, hq, hqδ, hqmul, hsδ⟩ := - exists_oscillatory_scale_parameters hδ + let params := oscillatoryScaleParameters hδ let N : VariableObject ℝ := fun i ↦ (i : ℝ) + 1 let T : VariableObject ℝ := fun i ↦ N i ^ ((α : ℝ)⁻¹) let a : VariableObject ℕ := fun i ↦ i + 1 @@ -247,11 +263,9 @@ private theorem sub_one_le_exponentSumGrowthExponent exact tendsto_atTop_add_const_right atTop 1 tendsto_natCast_atTop_atTop have hTtop : Tendsto T atTop atTop := (tendsto_rpow_atTop (inv_pos.mpr (zero_lt_one.trans hαR))).comp hNtop - have hTunbounded : T.IsUnbounded := by - rw [VariableObject.IsUnbounded] - convert hTtop using 1 - ext i - rw [Real.norm_eq_abs, abs_of_nonneg (le_trans zero_le_one (hT i))] + have hTunbounded : T.IsUnbounded := + (VariableObject.isUnbounded_iff_tendsto_atTop + fun i ↦ zero_le_one.trans (hT i)).2 hTtop have hNTexact (i : ℕ) : N i = T i ^ (α : ℝ) := by dsimp [T] rw [← Real.rpow_mul (le_trans zero_le_one (hN i)), @@ -265,11 +279,10 @@ private theorem sub_one_le_exponentSumGrowthExponent dsimp [N, a, b] push_cast exact ⟨le_rfl, le_rfl⟩ - have hbound := isPowerBounded_logPhase α hN hT hTunbounded hNT hab obtain ⟨K, E, hK, hEone, hlogEstimate⟩ := - exists_norm_logPhase_sum_sub_mainTerm_le s - have hKpower : ∀ᶠ i in atTop, K ≤ T i ^ q := - tendsto_atTop.1 ((tendsto_rpow_atTop hq).comp hTtop) K + exists_norm_logPhase_sum_sub_mainTerm_le params.order + have hKpower : ∀ᶠ i in atTop, K ≤ T i ^ params.exponent := + tendsto_atTop.1 ((tendsto_rpow_atTop params.exponent_pos).comp hTtop) K let d : ℝ := 1 / (1 + 2 * Real.pi) have hd : 0 < d := by dsimp [d]; positivity have hE : 0 ≤ E := zero_le_one.trans hEone @@ -288,12 +301,12 @@ private theorem sub_one_le_exponentSumGrowthExponent congr 1 dsimp [δ] ring - obtain ⟨hratio, hremainder⟩ := oscillatory_scale_bounds - (hT i) (hN i) hK hqδ hqmul hsδ hiK hNscale + have hscale := params.hasSmallEulerMaclaurinRemainder + (hT i) (hN i) hK hiK hNscale have hablt : a i < b i := by dsimp [a, b]; omega have haeq : (a i : ℝ) = N i := by dsimp [N, a]; push_cast; ring have hbeq : (b i : ℝ) = 2 * N i := by dsimp [N, b]; push_cast; ring - have herr := hlogEstimate hablt (hN i) (hT i) haeq hbeq hratio hremainder + have herr := hlogEstimate hablt (hN i) (hT i) haeq hbeq hscale have hInt := (norm_logPhaseMainTerm_bounds hNi (hT i)).1 have hpower : N i / T i = T i ^ ((α : ℝ) - 1) := by rw [hNTexact] @@ -309,15 +322,15 @@ private theorem sub_one_le_exponentSumGrowthExponent norm_le_norm_add_norm_sub _ _ _ ≤ ‖exponentialSum logPhase T N a b i‖ + E := by gcongr - simpa only [exponentialSum, logPhase] using herr + simpa only [exponentialSum_apply, logPhase] using herr have hEsmall : E ≤ d / 2 * T i ^ ((α : ℝ) - 1) := by calc E = d / 2 * (2 * E / d) := by field_simp [hd.ne'] _ ≤ d / 2 * T i ^ ((α : ℝ) - 1) := mul_le_mul_of_nonneg_left hiSmall (by positivity) linarith - exact exponent_le_of_isPowerBounded_of_eventually_norm_ge_rpow - hT hTunbounded hbound (half_pos hd) (by simpa [d] using hlower) + exact le_exponentSumGrowthExponent_of_logPhase_lower_bound α hN hT hTunbounded hNT hab + (half_pos hd) (by simpa [d] using hlower) /-! ## The `L²` lower bound for `0 < α ≤ 1` -/ @@ -327,8 +340,7 @@ private theorem exists_logPhase_sum_norm_sq_ge : 0 < R → 0 < N → N ≤ a → (b : ℝ) ≤ 2 * N → N ≤ R / (4 * C) → ∃ t ∈ Set.Icc R (2 * R), ((Finset.Icc a b).card : ℝ) / 2 ≤ - ‖∑ n ∈ Finset.Icc a b, - (𝐞 (t * Real.log ((n : ℝ) / N)) : ℂ)‖ ^ 2 := by + ‖exponentialSumAt Real.log t N a b‖ ^ 2 := by obtain ⟨C₀, hC₀, hlarge⟩ := l2_integral_estimate_exists_norm_sq_ge refine ⟨C₀, hC₀, ?_⟩ intro R N a b hR hN ha hb hNR @@ -346,8 +358,8 @@ private theorem exists_logPhase_sum_norm_sq_ge : simp [coeff] rw [hmass] at htlarge refine ⟨t, ht, ?_⟩ - rw [Finset.sum_subtype (Finset.Icc a b) (fun _ ↦ Iff.rfl)] - simpa only [coeff, ξ, one_mul, mul_comm] using htlarge + rw [exponentialSumAt, Finset.sum_subtype (Finset.Icc a b) (fun _ ↦ Iff.rfl)] + simpa only [expSum, oscillatory, coeff, ξ, one_mul, mul_comm] using htlarge private theorem half_le_exponentSumGrowthExponent {α : ℝ≥0} (hα : 0 < α) (hαone : α ≤ 1) : @@ -385,8 +397,7 @@ private theorem half_le_exponentSumGrowthExponent _ ≤ D * N i ^ (α : ℝ)⁻¹ := mul_le_mul_of_nonneg_left hpow hDpos.le have hgood (i : ℕ) : ∃ t ∈ Set.Icc (R i) (2 * R i), ((Finset.Icc (a i) (b i)).card : ℝ) / 2 ≤ - ‖∑ m ∈ Finset.Icc (a i) (b i), - (𝐞 (t * Real.log ((m : ℝ) / N i)) : ℂ)‖ ^ 2 := by + ‖exponentialSumAt Real.log t (N i) (a i) (b i)‖ ^ 2 := by apply hlarge (mul_pos hDpos (Real.rpow_pos_of_pos (hNpos i) _)) (hNpos i) · dsimp [N, a, n] norm_num @@ -397,8 +408,7 @@ private theorem half_le_exponentSumGrowthExponent let T : VariableObject ℝ := fun i ↦ (hgood i).choose have hTmem (i : ℕ) : T i ∈ Set.Icc (R i) (2 * R i) := (hgood i).choose_spec.1 have hTsquare (i : ℕ) : ((Finset.Icc (a i) (b i)).card : ℝ) / 2 ≤ - ‖∑ m ∈ Finset.Icc (a i) (b i), - (𝐞 (T i * Real.log ((m : ℝ) / N i)) : ℂ)‖ ^ 2 := + ‖exponentialSumAt Real.log (T i) (N i) (a i) (b i)‖ ^ 2 := (hgood i).choose_spec.2 have hTbounds (i : ℕ) : D * N i ^ (α : ℝ)⁻¹ ≤ T i ∧ T i ≤ 2 * (D * N i ^ (α : ℝ)⁻¹) := by @@ -413,11 +423,9 @@ private theorem half_le_exponentSumGrowthExponent exact (tendsto_rpow_atTop (inv_pos.mpr hαR)).comp hNtop |>.const_mul_atTop hDpos have hTtop : Tendsto T atTop atTop := tendsto_atTop_mono' atTop (Filter.Eventually.of_forall fun i ↦ (hTmem i).1) hRtop - have hTunbounded : T.IsUnbounded := by - rw [VariableObject.IsUnbounded] - convert hTtop using 1 - ext i - rw [Real.norm_eq_abs, abs_of_nonneg (zero_le_one.trans (hT i))] + have hTunbounded : T.IsUnbounded := + (VariableObject.isUnbounded_iff_tendsto_atTop + fun i ↦ zero_le_one.trans (hT i)).2 hTtop have hNT : IsPowerAsymptotic N T (α : ℝ) := isPowerAsymptotic_of_between_const_rpow (A := D) (B := 2 * D) hαR (zero_lt_one.trans_le hD) (mul_pos (by norm_num) (zero_lt_one.trans_le hD)) hNtop @@ -428,8 +436,6 @@ private theorem half_le_exponentSumGrowthExponent dsimp [N, a, b, n] push_cast exact ⟨le_rfl, le_rfl⟩ - have hbound := isPowerBounded_logPhase α (fun i ↦ (hN i).trans' one_le_two) - hT hTunbounded hNT hab let L : ℝ := (2 * D) ^ ((α : ℝ) / 2) have hL : 0 < L := Real.rpow_pos_of_pos (mul_pos (by norm_num) hDpos) _ have hlower : ∀ᶠ i in atTop, @@ -447,7 +453,7 @@ private theorem half_le_exponentSumGrowthExponent calc N i / 2 ≤ ((Finset.Icc (a i) (b i)).card : ℝ) / 2 := by gcongr _ ≤ ‖exponentialSum logPhase T N a b i‖ ^ 2 := by - simpa only [exponentialSum, logPhase] using hTsquare i + simpa only [exponentialSum_apply, logPhase] using hTsquare i have hrootSquare : (N i ^ (1 / 2 : ℝ)) ^ 2 = N i := by rw [← Real.rpow_natCast] rw [← Real.rpow_mul (hNpos i).le] @@ -474,16 +480,18 @@ private theorem half_le_exponentSumGrowthExponent (1 / (2 * L)) * (L * N i ^ (1 / 2 : ℝ)) := by gcongr _ = N i ^ (1 / 2 : ℝ) / 2 := by field_simp [hL.ne'] _ ≤ ‖exponentialSum logPhase T N a b i‖ := hroot - exact exponent_le_of_isPowerBounded_of_eventually_norm_ge_rpow - hT hTunbounded hbound (by positivity) hlower + exact le_exponentSumGrowthExponent_of_logPhase_lower_bound α + (fun i ↦ (hN i).trans' one_le_two) hT hTunbounded hNT hab (by positivity) hlower /-! ## Trivial bounds -/ -private theorem exponentSumGrowthExponent_nonneg (α : ℝ≥0) : +/-- The exponential-sum growth exponent is nonnegative. -/ +theorem exponentSumGrowthExponent_nonneg (α : ℝ≥0) : 0 ≤ exponentSumGrowthExponent α := (isExponentSumBound_exponentSumGrowthExponent α).nonneg -private theorem exponentSumGrowthExponent_le_self (α : ℝ≥0) : +/-- The triangle inequality bounds the growth exponent by the scale exponent. -/ +theorem exponentSumGrowthExponent_le_self (α : ℝ≥0) : exponentSumGrowthExponent α ≤ (α : ℝ) := exponentSumGrowthExponent_le_iff.mpr (isExponentSumBound_self α) diff --git a/Expdb/ExponentialSums/UpperSemicontinuity.lean b/Expdb/ExponentialSums/UpperSemicontinuity.lean new file mode 100644 index 0000000..c81e8c9 --- /dev/null +++ b/Expdb/ExponentialSums/UpperSemicontinuity.lean @@ -0,0 +1,478 @@ +module + +public import Expdb.ExponentialSums.TrivialBounds + +import Expdb.ExponentialSums.ExponentSumGrowthNonAsymptotic +import Expdb.ExponentialSums.ScaleTransfer +import Mathlib.Data.Finset.Max +import Mathlib.Topology.Semicontinuity.Basic + +/-! +# Upper semicontinuity of the exponential-sum growth exponent + +This file proves the upper semicontinuity assertion in the blueprint. The main input is scale +transference: dilation and finite Fourier inversion increase the scale, while decomposition into +residue classes decreases it. Both operations preserve the fixed model order of the phase. +-/ + +@[expose] public section + +open Filter Topology +open scoped ContDiff Expdb FourierTransform NNReal + +noncomputable section + +namespace Expdb + +/-! ## Scale transference -/ + +/-- On the subcritical interval, the exponential-sum growth exponent is monotone. -/ +theorem exponentSumGrowthExponent_monoOn_Icc : + MonotoneOn exponentSumGrowthExponent (Set.Icc 0 1) := by + intro α hα γ hγ hαγ + by_cases heq : α = γ + · simp [heq] + have hlt : (α : ℝ) < (γ : ℝ) := by exact_mod_cast lt_of_le_of_ne hαγ heq + rw [exponentSumGrowthExponent_le_iff] + intro N T F a b hN hT hTunbounded hNT hF hab + apply (isPowerBounded_iff_forall_pos _ T _ hT hTunbounded).mpr + intro ε hε + obtain ⟨hphase, σ, hσ, herror⟩ := hF + obtain ⟨δ, hδ, P, hP, C, hC, hfixed⟩ := + (exponentSumGrowthExponent_le_iff_nonAsymptotic.mp + (le_rfl : exponentSumGrowthExponent γ ≤ exponentSumGrowthExponent γ)) + (ε / 2) (by linarith) σ hσ + let η : ℝ := min (δ / 4) (((γ : ℝ) - (α : ℝ)) / 2) + have hη : 0 < η := by dsimp [η]; positivity + have hηδ : η < δ := lt_of_le_of_lt (min_le_left _ _) (by linarith) + let κ : ℝ := (γ : ℝ) - (α : ℝ) - η + have hκ : 0 < κ := by + dsimp [κ, η] + have := min_le_right (δ / 4) (((γ : ℝ) - (α : ℝ)) / 2) + linarith + let q : VariableObject ℕ := floorRpow T κ + let Q : VariableObject ℝ := fun i ↦ (q i : ℝ) + let M : VariableObject ℝ := Q * N + have hTtop : Tendsto T atTop atTop := + (VariableObject.isUnbounded_iff_tendsto_atTop + (fun i ↦ zero_le_one.trans (hT i))).mp hTunbounded + have hQasym : IsPowerAsymptotic Q T κ := + isPowerAsymptotic_floorRpow hκ hT hTunbounded + have hMasym0 : IsPowerAsymptotic M T (κ + (α : ℝ)) := hQasym.mul hNT hT + have hMasym : IsPowerAsymptotic M T ((γ : ℝ) - η) := by + convert hMasym0 using 1 + dsimp [κ] + ring + have hMdivAsym : IsPowerAsymptotic (M / T) T ((γ : ℝ) - η - 1) := by + apply hMasym.div + · refine ⟨VariableObject.fixed 1, IsEqUpToInfinitesimal.refl _, ?_⟩ + exact Filter.Eventually.of_forall fun i ↦ by simp [VariableObject.fixed] + · exact hT + have hMdivZero : Tendsto (M / T) atTop (𝓝 0) := by + apply hMdivAsym.tendsto_zero_of_neg + · have hγone : (γ : ℝ) ≤ 1 := by exact_mod_cast hγ.2 + linarith + · exact hT + · exact hTunbounded + have hFapprox : ∀ᶠ i in atTop, + IsApproximateModelPhaseFunction (F i) σ P (δ / 2) := + (IsModelPhaseFunctionWith.mk hphase herror).eventually_isApproximate P (by linarith) + have hMdivSmall : ∀ᶠ i in atTop, M i / T i ≤ δ / 2 := by + have hnear := (Metric.tendsto_nhds.1 hMdivZero) (δ / 2) (by linarith) + filter_upwards [hnear] with i hi + have hMnonneg : 0 ≤ M i := by + change 0 ≤ (q i : ℝ) * N i + exact mul_nonneg (Nat.cast_nonneg _) (zero_le_one.trans (hN i)) + rw [dist_zero_right] at hi + change |M i / T i| < δ / 2 at hi + rw [abs_of_nonneg (div_nonneg hMnonneg (zero_le_one.trans (hT i)))] at hi + exact hi.le + classical + have hMbetween := hMasym.eventually_between + (Filter.Eventually.of_forall hT) (sub_pos.mpr hηδ) + have hthreshold : ∀ᶠ i in atTop, C ≤ T i := + hTtop.eventually (eventually_ge_atTop C) + refine Asymptotics.IsBigO.of_bound C ?_ + filter_upwards [hFapprox, hMdivSmall, hMbetween, hthreshold] + with i hiF hiMsmall hiM hiC + have hqi : 0 < q i := floorRpow_pos T κ i + letI : NeZero (q i) := ⟨hqi.ne'⟩ + have hMi : 1 ≤ M i := by + dsimp [M, Q] + have hqone : (1 : ℝ) ≤ q i := by exact_mod_cast (Nat.succ_le_iff.mp hqi) + nlinarith [hN i] + have hMbounds : T i ^ ((γ : ℝ) - δ) ≤ M i ∧ M i ≤ T i ^ ((γ : ℝ) + δ) := by + constructor + · convert hiM.1 using 1 + congr 1 + ring + · exact hiM.2.trans (Real.rpow_le_rpow_of_exponent_le (hT i) (by linarith)) + have hinterval : M i ≤ ((q i * a i : ℕ) : ℝ) ∧ + ((q i * b i : ℕ) : ℝ) ≤ 2 * M i := by + dsimp [M, Q] + push_cast + constructor <;> nlinarith [hqi.le, (hab i).1, (hab i).2] + have hcoeffBound (k : ZMod (q i)) : + ‖(k.val : ℝ) * N i / T i‖ ≤ M i / T i := by + have hval : (k.val : ℝ) ≤ q i := by exact_mod_cast k.val_lt.le + dsimp [M, Q] + rw [abs_of_nonneg] + · exact div_le_div_of_nonneg_right + (mul_le_mul_of_nonneg_right hval (zero_le_one.trans (hN i))) + (zero_le_one.trans (hT i)) + · exact div_nonneg + (mul_nonneg (Nat.cast_nonneg _) (zero_le_one.trans (hN i))) + (zero_le_one.trans (hT i)) + have hphaseBound (k : ZMod (q i)) : + ‖exponentialSumAt + (fun u ↦ F i u + (k.val : ℝ) * N i / T i * u) + (T i) (M i) (q i * a i) (q i * b i)‖ ≤ + C * T i ^ (exponentSumGrowthExponent γ + ε / 2) := by + have hiG : IsApproximateModelPhaseFunction + (fun u ↦ F i u + (k.val : ℝ) * N i / T i * u) σ P δ := by + have hk := hiF.add_linear ((hcoeffBound k).trans hiMsmall) + convert hk using 1 + ring + exact hfixed (T i) (M i) _ (q i * a i) (q i * b i) + ⟨hiC, hMbounds.1, hMbounds.2, hiG, hinterval.1, hinterval.2⟩ + have hdilate := norm_exponentialSumAt_dilate_le (F i) (T i) (N i) + (a i) (b i) (q i) hqi (ne_of_gt (zero_lt_one.trans_le (hT i))) + (ne_of_gt (zero_lt_one.trans_le (hN i))) + calc + ‖exponentialSum F T N a b i‖ ≤ + ∑ _k : ZMod (q i), + (C * T i ^ (exponentSumGrowthExponent γ + ε / 2)) / q i := by + rw [exponentialSum_apply] + refine hdilate.trans ?_ + apply Finset.sum_le_sum + intro k _ + exact div_le_div_of_nonneg_right (hphaseBound k) (Nat.cast_nonneg _) + _ = C * T i ^ (exponentSumGrowthExponent γ + ε / 2) := by + rw [Finset.sum_const, show Finset.univ.card = q i from ZMod.card (q i), + nsmul_eq_mul] + field_simp [show (q i : ℝ) ≠ 0 by exact_mod_cast hqi.ne'] + _ ≤ C * ‖T i ^ (exponentSumGrowthExponent γ + ε)‖ := by + rw [Real.norm_eq_abs, + abs_of_nonneg (Real.rpow_nonneg (zero_le_one.trans (hT i)) _)] + exact mul_le_mul_of_nonneg_left + (Real.rpow_le_rpow_of_exponent_le (hT i) (by linarith)) + (zero_le_one.trans hC) + +/-- Increasing the scale by `γ - α` costs at most that amount in the growth exponent. -/ +theorem exponentSumGrowthExponent_le_add_sub + {α γ : ℝ≥0} (hαγ : α ≤ γ) : + exponentSumGrowthExponent γ ≤ + exponentSumGrowthExponent α + (γ : ℝ) - (α : ℝ) := by + by_cases heq : α = γ + · subst γ; simp + by_cases hαzero : α = 0 + · subst α + simpa using (exponentSumGrowthExponent_le_iff.mpr (isExponentSumBound_self γ)) + have hαpos : 0 < (α : ℝ) := by positivity + have hgap : 0 < (γ : ℝ) - (α : ℝ) := by + have hlt : (α : ℝ) < (γ : ℝ) := by + exact_mod_cast lt_of_le_of_ne hαγ heq + linarith + rw [exponentSumGrowthExponent_le_iff] + intro N T F a b hN hT hTunbounded hNT hF hab + apply (isPowerBounded_iff_forall_pos _ T _ hT hTunbounded).mpr + intro ε hε + obtain ⟨hphase, σ, hσ, herror⟩ := hF + obtain ⟨δ, hδ, P, hP, C, hC, hfixed⟩ := + (exponentSumGrowthExponent_le_iff_nonAsymptotic.mp + (le_rfl : exponentSumGrowthExponent α ≤ exponentSumGrowthExponent α)) + (ε / 4) (by linarith) σ hσ + let η : ℝ := min (δ / 4) (min (ε / 8) ((α : ℝ) / 4)) + have hη : 0 < η := by dsimp [η]; positivity + have hηδ : η < δ := lt_of_le_of_lt (min_le_left _ _) (by linarith) + have hηε : η ≤ ε / 8 := + (min_le_right (δ / 4) _).trans (min_le_left _ _) + have hηα : η < (α : ℝ) := by + have hηquarter : η ≤ (α : ℝ) / 4 := + (min_le_right (δ / 4) (min (ε / 8) ((α : ℝ) / 4))).trans + (min_le_right (ε / 8) ((α : ℝ) / 4)) + linarith + let κ : ℝ := (γ : ℝ) - (α : ℝ) + η + have hκ : 0 < κ := by dsimp [κ]; linarith + let q : VariableObject ℕ := floorRpow T κ + let Q : VariableObject ℝ := fun i ↦ (q i : ℝ) + have hTtop : Tendsto T atTop atTop := + (VariableObject.isUnbounded_iff_tendsto_atTop + (fun i ↦ zero_le_one.trans (hT i))).mp hTunbounded + have hQasym : IsPowerAsymptotic Q T κ := + isPowerAsymptotic_floorRpow hκ hT hTunbounded + have hQdivNasym : IsPowerAsymptotic (Q / N) T (η - (α : ℝ)) := by + have := hQasym.div hNT hT + convert this using 1 + dsimp [κ] + ring + have hQdivNzero : Tendsto (Q / N) atTop (𝓝 0) := by + apply hQdivNasym.tendsto_zero_of_neg + · linarith + · exact hT + · exact hTunbounded + have hqNevent : ∀ᶠ i in atTop, (q i : ℝ) ≤ N i := by + have := (Metric.tendsto_nhds.1 hQdivNzero) 1 zero_lt_one + filter_upwards [this] with i hi + rw [dist_zero_right, Real.norm_eq_abs] at hi + change |(q i : ℝ) / N i| < 1 at hi + rw [ + abs_of_nonneg (div_nonneg (Nat.cast_nonneg _) (zero_le_one.trans (hN i)))] at hi + have hNpos : 0 < N i := zero_lt_one.trans_le (hN i) + exact (div_le_one hNpos).mp hi.le + classical + let A : ℕ → ℕ → ℕ := fun i r ↦ (a i - r) ⌈/⌉ q i + let B : ℕ → ℕ → ℕ := fun i r ↦ + min ((b i - r) / q i) ⌊2 * residueScale (N i) (q i) r⌋₊ + have hmax (i : ℕ) : ∃ r ∈ Finset.range (q i), ∀ s ∈ Finset.range (q i), + ‖exponentialSumAt (residuePhase (F i) (N i) s) (T i) + (residueScale (N i) (q i) s) (A i s) (B i s)‖ ≤ + ‖exponentialSumAt (residuePhase (F i) (N i) r) (T i) + (residueScale (N i) (q i) r) (A i r) (B i r)‖ := + Finset.exists_max_image (Finset.range (q i)) + (fun r ↦ ‖exponentialSumAt (residuePhase (F i) (N i) r) (T i) + (residueScale (N i) (q i) r) (A i r) (B i r)‖) + ⟨0, Finset.mem_range.mpr (floorRpow_pos T κ i)⟩ + let r : VariableObject ℕ := fun i ↦ + if (q i : ℝ) ≤ N i then (hmax i).choose else 0 + have hrq (i : ℕ) : r i < q i := by + dsimp [r] + split_ifs + · exact Finset.mem_range.mp (hmax i).choose_spec.1 + · exact floorRpow_pos T κ i + have hrN (i : ℕ) : (r i : ℝ) < N i := by + dsimp [r] + split_ifs with hi + · exact lt_of_lt_of_le (by exact_mod_cast Finset.mem_range.mp (hmax i).choose_spec.1) hi + · simpa only [Nat.cast_zero] using zero_lt_one.trans_le (hN i) + let d : VariableObject ℝ := fun i ↦ (r i : ℝ) / N i + let c : VariableObject ℝ := fun i ↦ 1 - d i + have hdBound : ∀ i, 0 ≤ d i ∧ d i ≤ Q i / N i := by + intro i + constructor + · dsimp [d] + exact div_nonneg (Nat.cast_nonneg _) (zero_le_one.trans (hN i)) + · dsimp [d, Q] + exact div_le_div_of_nonneg_right (by exact_mod_cast (hrq i).le) + (zero_le_one.trans (hN i)) + have hdZero : Tendsto d atTop (𝓝 0) := + squeeze_zero' (Filter.Eventually.of_forall fun i ↦ (hdBound i).1) + (Filter.Eventually.of_forall fun i ↦ (hdBound i).2) hQdivNzero + have hcOne : Tendsto c atTop (𝓝 1) := by + simpa [c] using tendsto_const_nhds.sub hdZero + let M : VariableObject ℝ := fun i ↦ residueScale (N i) (q i) (r i) + have hNasymDiv : IsPowerAsymptotic (N / Q) T ((γ : ℝ) - κ) := hNT.div hQasym hT + have hcasym : IsPowerAsymptotic c T 0 := + isPowerAsymptotic_zero_of_tendsto_one hcOne hT hTunbounded + have hMformula : M = (N / Q) * c := by + funext i + dsimp [M, residueScale, Q, c, d] + field_simp [show (q i : ℝ) ≠ 0 by exact_mod_cast (floorRpow_pos T κ i).ne', + show N i ≠ 0 by exact (ne_of_gt (zero_lt_one.trans_le (hN i)))] + have hMasym0 : IsPowerAsymptotic M T (((γ : ℝ) - κ) + 0) := by + rw [hMformula] + exact hNasymDiv.mul hcasym hT + have hMasym : IsPowerAsymptotic M T ((α : ℝ) - η) := by + convert hMasym0 using 1 + dsimp [κ] + ring + let G : VariableFunction (VariableObject.fixed ℝ) ℝ := fun i ↦ residuePhase (F i) (N i) (r i) + have hmap (i : ℕ) : Set.MapsTo (fun u ↦ c i * u + d i) phaseInterval phaseInterval := by + intro u hu + have hdI : d i ∈ Set.Ico (0 : ℝ) 1 := by + exact ⟨(hdBound i).1, + (div_lt_one (zero_lt_one.trans_le (hN i))).mpr (hrN i)⟩ + rcases hu with ⟨hu1, hu2⟩ + dsimp [c, phaseInterval] at * + constructor <;> nlinarith [hdI.1, hdI.2] + have hGdata : IsModelPhaseFunctionWith G σ := by + have hdata := + (IsModelPhaseFunctionWith.mk hphase herror).comp_affine_tendsto_id hcOne hdZero hmap + change IsModelPhaseFunctionWith + (fun i u ↦ F i ((1 - (r i : ℝ) / N i) * u + (r i : ℝ) / N i)) σ + simpa only [c, d] using hdata + have hGapprox : ∀ᶠ i in atTop, IsApproximateModelPhaseFunction (G i) σ P δ := + hGdata.eventually_isApproximate P hδ + have hMbetween := hMasym.eventually_between + (Filter.Eventually.of_forall hT) (sub_pos.mpr hηδ) + have hMtop : Tendsto M atTop atTop := by + have hpowtop : Tendsto (fun i ↦ T i ^ (((α : ℝ) - η) / 2)) atTop atTop := + (tendsto_rpow_atTop (by linarith)).comp hTtop + apply tendsto_atTop_mono' atTop _ hpowtop + have hb := hMasym.eventually_between (Filter.Eventually.of_forall hT) + (show 0 < ((α : ℝ) - η) / 2 by linarith) + filter_upwards [hb] with i hi + have hexp : ((α : ℝ) - η) / 2 = + (α : ℝ) - η - ((α : ℝ) - η) / 2 := by ring + rw [hexp] + exact hi.1 + have hMone : ∀ᶠ i in atTop, 1 ≤ M i := hMtop.eventually (eventually_ge_atTop 1) + have hthreshold : ∀ᶠ i in atTop, C ≤ T i := hTtop.eventually (eventually_ge_atTop C) + have hqUpper : ∀ᶠ i in atTop, (q i : ℝ) ≤ T i ^ κ := by + have hpowlarge : ∀ᶠ i in atTop, 1 ≤ T i ^ κ := + ((tendsto_rpow_atTop hκ).comp hTtop).eventually (eventually_ge_atTop 1) + filter_upwards [hpowlarge] with i hi + dsimp [q, floorRpow] + rw [max_eq_right ((Nat.one_le_floor_iff _).mpr hi)] + exact Nat.floor_le (Real.rpow_nonneg (zero_le_one.trans (hT i)) _) + refine Asymptotics.IsBigO.of_bound (2 * C) ?_ + filter_upwards [hqNevent, hGapprox, hMbetween, hMone, hthreshold, hqUpper] + with i hiqN hiG hiM hiMone hiC hiqUpper + have hqi := floorRpow_pos T κ i + have hMbounds : T i ^ ((α : ℝ) - δ) ≤ M i ∧ M i ≤ T i ^ ((α : ℝ) + δ) := by + constructor + · have hexp : (α : ℝ) - δ = (α : ℝ) - η - (δ - η) := by ring + rw [hexp] + exact hiM.1 + · exact hiM.2.trans (Real.rpow_le_rpow_of_exponent_le (hT i) (by linarith)) + have hA : M i ≤ (A i (r i) : ℝ) := by + dsimp [M, residueScale, A] + have hceil : a i - r i ≤ q i * ((a i - r i) ⌈/⌉ q i) := + le_smul_ceilDiv hqi + have hra : r i ≤ a i := by + exact_mod_cast (hrN i).le.trans (hab i).1 + have hceilR : ((a i - r i : ℕ) : ℝ) ≤ + (q i : ℝ) * (((a i - r i) ⌈/⌉ q i : ℕ) : ℝ) := by + exact_mod_cast hceil + rw [Nat.cast_sub hra] at hceilR + rw [div_le_iff₀ (show (0 : ℝ) < q i by exact_mod_cast hqi)] + nlinarith [(hab i).1] + have hB : (B i (r i) : ℝ) ≤ 2 * M i := by + dsimp [B, M] + calc + ((min ((b i - r i) / q i) + ⌊2 * residueScale (N i) (q i) (r i)⌋₊ : ℕ) : ℝ) ≤ + (⌊2 * residueScale (N i) (q i) (r i)⌋₊ : ℕ) := by + exact_mod_cast min_le_right ((b i - r i) / q i) + ⌊2 * residueScale (N i) (q i) (r i)⌋₊ + _ ≤ 2 * residueScale (N i) (q i) (r i) := + Nat.floor_le (by linarith [hiMone]) + have hselected := hfixed (T i) (M i) (G i) (A i (r i)) (B i (r i)) + ⟨hiC, hMbounds.1, hMbounds.2, hiG, hA, hB⟩ + have hres := norm_exponentialSumAt_le_sum_residues (F i) (T i) (N i) + (a i) (b i) (q i) hqi hiqN + (ne_of_gt (zero_lt_one.trans_le (hN i))) (hab i).1 (hab i).2 + have hmaxEvent : ∀ s ∈ Finset.range (q i), + ‖exponentialSumAt (residuePhase (F i) (N i) s) (T i) + (residueScale (N i) (q i) s) (A i s) (B i s)‖ ≤ + ‖exponentialSumAt (G i) (T i) (M i) (A i (r i)) (B i (r i))‖ := by + intro s hs + have hri : r i = (hmax i).choose := by simp [r, hiqN] + change ‖exponentialSumAt (residuePhase (F i) (N i) s) (T i) + (residueScale (N i) (q i) s) (A i s) (B i s)‖ ≤ + ‖exponentialSumAt (residuePhase (F i) (N i) (r i)) (T i) + (residueScale (N i) (q i) (r i)) (A i (r i)) (B i (r i))‖ + rw [hri] + exact (hmax i).choose_spec.2 s hs + have hsum : ‖exponentialSum F T N a b i‖ ≤ + (q i : ℝ) * + (‖exponentialSumAt (G i) (T i) (M i) (A i (r i)) (B i (r i))‖ + 1) := by + rw [exponentialSum_apply] + refine hres.trans ?_ + calc + _ ≤ ∑ _s ∈ Finset.range (q i), + (‖exponentialSumAt (G i) (T i) (M i) (A i (r i)) (B i (r i))‖ + 1) := by + gcongr with s hs + simpa only [A, B] using hmaxEvent s hs + _ = _ := by simp [mul_add, mul_comm] + have hβnonneg : 0 ≤ exponentSumGrowthExponent α := + (isExponentSumBound_exponentSumGrowthExponent α).nonneg + calc + ‖exponentialSum F T N a b i‖ ≤ + (q i : ℝ) * (C * T i ^ (exponentSumGrowthExponent α + ε / 4) + 1) := by + exact hsum.trans (mul_le_mul_of_nonneg_left + (add_le_add hselected le_rfl) (Nat.cast_nonneg _)) + _ ≤ 2 * C * T i ^ + (exponentSumGrowthExponent α + (γ : ℝ) - (α : ℝ) + ε) := by + have hone : 1 ≤ C * T i ^ (exponentSumGrowthExponent α + ε / 4) := by + calc + 1 ≤ C := hC + _ = C * 1 := by ring + _ ≤ _ := by gcongr; exact Real.one_le_rpow (hT i) (by linarith) + calc + _ ≤ (q i : ℝ) * (2 * (C * T i ^ (exponentSumGrowthExponent α + ε / 4))) := by + gcongr; linarith + _ ≤ T i ^ κ * (2 * (C * T i ^ (exponentSumGrowthExponent α + ε / 4))) := by + gcongr + _ = 2 * C * + (T i ^ κ * T i ^ (exponentSumGrowthExponent α + ε / 4)) := by ring + _ = 2 * C * T i ^ (κ + exponentSumGrowthExponent α + ε / 4) := by + congr 1 + rw [← Real.rpow_add (zero_lt_one.trans_le (hT i))] + congr 1 + ring + _ ≤ _ := by + have hp : T i ^ (κ + exponentSumGrowthExponent α + ε / 4) ≤ + T i ^ (exponentSumGrowthExponent α + (γ : ℝ) - (α : ℝ) + ε) := by + apply Real.rpow_le_rpow_of_exponent_le (hT i) + dsimp [κ] + linarith + exact mul_le_mul_of_nonneg_left hp + (mul_nonneg (by norm_num) (zero_le_one.trans hC)) + _ = 2 * C * ‖T i ^ + (exponentSumGrowthExponent α + (γ : ℝ) - (α : ℝ) + ε)‖ := by + rw [Real.norm_eq_abs, + abs_of_nonneg (Real.rpow_nonneg (zero_le_one.trans (hT i)) _)] + +/-- The growth exponent is `1`-Lipschitz on the subcritical interval. -/ +theorem lipschitzOnWith_exponentSumGrowthExponent : + LipschitzOnWith 1 exponentSumGrowthExponent (Set.Icc 0 1) := by + rw [lipschitzOnWith_iff_dist_le_mul] + intro α hα γ hγ + simp only [NNReal.coe_one, one_mul, Real.dist_eq] + wlog hαγ : α ≤ γ generalizing α γ + · rw [abs_sub_comm, dist_comm] + exact this γ hγ α hα (le_of_not_ge hαγ) + have hmono := exponentSumGrowthExponent_monoOn_Icc hα hγ hαγ + have hslope := exponentSumGrowthExponent_le_add_sub hαγ + rw [abs_of_nonpos (sub_nonpos.mpr hmono), NNReal.dist_eq, + abs_of_nonpos (sub_nonpos.mpr (by exact_mod_cast hαγ))] + linarith + +/-- The exponential-sum growth exponent is continuous on the subcritical interval. -/ +theorem continuousOn_exponentSumGrowthExponent : + ContinuousOn exponentSumGrowthExponent (Set.Icc 0 1) := + lipschitzOnWith_exponentSumGrowthExponent.continuousOn + +/-- The exponential-sum growth exponent is upper semicontinuous. -/ +theorem upperSemicontinuous_exponentSumGrowthExponent : + UpperSemicontinuous exponentSumGrowthExponent := by + rw [upperSemicontinuous_iff] + intro α y hy + by_cases hαlt : α < 1 + · have hIcc : Set.Icc (0 : ℝ≥0) 1 ∈ nhds α := + Filter.mem_of_superset (Iio_mem_nhds hαlt) fun γ hγ ↦ ⟨zero_le, hγ.le⟩ + exact ((continuousOn_exponentSumGrowthExponent α ⟨zero_le, hαlt.le⟩).continuousAt + hIcc).upperSemicontinuousAt y hy + · have hαone : 1 ≤ α := le_of_not_gt hαlt + by_cases hαeq : α = 1 + · subst α + have hβnonneg := exponentSumGrowthExponent_nonneg 1 + let ρ : ℝ := min (y / 2) 1 + have hypos : 0 < y := lt_of_le_of_lt hβnonneg hy + have hρ : 0 < ρ := by dsimp [ρ]; positivity + rw [Metric.eventually_nhds_iff] + refine ⟨ρ, hρ, ?_⟩ + intro γ hdist + by_cases hγone : γ ≤ 1 + · exact lt_of_le_of_lt + (exponentSumGrowthExponent_monoOn_Icc + ⟨zero_le, hγone⟩ ⟨zero_le, le_rfl⟩ hγone) hy + · have hγgt : 1 < γ := lt_of_not_ge hγone + rw [exponentSumGrowthExponent_eq_sub_one hγgt] + have hdist' : |(γ : ℝ) - 1| < ρ := by + simpa [NNReal.dist_eq, abs_sub_comm] using hdist + have hρy := min_le_left (y / 2) (1 : ℝ) + have hdiffUpper := (abs_lt.mp hdist').2 + linarith + · have hαgt : 1 < α := lt_of_le_of_ne hαone (Ne.symm hαeq) + have heq : exponentSumGrowthExponent =ᶠ[nhds α] + fun γ : ℝ≥0 ↦ (γ : ℝ) - 1 := by + filter_upwards [Ioi_mem_nhds hαgt] with γ hγ + exact exponentSumGrowthExponent_eq_sub_one hγ + have hcont : ContinuousAt exponentSumGrowthExponent α := + (by fun_prop : ContinuousAt (fun γ : ℝ≥0 ↦ (γ : ℝ) - 1) α).congr_of_eventuallyEq + heq + exact hcont.upperSemicontinuousAt y hy + +end Expdb diff --git a/Expdb/Fourier/Bump.lean b/Expdb/Fourier/Bump.lean new file mode 100644 index 0000000..11c5e5e --- /dev/null +++ b/Expdb/Fourier/Bump.lean @@ -0,0 +1,328 @@ +module + +public import Expdb.Basic.Definitions + +public import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct +public import Mathlib.Analysis.Distribution.SchwartzSpace.Fourier + +/-! +# A normalized smooth bump and its Fourier transform + +This module collects the concrete bump function used in the proof of the `L²` integral +estimate of the blueprint's Basic Fourier estimates chapter (`l2-chapter`), together with its +Fourier transform and the orthonormal family formed by its translates. + +The bump `bump` is a fixed smooth, nonnegative, compactly supported function with +`‖bump‖_{L²} = 1` and support in `[-1/4, 1/4]`. Its translates by `1`-separated shifts are +therefore orthonormal, which is what the `L²` estimate uses. + +These declarations are auxiliary to `Expdb.Fourier.L2Integral` and are collected in the +namespace `Expdb.L2Bump`. +-/ + +@[expose] public section + +open MeasureTheory Real Complex Filter Topology BigOperators +open scoped FourierTransform SchwartzMap ContDiff + +noncomputable section + +namespace Expdb.L2Bump + +/-! ## A normalized smooth bump -/ + +def rawBump : ContDiffBump (0 : ℝ) := + ⟨1 / 8, 1 / 4, by norm_num, by norm_num⟩ + +def rawL2 : ℝ := ∫ x : ℝ, (rawBump x) ^ 2 + +private lemma rawL2_pos : 0 < rawL2 := by + have hraw : Continuous (rawBump : ℝ → ℝ) := + (rawBump.contDiff (n := ⊤)).continuous + have hsq : Continuous (fun x : ℝ => (rawBump x) ^ 2) := by + convert (continuous_pow 2).comp hraw using 1 + ext x + rfl + apply integral_pos_of_integrable_nonneg_nonzero (x := 0) + · exact hsq + · apply hsq.integrable_of_hasCompactSupport + apply HasCompactSupport.of_support_subset_isCompact rawBump.hasCompactSupport.isCompact + intro x hx + apply subset_tsupport rawBump + simp only [Function.mem_support] at hx ⊢ + intro hzero + apply hx + simp [hzero] + · intro x + positivity + · have hzero : (rawBump : ℝ → ℝ) 0 = 1 := by + apply rawBump.one_of_mem_closedBall + simp [rawBump, Metric.mem_closedBall] + simp [hzero] + +def bump (x : ℝ) : ℝ := rawBump x / Real.sqrt rawL2 + +lemma bump_smooth : ContDiff ℝ ∞ bump := by + change ContDiff ℝ ∞ (fun x => rawBump x / Real.sqrt rawL2) + exact (rawBump.contDiff (n := ⊤)).div_const (Real.sqrt rawL2) + +lemma bump_hasCompactSupport : HasCompactSupport bump := by + apply HasCompactSupport.of_support_subset_isCompact rawBump.hasCompactSupport.isCompact + intro x hx + apply subset_tsupport rawBump + simp only [Function.mem_support] at hx ⊢ + intro hzero + apply hx + simp [bump, hzero] + +lemma bump_supp (x : ℝ) (hx : bump x ≠ 0) : |x| ≤ 1 / 4 := by + have hraw : (rawBump : ℝ → ℝ) x ≠ 0 := by + intro hzero + apply hx + simp [bump, hzero] + have hmem : x ∈ Metric.ball (0 : ℝ) rawBump.rOut := by + rw [← rawBump.support_eq] + exact hraw + have : |x| < 1 / 4 := by + simpa [rawBump, Metric.mem_ball, Real.dist_eq] using hmem + exact this.le + +lemma bump_nonneg (x : ℝ) : 0 ≤ bump x := + div_nonneg (rawBump.nonneg' x) (Real.sqrt_nonneg rawL2) + +lemma bump_l2norm : ∫ x : ℝ, (bump x) ^ 2 = 1 := by + rw [show (fun x : ℝ => (bump x) ^ 2) = fun x => (rawBump x) ^ 2 / rawL2 by + funext x + simp only [bump, div_pow] + rw [Real.sq_sqrt rawL2_pos.le]] + rw [integral_div] + exact div_self (ne_of_gt rawL2_pos) + +-- bump̂(u) = ∫_ℝ bump(x) e(-xu) dx +def bumpFourier (u : ℝ) : ℂ := + ∫ x : ℝ, (bump x : ℂ) * 𝐞 (-(x * u)) + +-- bump is integrable +lemma bump_integrable : Integrable bump := + bump_smooth.continuous.integrable_of_hasCompactSupport bump_hasCompactSupport + +-- ∫ bump > 0 (from proof: "bump(t) ≥ 0 and ‖bump‖_{L²} = 1 so bump ≢ 0") +private lemma bump_integral_pos : 0 < ∫ x : ℝ, bump x := by + have hne : ∃ x, bump x ≠ 0 := by + by_contra h + push Not at h + have hsquare : ∫ x : ℝ, (bump x) ^ 2 = 0 := by + calc + ∫ x : ℝ, (bump x) ^ 2 + = ∫ x : ℝ, (0 : ℝ) ^ 2 := by + congr 1 + ext x + rw [h x] + _ = 0 := by simp + linarith [bump_l2norm, hsquare] + obtain ⟨x, hx⟩ := hne + exact integral_pos_of_integrable_nonneg_nonzero + bump_smooth.continuous bump_integrable bump_nonneg hx + +/-! ## Plancherel and decay of the bump's Fourier transform -/ + +private lemma bump_complex_hasCompactSupport : HasCompactSupport (fun x : ℝ => (bump x : ℂ)) := + HasCompactSupport.of_support_subset_isCompact + (isCompact_Icc (a := -1 / 4) (b := 1 / 4)) (by + intro x hx + simp only [Function.mem_support] at hx + have h := bump_supp x (by exact_mod_cast hx) + simp only [Set.mem_Icc, abs_le] at h ⊢ + simpa only [neg_div] using h) + +private lemma bump_complex_smooth : ContDiff ℝ ∞ (fun x : ℝ => (bump x : ℂ)) := by + change ContDiff ℝ ∞ (Complex.ofRealCLM ∘ bump) + exact (Complex.ofRealCLM.contDiff (n := ∞)).comp bump_smooth + +private def bumpSchwartz : 𝓢(ℝ, ℂ) := + bump_complex_hasCompactSupport.toSchwartzMap bump_complex_smooth + +private lemma bumpFourier_eq_fourier : bumpFourier = 𝓕 (bumpSchwartz : ℝ → ℂ) := by + funext u + rw [Real.fourier_real_eq] + simp only [bumpFourier, Real.fourierChar_apply, mul_neg, Complex.ofReal_neg, + Complex.ofReal_mul, Complex.ofReal_ofNat, neg_mul, bumpSchwartz, + HasCompactSupport.toSchwartzMap_toFun, Circle.smul_def, smul_eq_mul] + apply integral_congr_ae + filter_upwards with x + ring + +lemma bumpFourier_continuous : Continuous bumpFourier := by + rw [bumpFourier_eq_fourier] + exact (𝓕 bumpSchwartz).continuous + +lemma bumpFourier_l2 : ∫ u : ℝ, ‖bumpFourier u‖ ^ 2 = 1 := by + simp_rw [bumpFourier_eq_fourier] + rw [← SchwartzMap.fourier_coe, SchwartzMap.integral_norm_sq_fourier] + simpa [bumpSchwartz, Real.norm_eq_abs, abs_of_nonneg (bump_nonneg _)] using bump_l2norm + +lemma bumpFourier_sq_integrable : + Integrable (fun u : ℝ => ‖bumpFourier u‖ ^ 2) := by + by_contra h + have hzero := bumpFourier_l2 + rw [integral_undef h] at hzero + norm_num at hzero + +lemma bumpFourier_decay (K : ℕ) : + ∃ C : ℝ, 0 < C ∧ ∀ u : ℝ, ‖bumpFourier u‖ ≤ C * (1 + |u|) ^ (-(K : ℝ)) := by + let g : 𝓢(ℝ, ℂ) := 𝓕 bumpSchwartz + have hfourier : ∀ u : ℝ, bumpFourier u = g u := by + intro u + exact congr_fun bumpFourier_eq_fourier u + let c : ℝ := 2 ^ K * (Finset.Iic (K, 0)).sup + (fun m => SchwartzMap.seminorm ℝ m.1 m.2) g + refine ⟨|c| + 1, by positivity, ?_⟩ + intro u + have hweight : (1 + |u|) ^ K * ‖bumpFourier u‖ ≤ c := by + have hw := SchwartzMap.one_add_le_sup_seminorm_apply + (𝕜 := ℝ) (m := (K, 0)) (k := K) (n := 0) le_rfl le_rfl g u + rw [norm_iteratedFDeriv_zero, ← hfourier u] at hw + simpa [c, Real.norm_eq_abs] using hw + have hbase : 0 < 1 + |u| := by positivity + have hpow : 0 < (1 + |u|) ^ K := by positivity + have hrpow : (1 + |u|) ^ (-(K : ℝ)) = ((1 + |u|) ^ K)⁻¹ := by + rw [← Real.rpow_natCast, Real.rpow_neg hbase.le] + rw [hrpow, ← div_eq_mul_inv] + apply (le_div_iff₀ hpow).2 + calc + ‖bumpFourier u‖ * (1 + |u|) ^ K = + (1 + |u|) ^ K * ‖bumpFourier u‖ := by ring + _ ≤ c := hweight + _ ≤ |c| + 1 := by linarith [le_abs_self c] + +lemma bumpFourier_lower_bound : + ∃ c δ : ℝ, 0 < c ∧ 0 < δ ∧ + ∀ u : ℝ, |u| ≤ δ → c ≤ ‖bumpFourier u‖ ^ 2 := by + have hcts : Continuous bumpFourier := bumpFourier_continuous + have hpsi0_eq : (bumpFourier 0).re = ∫ x : ℝ, bump x := by + simp only [bumpFourier, mul_zero, neg_zero] + have hbumpc : Integrable (fun x : ℝ => (bump x : ℂ)) := bump_integrable.ofReal + simpa using (integral_re hbumpc).symm + have hpsi0 : 0 < (bumpFourier 0).re := by + rw [hpsi0_eq] + exact bump_integral_pos + have hpos : 0 < ‖bumpFourier 0‖ := by + rw [norm_pos_iff] + intro hzero + have : (bumpFourier 0).re = 0 := by rw [hzero]; rfl + linarith + set v₀ := ‖bumpFourier 0‖ + obtain ⟨δ, hδ, hball⟩ := + (Metric.continuousAt_iff.mp hcts.continuousAt) (v₀ / 2) (by linarith) + refine ⟨(v₀ / 2) ^ 2, δ / 2, by positivity, by positivity, ?_⟩ + intro u hu + have hdist : dist (bumpFourier u) (bumpFourier 0) < v₀ / 2 := by + apply hball + rw [Real.dist_eq] + simp only [sub_zero] + exact lt_of_le_of_lt hu (by linarith) + have hbound : v₀ - ‖bumpFourier u‖ < v₀ / 2 := by + calc + v₀ - ‖bumpFourier u‖ = ‖bumpFourier 0‖ - ‖bumpFourier u‖ := rfl + _ ≤ ‖bumpFourier 0 - bumpFourier u‖ := norm_sub_norm_le _ _ + _ = dist (bumpFourier u) (bumpFourier 0) := by + rw [dist_eq_norm_sub, norm_sub_rev] + _ < v₀ / 2 := hdist + have hball' : v₀ / 2 < ‖bumpFourier u‖ := by linarith + nlinarith [norm_nonneg (bumpFourier u)] + +/-! ## Weighted Plancherel identity -/ + +-- Package translates of the concrete bump as Schwartz functions. +def bumpShift (w : ℝ) : 𝓢(ℝ, ℂ) := by + let f : ℝ → ℂ := fun x => (bump (x + w) : ℂ) + have hcomp : HasCompactSupport f := by + apply HasCompactSupport.of_support_subset_isCompact + (isCompact_Icc (a := -w - 1 / 4) (b := -w + 1 / 4)) + intro x hx + change (bump (x + w) : ℂ) ≠ 0 at hx + have hx' : bump (x + w) ≠ 0 := by exact_mod_cast hx + have h := abs_le.mp (bump_supp (x + w) hx') + constructor <;> linarith + have hsmooth : ContDiff ℝ ∞ f := by + change ContDiff ℝ ∞ ((fun x : ℝ => (bump x : ℂ)) ∘ fun x => x + w) + exact + ((Complex.ofRealCLM.contDiff (n := ∞)).comp bump_smooth).comp + (contDiff_id.add contDiff_const) + exact hcomp.toSchwartzMap hsmooth + +lemma bumpShift_apply (w x : ℝ) : bumpShift w x = bump (x + w) := rfl + +lemma fourier_bumpShift (w u : ℝ) : + (𝓕 (bumpShift w : ℝ → ℂ)) u = + 𝐞 (w * u) * bumpFourier u := by + have hcoe : (bumpShift w : ℝ → ℂ) = fun x : ℝ => (bump (x + w) : ℂ) := by + ext x + exact_mod_cast bumpShift_apply w x + rw [hcoe, Real.fourier_real_eq] + have hpsi : bumpFourier u = + ∫ x : ℝ, 𝐞 (-(x * u)) * (bump x : ℂ) := by + simp only [bumpFourier] + apply integral_congr_ae + filter_upwards with x + ring + rw [hpsi] + have ht := congr_fun + (Fourier.fourierIntegral_comp_add_right 𝐞 volume (fun x : ℝ => (bump x : ℂ)) w) u + simpa [Fourier.fourierIntegral_def, Circle.smul_def, Real.fourierChar_apply] using ht + +private lemma bumpShift_inner_eq_zero {v w : ℝ} (hvw : 1 ≤ |v - w|) : + ∫ x : ℝ, inner ℂ (bumpShift v x) (bumpShift w x) = 0 := by + apply integral_eq_zero_of_ae + filter_upwards with x + by_cases hxv : bump (x + v) = 0 + · simp [bumpShift_apply, hxv] + by_cases hxw : bump (x + w) = 0 + · simp [bumpShift_apply, hxw] + exfalso + have hv := bump_supp (x + v) hxv + have hw := bump_supp (x + w) hxw + have hbound : |v - w| ≤ 1 / 2 := by + calc + |v - w| = |(x + v) - (x + w)| := by ring_nf + _ ≤ |x + v| + |x + w| := abs_sub _ _ + _ ≤ 1 / 4 + 1 / 4 := by linarith + _ = 1 / 2 := by norm_num + linarith + +private lemma bumpShift_inner_self (w : ℝ) : + ∫ x : ℝ, inner ℂ (bumpShift w x) (bumpShift w x) = 1 := by + calc + ∫ x : ℝ, inner ℂ (bumpShift w x) (bumpShift w x) = + ∫ x : ℝ, (((bump (x + w)) ^ 2 : ℝ) : ℂ) := by + apply integral_congr_ae + filter_upwards with x + simp [bumpShift_apply, abs_of_nonneg (bump_nonneg _)] + _ = ((∫ x : ℝ, (bump (x + w)) ^ 2 : ℝ) : ℂ) := integral_ofReal + _ = ((∫ x : ℝ, (bump x) ^ 2 : ℝ) : ℂ) := by + rw [integral_add_right_eq_self (fun x : ℝ => (bump x) ^ 2) w] + _ = 1 := by rw [bump_l2norm]; norm_num + +lemma bumpShift_orthonormal {ι : Type*} [Finite ι] + (ξ : ι → ℝ) (N : ℝ) (hN : 0 < N) + (hsep : IsSeparatedFamily (1 / N) ξ) : + Orthonormal ℂ (fun r => (bumpShift (N * ξ r)).toLp 2) := by + classical + letI := Fintype.ofFinite ι + rw [orthonormal_iff_ite] + intro r s + rw [SchwartzMap.inner_toL2_toL2_eq + (bumpShift (N * ξ r)) (bumpShift (N * ξ s)) volume] + by_cases hrs : r = s + · subst s + rw [if_pos rfl, bumpShift_inner_self] + · rw [if_neg hrs] + apply bumpShift_inner_eq_zero + rw [show N * ξ r - N * ξ s = N * (ξ r - ξ s) by ring, abs_mul, abs_of_pos hN] + calc + 1 = N * (1 / N) := by field_simp + _ ≤ N * |ξ r - ξ s| := mul_le_mul_of_nonneg_left (hsep hrs) hN.le + +end Expdb.L2Bump + +end diff --git a/Expdb/Fourier/L2Integral.lean b/Expdb/Fourier/L2Integral.lean index 6ec4bbf..157a3a3 100644 --- a/Expdb/Fourier/L2Integral.lean +++ b/Expdb/Fourier/L2Integral.lean @@ -1,11 +1,10 @@ module public import Expdb.Basic.Definitions +public import Expdb.Fourier.Bump public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic import Mathlib.Algebra.Order.Interval.Set.Group -import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct -import Mathlib.Analysis.Distribution.SchwartzSpace.Fourier import Mathlib.Analysis.PSeries import Mathlib.MeasureTheory.Integral.IntervalAverage @@ -27,104 +26,12 @@ noncomputable section namespace Expdb -/-! ### A normalized smooth bump -/ - -private def rawBump : ContDiffBump (0 : ℝ) := - ⟨1 / 8, 1 / 4, by norm_num, by norm_num⟩ - -private def rawL2 : ℝ := ∫ x : ℝ, (rawBump x) ^ 2 - -private lemma rawL2_pos : 0 < rawL2 := by - have hraw : Continuous (rawBump : ℝ → ℝ) := - (rawBump.contDiff (n := ⊤)).continuous - have hsq : Continuous (fun x : ℝ => (rawBump x) ^ 2) := by - convert (continuous_pow 2).comp hraw using 1 - ext x - rfl - apply integral_pos_of_integrable_nonneg_nonzero (x := 0) - · exact hsq - · apply hsq.integrable_of_hasCompactSupport - apply HasCompactSupport.of_support_subset_isCompact rawBump.hasCompactSupport.isCompact - intro x hx - apply subset_tsupport rawBump - simp only [Function.mem_support] at hx ⊢ - intro hzero - apply hx - simp [hzero] - · intro x - positivity - · have hzero : (rawBump : ℝ → ℝ) 0 = 1 := by - apply rawBump.one_of_mem_closedBall - simp [rawBump, Metric.mem_closedBall] - simp [hzero] - -private def bump (x : ℝ) : ℝ := rawBump x / Real.sqrt rawL2 - -private lemma bump_smooth : ContDiff ℝ ∞ bump := by - change ContDiff ℝ ∞ (fun x => rawBump x / Real.sqrt rawL2) - exact (rawBump.contDiff (n := ⊤)).div_const (Real.sqrt rawL2) - -private lemma bump_hasCompactSupport : HasCompactSupport bump := by - apply HasCompactSupport.of_support_subset_isCompact rawBump.hasCompactSupport.isCompact - intro x hx - apply subset_tsupport rawBump - simp only [Function.mem_support] at hx ⊢ - intro hzero - apply hx - simp [bump, hzero] - -private lemma bump_supp (x : ℝ) (hx : bump x ≠ 0) : |x| ≤ 1 / 4 := by - have hraw : (rawBump : ℝ → ℝ) x ≠ 0 := by - intro hzero - apply hx - simp [bump, hzero] - have hmem : x ∈ Metric.ball (0 : ℝ) rawBump.rOut := by - rw [← rawBump.support_eq] - exact hraw - have : |x| < 1 / 4 := by - simpa [rawBump, Metric.mem_ball, Real.dist_eq] using hmem - exact this.le - -private lemma bump_nonneg (x : ℝ) : 0 ≤ bump x := - div_nonneg (rawBump.nonneg' x) (Real.sqrt_nonneg rawL2) - -private lemma bump_l2norm : ∫ x : ℝ, (bump x) ^ 2 = 1 := by - rw [show (fun x : ℝ => (bump x) ^ 2) = fun x => (rawBump x) ^ 2 / rawL2 by - funext x - simp only [bump, div_pow] - rw [Real.sq_sqrt rawL2_pos.le]] - rw [integral_div] - exact div_self (ne_of_gt rawL2_pos) - --- bump̂(u) = ∫_ℝ bump(x) e(-xu) dx -private def bumpFourier (u : ℝ) : ℂ := - ∫ x : ℝ, (bump x : ℂ) * 𝐞 (-(x * u)) - --- bump is integrable -private lemma bump_integrable : Integrable bump := - bump_smooth.continuous.integrable_of_hasCompactSupport bump_hasCompactSupport - --- ∫ bump > 0 (from proof: "bump(t) ≥ 0 and ‖bump‖_{L²} = 1 so bump ≢ 0") -private lemma bump_integral_pos : 0 < ∫ x : ℝ, bump x := by - have hne : ∃ x, bump x ≠ 0 := by - by_contra h - push Not at h - have hsquare : ∫ x : ℝ, (bump x) ^ 2 = 0 := by - calc - ∫ x : ℝ, (bump x) ^ 2 - = ∫ x : ℝ, (0 : ℝ) ^ 2 := by - congr 1 - ext x - rw [h x] - _ = 0 := by simp - linarith [bump_l2norm, hsquare] - obtain ⟨x, hx⟩ := hne - exact integral_pos_of_integrable_nonneg_nonzero - bump_smooth.continuous bump_integrable bump_nonneg hx +open L2Bump /-! ### The exponential sum -/ -private def expSum {ι : Type*} [Fintype ι] (a : ι → ℂ) (ξ : ι → ℝ) (t : ℝ) : ℂ := +/-- The exponential sum with coefficients `a` and frequencies `ξ`, evaluated at `t`. -/ +def expSum {ι : Type*} [Fintype ι] (a : ι → ℂ) (ξ : ι → ℝ) (t : ℝ) : ℂ := ∑ r, a r * 𝐞 (ξ r * t) private def expSumSq {ι : Type*} [Fintype ι] (a : ι → ℂ) (ξ : ι → ℝ) (t : ℝ) : ℝ := @@ -145,209 +52,19 @@ private lemma coeff_eq_zero_of_sum_norm_sq_eq_zero (fun i (_ : i ∈ Finset.univ) ↦ sq_nonneg ‖a i‖)).1 h) r (Finset.mem_univ r) nlinarith [norm_nonneg (a r)] +/-- An exponential sum is continuous in its evaluation point. -/ +@[fun_prop] +lemma expSum_continuous {ι : Type*} [Fintype ι] (a : ι → ℂ) (ξ : ι → ℝ) : + Continuous (expSum a ξ) := by + unfold expSum + fun_prop + private lemma expSumSq_continuous {ι : Type*} [Fintype ι] (a : ι → ℂ) (ξ : ι → ℝ) : Continuous (expSumSq a ξ) := by - unfold expSumSq expSum + unfold expSumSq fun_prop -/-! ### Plancherel and decay of the bump's Fourier transform -/ - -private lemma bump_complex_hasCompactSupport : HasCompactSupport (fun x : ℝ => (bump x : ℂ)) := - HasCompactSupport.of_support_subset_isCompact - (isCompact_Icc (a := -1 / 4) (b := 1 / 4)) (by - intro x hx - simp only [Function.mem_support] at hx - have h := bump_supp x (by exact_mod_cast hx) - simp only [Set.mem_Icc, abs_le] at h ⊢ - simpa only [neg_div] using h) - -private lemma bump_complex_smooth : ContDiff ℝ ∞ (fun x : ℝ => (bump x : ℂ)) := by - change ContDiff ℝ ∞ (Complex.ofRealCLM ∘ bump) - exact (Complex.ofRealCLM.contDiff (n := ∞)).comp bump_smooth - -private def bumpSchwartz : 𝓢(ℝ, ℂ) := - bump_complex_hasCompactSupport.toSchwartzMap bump_complex_smooth - -private lemma bumpFourier_eq_fourier : bumpFourier = 𝓕 (bumpSchwartz : ℝ → ℂ) := by - funext u - rw [Real.fourier_real_eq] - simp only [bumpFourier, Real.fourierChar_apply, mul_neg, Complex.ofReal_neg, - Complex.ofReal_mul, Complex.ofReal_ofNat, neg_mul, bumpSchwartz, - HasCompactSupport.toSchwartzMap_toFun, Circle.smul_def, smul_eq_mul] - apply integral_congr_ae - filter_upwards with x - ring - -private lemma bumpFourier_continuous : Continuous bumpFourier := by - rw [bumpFourier_eq_fourier] - exact (𝓕 bumpSchwartz).continuous - -private lemma bumpFourier_l2 : ∫ u : ℝ, ‖bumpFourier u‖ ^ 2 = 1 := by - simp_rw [bumpFourier_eq_fourier] - rw [← SchwartzMap.fourier_coe, SchwartzMap.integral_norm_sq_fourier] - simpa [bumpSchwartz, Real.norm_eq_abs, abs_of_nonneg (bump_nonneg _)] using bump_l2norm - -private lemma bumpFourier_sq_integrable : - Integrable (fun u : ℝ => ‖bumpFourier u‖ ^ 2) := by - by_contra h - have hzero := bumpFourier_l2 - rw [integral_undef h] at hzero - norm_num at hzero - -private lemma bumpFourier_decay (K : ℕ) : - ∃ C : ℝ, 0 < C ∧ ∀ u : ℝ, ‖bumpFourier u‖ ≤ C * (1 + |u|) ^ (-(K : ℝ)) := by - let g : 𝓢(ℝ, ℂ) := 𝓕 bumpSchwartz - have hfourier : ∀ u : ℝ, bumpFourier u = g u := by - intro u - exact congr_fun bumpFourier_eq_fourier u - let c : ℝ := 2 ^ K * (Finset.Iic (K, 0)).sup - (fun m => SchwartzMap.seminorm ℝ m.1 m.2) g - refine ⟨|c| + 1, by positivity, ?_⟩ - intro u - have hweight : (1 + |u|) ^ K * ‖bumpFourier u‖ ≤ c := by - have hw := SchwartzMap.one_add_le_sup_seminorm_apply - (𝕜 := ℝ) (m := (K, 0)) (k := K) (n := 0) le_rfl le_rfl g u - rw [norm_iteratedFDeriv_zero, ← hfourier u] at hw - simpa [c, Real.norm_eq_abs] using hw - have hbase : 0 < 1 + |u| := by positivity - have hpow : 0 < (1 + |u|) ^ K := by positivity - have hrpow : (1 + |u|) ^ (-(K : ℝ)) = ((1 + |u|) ^ K)⁻¹ := by - rw [← Real.rpow_natCast, Real.rpow_neg hbase.le] - rw [hrpow, ← div_eq_mul_inv] - apply (le_div_iff₀ hpow).2 - calc - ‖bumpFourier u‖ * (1 + |u|) ^ K = - (1 + |u|) ^ K * ‖bumpFourier u‖ := by ring - _ ≤ c := hweight - _ ≤ |c| + 1 := by linarith [le_abs_self c] - -private lemma bumpFourier_lower_bound : - ∃ c δ : ℝ, 0 < c ∧ 0 < δ ∧ - ∀ u : ℝ, |u| ≤ δ → c ≤ ‖bumpFourier u‖ ^ 2 := by - have hcts : Continuous bumpFourier := bumpFourier_continuous - have hpsi0_eq : (bumpFourier 0).re = ∫ x : ℝ, bump x := by - simp only [bumpFourier, mul_zero, neg_zero] - have hbumpc : Integrable (fun x : ℝ => (bump x : ℂ)) := bump_integrable.ofReal - simpa using (integral_re hbumpc).symm - have hpsi0 : 0 < (bumpFourier 0).re := by - rw [hpsi0_eq] - exact bump_integral_pos - have hpos : 0 < ‖bumpFourier 0‖ := by - rw [norm_pos_iff] - intro hzero - have : (bumpFourier 0).re = 0 := by rw [hzero]; rfl - linarith - set v₀ := ‖bumpFourier 0‖ - obtain ⟨δ, hδ, hball⟩ := - (Metric.continuousAt_iff.mp hcts.continuousAt) (v₀ / 2) (by linarith) - refine ⟨(v₀ / 2) ^ 2, δ / 2, by positivity, by positivity, ?_⟩ - intro u hu - have hdist : dist (bumpFourier u) (bumpFourier 0) < v₀ / 2 := by - apply hball - rw [Real.dist_eq] - simp only [sub_zero] - exact lt_of_le_of_lt hu (by linarith) - have hbound : v₀ - ‖bumpFourier u‖ < v₀ / 2 := by - calc - v₀ - ‖bumpFourier u‖ = ‖bumpFourier 0‖ - ‖bumpFourier u‖ := rfl - _ ≤ ‖bumpFourier 0 - bumpFourier u‖ := norm_sub_norm_le _ _ - _ = dist (bumpFourier u) (bumpFourier 0) := by - rw [dist_eq_norm_sub, norm_sub_rev] - _ < v₀ / 2 := hdist - have hball' : v₀ / 2 < ‖bumpFourier u‖ := by linarith - nlinarith [norm_nonneg (bumpFourier u)] - -/-! ### Weighted Plancherel identity -/ - --- Package translates of the concrete bump as Schwartz functions. -private def bumpShift (w : ℝ) : 𝓢(ℝ, ℂ) := by - let f : ℝ → ℂ := fun x => (bump (x + w) : ℂ) - have hcomp : HasCompactSupport f := by - apply HasCompactSupport.of_support_subset_isCompact - (isCompact_Icc (a := -w - 1 / 4) (b := -w + 1 / 4)) - intro x hx - change (bump (x + w) : ℂ) ≠ 0 at hx - have hx' : bump (x + w) ≠ 0 := by exact_mod_cast hx - have h := abs_le.mp (bump_supp (x + w) hx') - constructor <;> linarith - have hsmooth : ContDiff ℝ ∞ f := by - change ContDiff ℝ ∞ ((fun x : ℝ => (bump x : ℂ)) ∘ fun x => x + w) - exact bump_complex_smooth.comp (contDiff_id.add contDiff_const) - exact hcomp.toSchwartzMap hsmooth - -private lemma bumpShift_apply (w x : ℝ) : bumpShift w x = bump (x + w) := rfl - -private lemma fourier_bumpShift (w u : ℝ) : - (𝓕 (bumpShift w : ℝ → ℂ)) u = - 𝐞 (w * u) * bumpFourier u := by - have hcoe : (bumpShift w : ℝ → ℂ) = fun x : ℝ => (bump (x + w) : ℂ) := by - ext x - exact_mod_cast bumpShift_apply w x - rw [hcoe, Real.fourier_real_eq] - have hpsi : bumpFourier u = - ∫ x : ℝ, 𝐞 (-(x * u)) * (bump x : ℂ) := by - simp only [bumpFourier] - apply integral_congr_ae - filter_upwards with x - ring - rw [hpsi] - have ht := congr_fun - (Fourier.fourierIntegral_comp_add_right 𝐞 volume (fun x : ℝ => (bump x : ℂ)) w) u - simpa [Fourier.fourierIntegral_def, Circle.smul_def, Real.fourierChar_apply] using ht - -private lemma bumpShift_inner_eq_zero {v w : ℝ} (hvw : 1 ≤ |v - w|) : - ∫ x : ℝ, inner ℂ (bumpShift v x) (bumpShift w x) = 0 := by - apply integral_eq_zero_of_ae - filter_upwards with x - by_cases hxv : bump (x + v) = 0 - · simp [bumpShift_apply, hxv] - by_cases hxw : bump (x + w) = 0 - · simp [bumpShift_apply, hxw] - exfalso - have hv := bump_supp (x + v) hxv - have hw := bump_supp (x + w) hxw - have hbound : |v - w| ≤ 1 / 2 := by - calc - |v - w| = |(x + v) - (x + w)| := by ring_nf - _ ≤ |x + v| + |x + w| := abs_sub _ _ - _ ≤ 1 / 4 + 1 / 4 := by linarith - _ = 1 / 2 := by norm_num - linarith - -private lemma bumpShift_inner_self (w : ℝ) : - ∫ x : ℝ, inner ℂ (bumpShift w x) (bumpShift w x) = 1 := by - calc - ∫ x : ℝ, inner ℂ (bumpShift w x) (bumpShift w x) = - ∫ x : ℝ, (((bump (x + w)) ^ 2 : ℝ) : ℂ) := by - apply integral_congr_ae - filter_upwards with x - simp [bumpShift_apply, abs_of_nonneg (bump_nonneg _)] - _ = ((∫ x : ℝ, (bump (x + w)) ^ 2 : ℝ) : ℂ) := integral_ofReal - _ = ((∫ x : ℝ, (bump x) ^ 2 : ℝ) : ℂ) := by - rw [integral_add_right_eq_self (fun x : ℝ => (bump x) ^ 2) w] - _ = 1 := by rw [bump_l2norm]; norm_num - -private lemma bumpShift_orthonormal {ι : Type*} [Finite ι] - (ξ : ι → ℝ) (N : ℝ) (hN : 0 < N) - (hsep : IsSeparatedFamily (1 / N) ξ) : - Orthonormal ℂ (fun r => (bumpShift (N * ξ r)).toLp 2) := by - classical - letI := Fintype.ofFinite ι - rw [orthonormal_iff_ite] - intro r s - rw [SchwartzMap.inner_toL2_toL2_eq - (bumpShift (N * ξ r)) (bumpShift (N * ξ s)) volume] - by_cases hrs : r = s - · subst s - rw [if_pos rfl, bumpShift_inner_self] - · rw [if_neg hrs] - apply bumpShift_inner_eq_zero - rw [show N * ξ r - N * ξ s = N * (ξ r - ξ s) by ring, abs_mul, abs_of_pos hN] - calc - 1 = N * (1 / N) := by field_simp - _ ≤ N * |ξ r - ξ s| := mul_le_mul_of_nonneg_left (hsep hrs) hN.le - private lemma weighted_l2_identity {ι : Type*} [Fintype ι] (a : ι → ℂ) (ξ : ι → ℝ) (N : ℝ) (hN : 0 < N) (t₀ : ℝ) (hsep : IsSeparatedFamily (1 / N) ξ) : diff --git a/Expdb/Mathlib/EulerMaclaurin.lean b/Expdb/Mathlib/EulerMaclaurin.lean index d2bee12..adbc007 100644 --- a/Expdb/Mathlib/EulerMaclaurin.lean +++ b/Expdb/Mathlib/EulerMaclaurin.lean @@ -3,7 +3,7 @@ module public import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas public import Mathlib.NumberTheory.ZetaValues -import Mathlib.MeasureTheory.Integral.DivergenceTheorem +import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts import Mathlib.Tactic.Abel import Mathlib.Tactic.Linarith import Mathlib.Tactic.Module @@ -104,42 +104,38 @@ private lemma saw_one {x : ℝ} : saw 1 x = Int.fract x - 1 / 2 := by @[simp] private lemma saw_one_zero : saw 1 0 = -2⁻¹ := by simp only [saw_one, Int.fract_zero, one_div, zero_sub] -/-! ## Non-explicit bounds -/ - -private lemma exists_max_bernoulli (s : ℕ) : - ∃ x ∈ Icc 0 1, IsMaxOn (fun x ↦ |bernoulliFun s x|) (Icc 0 1) x := by - apply isCompact_Icc.exists_isMaxOn - · exact nonempty_Icc.mpr zero_le_one - · exact (continuous_bernoulliFun s).abs.continuousOn - -private def bernoulliBound (s : ℕ) : ℝ := - |bernoulliFun s (exists_max_bernoulli s).choose| - -private lemma abs_bernoulliFun_le (s : ℕ) (x : ℝ) (m : x ∈ Icc 0 1) : - |bernoulliFun s x| ≤ bernoulliBound s := by - simp only [bernoulliBound] - obtain ⟨_, hmax⟩ := (exists_max_bernoulli s).choose_spec - exact hmax m - -private lemma bddAbove_range_abs_saw (s : ℕ) : - BddAbove (range fun x ↦ |saw s x|) := by - refine ⟨(s.factorial : ℝ)⁻¹ * bernoulliBound s, ?_⟩ - rintro _ ⟨x, rfl⟩ - have sp : 0 < (s.factorial : ℝ)⁻¹ := inv_pos.mpr (Nat.cast_pos.mpr (Nat.factorial_pos _)) - simp only [saw_eq_bernoulliFun_fract, abs_mul, abs_of_pos sp] - refine mul_le_mul_of_nonneg_left ?_ sp.le - exact abs_bernoulliFun_le _ _ (unitInterval.fract_mem x) - -/-- A uniform bound for the absolute value of `saw s`. -/ -def sawBound (s : ℕ) : ℝ := - sSup (range fun x ↦ |saw s x|) +/-! ## Explicit bounds -/ -private lemma abs_saw_le (s : ℕ) (x : ℝ) : |saw s x| ≤ sawBound s := by - exact le_csSup (bddAbove_range_abs_saw s) (mem_range_self x) +/-- An explicit uniform bound for the absolute value of `saw s`, obtained by summing the +absolute values of the coefficients of the `s`th Bernoulli polynomial. -/ +def sawBound (s : ℕ) : ℝ := + (s.factorial : ℝ)⁻¹ * ∑ i ∈ Finset.range (s + 1), + |(_root_.bernoulli (s - i) : ℝ) * (s.choose i : ℝ)| + +private lemma abs_bernoulliFun_le (s : ℕ) (x : ℝ) (hx : x ∈ Icc 0 1) : + |bernoulliFun s x| ≤ ∑ i ∈ Finset.range (s + 1), + |(_root_.bernoulli (s - i) : ℝ) * (s.choose i : ℝ)| := by + rw [bernoulliFun, Polynomial.bernoulli_def, Polynomial.map_sum, Polynomial.eval_finsetSum] + simp only [Polynomial.map_monomial, Polynomial.eval_monomial, map_mul, map_natCast] + refine (Finset.abs_sum_le_sum_abs _ _).trans ?_ + apply Finset.sum_le_sum + intro i hi + rw [abs_mul] + apply mul_le_of_le_one_right (abs_nonneg _) + rw [abs_pow] + exact pow_le_one₀ (abs_nonneg x) (abs_le.mpr ⟨by linarith [hx.1], hx.2⟩) + +/-- The absolute value of `saw s` is bounded by the explicit constant `sawBound s`. -/ +lemma abs_saw_le (s : ℕ) (x : ℝ) : |saw s x| ≤ sawBound s := by + have hs : 0 ≤ (s.factorial : ℝ)⁻¹ := by positivity + rw [saw_eq_bernoulliFun_fract, sawBound, abs_mul, abs_of_nonneg hs] + exact mul_le_mul_of_nonneg_left + (abs_bernoulliFun_le s _ (unitInterval.fract_mem x)) hs /-- The uniform bound for `saw` is nonnegative. -/ @[simp] lemma sawBound_nonneg {s : ℕ} : 0 ≤ sawBound s := by - exact (abs_nonneg (saw s 0)).trans (abs_saw_le s 0) + simp only [sawBound] + positivity /-! ## Euler--Maclaurin on one unit interval -/ @@ -181,29 +177,30 @@ private lemma presaw_smul_iteratedDeriv_by_parts [CompleteSpace E] have i1 : IntervalIntegrable (fun x ↦ presaw (s + 1) c x • iteratedDerivWithin (s + 1) f t x) volume (a : ℝ) (a + 1) := intervalIntegrable_presaw_smul (s := s + 1) (c := c) fc (by linarith) u abt + have ha : (a : ℝ) ≤ a + 1 := by norm_num rw [eq_sub_iff_add_eq, ← intervalIntegral.integral_add i0 i1] - set g := fun x ↦ presaw (s + 1) c x • iteratedDerivWithin s f t x - set g' := fun x ↦ presaw s c x • iteratedDerivWithin s f t x + - presaw (s + 1) c x • iteratedDerivWithin (s + 1) f t x - have df : ∀ x ∈ Ioo (a : ℝ) (a + 1) \ ∅, HasDerivAt g (g' x) x := by - intro x m - simp only [sdiff_empty] at m - simp only [g, g', add_comm (presaw s c _ • _) _] - apply HasDerivAt.smul - · exact hasDerivAt_presaw - · have mt := abt (Ioo_subset_Icc_self m) - apply HasDerivWithinAt.hasDerivAt - · rw [iteratedDerivWithin_succ, hasDerivWithinAt_derivWithin_iff] - apply (fc.contDiffWithinAt mt).differentiableWithinAt_iteratedDerivWithin - · simp only [← Nat.cast_add_one, Nat.cast_lt, Nat.lt_add_one] - · simp only [mt, insert_eq_of_mem, u] - · exact Filter.monotone_mem (subset_trans Ioo_subset_Icc_self abt) (isOpen_Ioo.mem_nhds m) - refine Eq.trans (MeasureTheory.integral_eq_of_hasDerivAt_off_countable_of_le - (f := g) (f' := g') (Hd := df) (by linarith) countable_empty ?_ ?_) ?_ - · apply contDiff_presaw.continuous.continuousOn.smul - exact (fc.continuousOn_iteratedDerivWithin le_self_add u).mono abt - · exact i0.add i1 - · simp only [g] + apply intervalIntegral.integral_deriv_smul_eq_sub_of_hasDeriv_right + · exact contDiff_presaw.continuous.continuousOn + · simpa only [uIcc_of_le ha] using + (fc.continuousOn_iteratedDerivWithin le_self_add u).mono abt + · intro x _ + exact hasDerivAt_presaw.hasDerivWithinAt + · intro x hx + have hx' : x ∈ Ioo (a : ℝ) (a + 1) := by + simpa [min_eq_left ha, max_eq_right ha] using hx + have mt := abt (Ioo_subset_Icc_self hx') + apply HasDerivAt.hasDerivWithinAt + apply HasDerivWithinAt.hasDerivAt + · rw [iteratedDerivWithin_succ, hasDerivWithinAt_derivWithin_iff] + apply (fc.contDiffWithinAt mt).differentiableWithinAt_iteratedDerivWithin + · simp only [← Nat.cast_add_one, Nat.cast_lt, Nat.lt_add_one] + · simp only [mt, insert_eq_of_mem, u] + · exact Filter.monotone_mem (subset_trans Ioo_subset_Icc_self abt) + (isOpen_Ioo.mem_nhds hx') + · exact contDiff_presaw.continuous.intervalIntegrable _ _ + · apply ContinuousOn.intervalIntegrable + simpa only [uIcc_of_le ha] using + (fc.continuousOn_iteratedDerivWithin le_rfl u).mono abt private lemma presaw_iterated_by_parts [CompleteSpace E] (fc : ContDiffOn ℝ (s + 1) f t) (u : UniqueDiffOn ℝ t) (abt : Icc (a : ℝ) (a + 1) ⊆ t) : diff --git a/Expdb/Mathlib/IteratedDeriv.lean b/Expdb/Mathlib/IteratedDeriv.lean new file mode 100644 index 0000000..ce10d4c --- /dev/null +++ b/Expdb/Mathlib/IteratedDeriv.lean @@ -0,0 +1,49 @@ +module + +public import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas + +/-! +# Supplementary lemmas for iterated derivatives + +This file contains chain rules that are useful in the exponential-sums development but are not +currently available in Mathlib in the required two-set form. +-/ + +@[expose] public section + +namespace Expdb + +/-- Iterated derivatives of a function precomposed with an affine map. Unlike Mathlib's +`iteratedDerivWithin_comp_const_smul`, the domain and codomain sets may be different. -/ +theorem iteratedDerivWithin_comp_affine_of_mapsTo + {f : ℝ → ℝ} {s t : Set ℝ} {x c d : ℝ} {n : ℕ} + (hf : ContDiffOn ℝ n f t) (hs : UniqueDiffOn ℝ s) (ht : UniqueDiffOn ℝ t) + (hx : x ∈ s) (hst : Set.MapsTo (fun y ↦ c * y + d) s t) : + iteratedDerivWithin n (fun y ↦ f (c * y + d)) s x = + c ^ n * iteratedDerivWithin n f t (c * x + d) := by + induction n generalizing x with + | zero => simp + | succ n ih => + have hcx : c * x + d ∈ t := hst hx + have heq : Set.EqOn + (iteratedDerivWithin n (fun y ↦ f (c * y + d)) s) + (fun y ↦ c ^ n * iteratedDerivWithin n f t (c * y + d)) s := + fun y hy ↦ ih hf.of_succ hy + have houter : DifferentiableWithinAt ℝ (iteratedDerivWithin n f t) t (c * x + d) := + hf.differentiableOn_iteratedDerivWithin (Nat.cast_lt.mpr n.lt_succ_self) ht _ hcx + have haffine : HasDerivWithinAt (fun y : ℝ ↦ c * y + d) c s x := by + simpa using (((hasDerivAt_id x).const_mul c).add_const d |>.hasDerivWithinAt) + have hcomp : DifferentiableWithinAt ℝ + (fun y ↦ iteratedDerivWithin n f t (c * y + d)) s x := by + change DifferentiableWithinAt ℝ + ((iteratedDerivWithin n f t) ∘ fun y ↦ c * y + d) s x + exact houter.comp x haffine.differentiableWithinAt hst + rw [iteratedDerivWithin_succ, derivWithin_congr heq (ih hf.of_succ hx), + derivWithin_const_mul _ hcomp, iteratedDerivWithin_succ, + ← Function.comp_def, derivWithin.scomp x houter + haffine.differentiableWithinAt hst] + rw [haffine.derivWithin (hs.uniqueDiffWithinAt hx)] + simp only [pow_succ] + ring + +end Expdb diff --git a/blueprint/src/chapter/beta.tex b/blueprint/src/chapter/beta.tex index 09f5cf6..5622f33 100644 --- a/blueprint/src/chapter/beta.tex +++ b/blueprint/src/chapter/beta.tex @@ -108,10 +108,13 @@ \section{Exponential sum exponent} \] Note the discontinuity at $1$. Despite this, we have: -\begin{lemma}[Upper semicontinuity]\label{beta-semicts}\uses{beta-triv} $\beta$ is an upper semicontinuous function. +\begin{lemma}[Upper semicontinuity]\label{beta-semicts}\uses{beta-triv} +\lean{Expdb.upperSemicontinuous_exponentSumGrowthExponent}\leanok +$\beta$ is an upper semicontinuous function. \end{lemma} -\begin{proof} Routine from the definition. +\begin{proof}\leanok +Routine from the definition. \end{proof} We record the classical bounds on $\beta$: diff --git a/blueprint/src/chapter/notation.tex b/blueprint/src/chapter/notation.tex index 97f34ce..aec6111 100644 --- a/blueprint/src/chapter/notation.tex +++ b/blueprint/src/chapter/notation.tex @@ -39,7 +39,7 @@ \section{Asymptotic (or ``cheap nonstandard'') notation} A convenient property of this asymptotic formalism, analogous to the property of \emph{$\omega$-saturation} in nonstandard analysis, is that certain asymptotic bounds are automatically uniform in variable parameters. \begin{proposition}[Automatic uniformity]\label{auto} -\lean{Expdb.automatic_uniformity_of_pointwise_bounded, Expdb.automatic_uniformity_of_pointwise_infinitesimal} +\lean{Expdb.automatic_uniformity_of_choicewise_bounded, Expdb.automatic_uniformity_of_choicewise_infinitesimal} \leanok Let $E = E_{\ii}$ be a non-empty variable set, and let $f = f_{\ii}: E \to \C$ be a variable function. \begin{itemize} \item[(i)] Suppose that $f(x)=O(1)$ for all (variable) $x \in E$. Then after passing to a subsequence if necessary, the bound is uniform, that is to say, there exists a fixed $C$ such that $|f(x)| \leq C$ for all $x \in E$. diff --git a/scripts/lean_declarations.txt b/scripts/lean_declarations.txt index ff569e0..b66e783 100644 --- a/scripts/lean_declarations.txt +++ b/scripts/lean_declarations.txt @@ -8,11 +8,12 @@ Expdb.VariableObject.fixed Expdb.VariableObject.IsBounded Expdb.VariableObject.IsUnbounded Expdb.VariableObject.isUnbounded_iff_forall_eventually_norm_ge +Expdb.VariableObject.isUnbounded_iff_tendsto_atTop Expdb.VariableObject.IsInfinitesimal Expdb.VariableObject.isInfinitesimal_iff_forall_pos Expdb.VariableFunction -Expdb.VariableFunction.IsPointwiseBounded -Expdb.VariableFunction.IsPointwiseInfinitesimal +Expdb.VariableFunction.IsChoicewiseBounded +Expdb.VariableFunction.IsChoicewiseInfinitesimal Expdb.IsEqUpToInfinitesimal Expdb.IsEqUpToInfinitesimal.refl Expdb.IsEqUpToInfinitesimal.symm @@ -26,28 +27,71 @@ Expdb.IsLEUpToInfinitesimal Expdb.isLEUpToInfinitesimal_iff_forall_pos Expdb.isEqUpToInfinitesimal_iff_leUpToInfinitesimal Expdb.underspill -Expdb.automatic_uniformity_of_pointwise_bounded -Expdb.automatic_uniformity_of_pointwise_infinitesimal -Expdb.VariableFunction.isPointwiseBounded_iff_eventually_uniform -Expdb.VariableFunction.isPointwiseInfinitesimal_iff_forall_pos_uniform +Expdb.automatic_uniformity_of_choicewise_bounded +Expdb.automatic_uniformity_of_choicewise_infinitesimal +Expdb.VariableFunction.isChoicewiseBounded_iff_eventually_uniform +Expdb.VariableFunction.isChoicewiseInfinitesimal_iff_forall_pos_uniform Expdb.phaseInterval Expdb.IsPhaseFunction +Expdb.modelPhase +Expdb.modelPhaseErrorAt +Expdb.modelPhaseErrorAt_add_linear Expdb.modelPhaseError +Expdb.modelPhaseError_apply +Expdb.uniqueDiffOn_phaseInterval +Expdb.contDiffOn_modelPhase +Expdb.iteratedDerivWithin_modelPhase +Expdb.norm_iteratedDerivWithin_modelPhase_le +Expdb.continuousOn_iteratedDerivWithin_modelPhase +Expdb.IsApproximateModelPhaseFunction +Expdb.IsApproximateModelPhaseFunction.add_linear +Expdb.IsModelPhaseFunctionWith Expdb.IsModelPhaseFunction +Expdb.IsModelPhaseFunctionWith.isModelPhaseFunction +Expdb.IsModelPhaseFunction.exists_with +Expdb.IsModelPhaseFunctionWith.add_infinitesimal_linear +Expdb.IsModelPhaseFunctionWith.comp_affine_tendsto_id +Expdb.IsModelPhaseFunctionWith.eventually_isApproximate Expdb.logPhase Expdb.iteratedDerivWithin_log_eq_rpow_neg_one Expdb.isModelPhaseFunction_log Expdb.IsModelPhaseFunction.exists_subsequence_uniform_error Expdb.IsPowerAsymptotic Expdb.IsPowerAsymptotic.eventually_between +Expdb.IsPowerAsymptotic.mul +Expdb.IsPowerAsymptotic.div +Expdb.IsPowerAsymptotic.tendsto_zero_of_neg +Expdb.IsPowerAsymptotic.tendsto_atTop_of_pos +Expdb.isPowerAsymptotic_self +Expdb.isPowerAsymptotic_zero_of_tendsto_one +Expdb.floorRpow +Expdb.floorRpow_pos +Expdb.tendsto_floorRpow_cast_div_rpow_one +Expdb.isPowerAsymptotic_floorRpow Expdb.isPowerAsymptotic_of_logb_tendsto +Expdb.isPowerAsymptotic_of_between_of_infinitesimal Expdb.isPowerAsymptotic_of_between Expdb.isPowerAsymptotic_of_between_const_rpow Expdb.IsPowerBounded +Expdb.IsPowerBounded.mono Expdb.isPowerBounded_iff_forall_pos Expdb.exponent_le_of_isPowerBounded_of_eventually_norm_ge_rpow +Expdb.oscillatory +Expdb.norm_oscillatory +Expdb.exponentialSumAt +Expdb.norm_exponentialSumAt_le_card +Expdb.norm_exponentialSumAt_le_add_one +Expdb.exponentialSumAt_self +Expdb.exponentialSumAt_of_lt +Expdb.HasPhaseDerivBound +Expdb.HasPhaseFirstDerivLowerBound +Expdb.HasPhaseDerivBound.of_le +Expdb.HasSmallEulerMaclaurinRemainder Expdb.exponentialSum +Expdb.exponentialSum_apply Expdb.IsExponentSumBound +Expdb.exponentSumBounds +Expdb.mem_exponentSumBounds Expdb.exponentSumGrowthExponent Expdb.IsExponentSumBound.mono Expdb.isExponentSumBound_self @@ -58,19 +102,56 @@ Expdb.isLeast_exponentSumGrowthExponent Expdb.exponentSumBounds_eq_Ici Expdb.isClosed_exponentSumBounds Expdb.isPowerBounded_logPhase -Expdb.exponentialSumAt -Expdb.IsApproximateModelPhaseFunction +Expdb.le_exponentSumGrowthExponent_of_logPhase_lower_bound +Expdb.IsModelPhaseSumSetupAt Expdb.IsExponentSumBoundNonAsymptotic Expdb.exponentSumGrowthExponent_le_iff_nonAsymptotic Expdb.exponentSumGrowthExponent_eq_sub_one Expdb.exponentSumGrowthExponent_mem_Icc Expdb.exponentSumGrowthExponent_zero +Expdb.exponentSumGrowthExponent_nonneg +Expdb.exponentSumGrowthExponent_le_self +Expdb.exponentialSumAt_dilate +Expdb.norm_exponentialSumAt_dilate_le +Expdb.residueScale +Expdb.residuePhase +Expdb.residuePhase_identity +Expdb.exponentialSumAt_residue +Expdb.norm_exponentialSumAt_le_sum_residues +Expdb.iteratedDerivWithin_comp_affine_of_mapsTo +Expdb.exponentSumGrowthExponent_monoOn_Icc +Expdb.exponentSumGrowthExponent_le_add_sub +Expdb.lipschitzOnWith_exponentSumGrowthExponent +Expdb.continuousOn_exponentSumGrowthExponent +Expdb.upperSemicontinuous_exponentSumGrowthExponent +Expdb.L2Bump.rawBump +Expdb.L2Bump.rawL2 +Expdb.L2Bump.bump +Expdb.L2Bump.bump_smooth +Expdb.L2Bump.bump_hasCompactSupport +Expdb.L2Bump.bump_supp +Expdb.L2Bump.bump_nonneg +Expdb.L2Bump.bump_l2norm +Expdb.L2Bump.bumpFourier +Expdb.L2Bump.bump_integrable +Expdb.L2Bump.bumpFourier_continuous +Expdb.L2Bump.bumpFourier_l2 +Expdb.L2Bump.bumpFourier_sq_integrable +Expdb.L2Bump.bumpFourier_decay +Expdb.L2Bump.bumpFourier_lower_bound +Expdb.L2Bump.bumpShift +Expdb.L2Bump.bumpShift_apply +Expdb.L2Bump.fourier_bumpShift +Expdb.L2Bump.bumpShift_orthonormal +Expdb.expSum +Expdb.expSum_continuous Expdb.l2_integral_estimate Expdb.l2_integral_estimate_error Expdb.l2_integral_estimate_exists_norm_sq_ge Expdb.log_div_separated Expdb.contDiff_fourierChar Expdb.iteratedDeriv_fourierChar +Expdb.norm_iteratedDeriv_fourierChar Expdb.norm_iteratedDerivWithin_oscillatory_le Expdb.contDiffOn_oscillatory Expdb.approximate_model_phase_deriv_bounds @@ -84,6 +165,7 @@ Expdb.norm_logPhaseMainTerm_bounds Expdb.exists_norm_logPhase_sum_sub_mainTerm_le Expdb.EulerMaclaurin.saw Expdb.EulerMaclaurin.sawBound +Expdb.EulerMaclaurin.abs_saw_le Expdb.EulerMaclaurin.sawBound_nonneg Expdb.EulerMaclaurin.sum_Icc_eq_integral_add Expdb.EulerMaclaurin.norm_sum_Icc_nat_sub_integral_le