Formalised upper semicontinuity of beta

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

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

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