BoundState.lean`

68 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SharpLiebThirring.ExtremizerProof.profile line 25
Source documentation
The positive, unnormalized bound state.
```
def profile (r x : ℝ) : ℝ := (Real.cosh (r * x)) ^ (-1 / r)
```
def OAI.SharpLiebThirring.ExtremizerProof.potential line 27
def OAI.SharpLiebThirring.ExtremizerProof.profileDerivative line 29
lemma OAI.SharpLiebThirring.ExtremizerProof.profile_pos line 31
lemma OAI.SharpLiebThirring.ExtremizerProof.profile_continuous line 34
lemma OAI.SharpLiebThirring.ExtremizerProof.profile_contDiff line 38
lemma OAI.SharpLiebThirring.ExtremizerProof.profile_hasDerivAt line 42
lemma OAI.SharpLiebThirring.ExtremizerProof.tanh_hasDerivAt line 52
lemma OAI.SharpLiebThirring.ExtremizerProof.tanh_sq_add_sech_sq line 62
lemma OAI.SharpLiebThirring.ExtremizerProof.profileDerivative_hasDerivAt line 70
lemma OAI.SharpLiebThirring.ExtremizerProof.profileDerivative_continuous line 80
lemma OAI.SharpLiebThirring.ExtremizerProof.potential_continuous line 86
lemma OAI.SharpLiebThirring.ExtremizerProof.potential_nonneg line 91
lemma OAI.SharpLiebThirring.ExtremizerProof.cosh_lower_exponential line 95
lemma OAI.SharpLiebThirring.ExtremizerProof.profile_exponential_bound line 100
lemma OAI.SharpLiebThirring.ExtremizerProof.profileDerivative_exponential_bound line 115
lemma OAI.SharpLiebThirring.ExtremizerProof.integrable_exp_neg_abs line 122
lemma OAI.SharpLiebThirring.ExtremizerProof.memLp_exp_neg_abs line 141
lemma OAI.SharpLiebThirring.ExtremizerProof.profile_memLp line 152
lemma OAI.SharpLiebThirring.ExtremizerProof.profileDerivative_memLp line 160
def OAI.SharpLiebThirring.SobolevProof.baseCutoff line 173
Source documentation
Fixed smooth compact cutoff, equal to one on [-1,1].
```
def baseCutoff : ContDiffBump (0 : ℝ) := ⟨1, 2, by norm_num, by norm_num⟩
```
def OAI.SharpLiebThirring.SobolevProof.cutoff line 175
def OAI.SharpLiebThirring.SobolevProof.cutoffDerivative line 177
lemma OAI.SharpLiebThirring.SobolevProof.baseCutoff_smooth line 180
lemma OAI.SharpLiebThirring.SobolevProof.scale_pos line 182
lemma OAI.SharpLiebThirring.SobolevProof.cutoff_contDiff line 184
lemma OAI.SharpLiebThirring.SobolevProof.cutoff_compact line 187
lemma OAI.SharpLiebThirring.SobolevProof.cutoff_hasDerivAt line 192
lemma OAI.SharpLiebThirring.SobolevProof.cutoffDerivative_continuous line 200
lemma OAI.SharpLiebThirring.SobolevProof.cutoff_bound line 204
lemma OAI.SharpLiebThirring.SobolevProof.scale_tendsto line 209
lemma OAI.SharpLiebThirring.SobolevProof.cutoff_tendsto line 212
lemma OAI.SharpLiebThirring.SobolevProof.cutoffDerivative_uniform_bound line 221
lemma OAI.SharpLiebThirring.SobolevProof.cutoffDerivative_tendsto line 235

lemma OAI.SharpLiebThirring.SobolevProof.integral_multiplier_tendsto line 242

Source documentation

Dominated convergence for a uniformly bounded multiplier of an L¹ function.

lemma integral_multiplier_tendsto {a : ℕ → ℝ → ℂ} {l : ℂ} {g : ℝ → ℂ}
    (hg : Integrable g) (ha : ∀ n, AEStronglyMeasurable (a n) volume)
    {D : ℝ} (_hD : 0 ≤ D) (hb : ∀ n x, ‖a n x‖ ≤ D)
    (hl : ∀ x, Tendsto (fun n ↦ a n x) atTop (𝓝 l)) :
    Tendsto (fun n ↦ ∫ x : ℝ, a n x * g x) atTop (𝓝 (∫ x : ℝ, l * g x)) := by
…

lemma OAI.SharpLiebThirring.SobolevProof.weak_derivative_smooth_L2 line 265
Source documentation
Extend the distributional H¹ identity from compactly supported tests to smooth L² tests with L² classical derivative. No pointwise representative of an arbitrary H¹ element is assumed.
```
lemma weak_derivative_smooth_L2 (v : H1) {f f' : ℝ → ℂ}
    (hf : ContDiff ℝ ∞ f) (hd : ∀ x, HasDerivAt f (f' x) x)
    (hf2 : MemLp f 2 volume) (hf'2 : MemLp f' 2 volume) :
    (∫ x : ℝ, v.val x * f' x) = -(∫ x : ℝ, v.grad x * f x) := by
…
```
Mentions: OAI.SharpLiebThirring.H1
def OAI.SharpLiebThirring.SobolevProof.smoothH1 line 328
Source documentation
Classical smooth L² functions with L² derivative belong to the exact weak H¹ domain.
```
def smoothH1 (f f' : ℝ → ℂ) (hf : ContDiff ℝ ∞ f)
    (hd : ∀ x, HasDerivAt f (f' x) x) (hfc : Continuous f')
    (hf2 : MemLp f 2 volume) (hf'2 : MemLp f' 2 volume) : H1 where
…
```
Mentions: OAI.SharpLiebThirring.H1
lemma OAI.SharpLiebThirring.ExtremizerProof.potential_le line 351
lemma OAI.SharpLiebThirring.ExtremizerProof.potential_contDiff line 357
lemma OAI.SharpLiebThirring.ExtremizerProof.profileDerivative_contDiff line 363
def OAI.SharpLiebThirring.ExtremizerProof.profileSecond line 372
lemma OAI.SharpLiebThirring.ExtremizerProof.profileSecond_continuous line 374
lemma OAI.SharpLiebThirring.ExtremizerProof.profileSecond_memLp line 377
def OAI.SharpLiebThirring.ExtremizerProof.boundState line 389
Source documentation
The exact unnormalized extremizing bound state, as an element of the weak form domain.
```
def boundState (r : ℝ) (hr : 0 < r) : H1 :=
…
```
Mentions: OAI.SharpLiebThirring.H1
lemma OAI.SharpLiebThirring.ExtremizerProof.boundState_weak_ode line 397
lemma OAI.SharpLiebThirring.ExtremizerProof.boundState_negativeEigenfunction line 413
def OAI.SharpLiebThirring.scaleH1 line 448
Source documentation
Scalar multiplication in the weak form domain, without choosing pointwise representatives.
```
def scaleH1 (c : ℂ) (u : H1) : H1 where
…
```
Mentions: OAI.SharpLiebThirring.H1
lemma OAI.SharpLiebThirring.l2Pairing_scale_both line 457
lemma OAI.SharpLiebThirring.l2Pairing_scale_right line 466
lemma OAI.SharpLiebThirring.schrodingerForm_scale_right line 472
lemma OAI.SharpLiebThirring.IsNegativeEigenfunction.scale line 480
lemma OAI.SharpLiebThirring.oneStateMoment_le_negativeMoment line 487
lemma OAI.SharpLiebThirring.oneStateConstant_le_optimalConstant line 503
lemma OAI.SharpLiebThirring.ExtremizerProof.profile_norm_integrable line 518
lemma OAI.SharpLiebThirring.ExtremizerProof.profile_norm_pos line 526
lemma OAI.SharpLiebThirring.ExtremizerProof.boundState_l2Pairing line 536
def OAI.SharpLiebThirring.ExtremizerProof.normalizedBoundState line 547
lemma OAI.SharpLiebThirring.ExtremizerProof.normalizedBoundState_norm line 550
lemma OAI.SharpLiebThirring.ExtremizerProof.normalizedBoundState_eigenfunction line 561
lemma OAI.SharpLiebThirring.ExtremizerProof.one_le_oneStateMoment line 565
lemma OAI.SharpLiebThirring.ExtremizerProof.one_le_negativeMoment line 574
lemma OAI.SharpLiebThirring.ExtremizerProof.memLp_exp_neg_mul_abs line 584
lemma OAI.SharpLiebThirring.ExtremizerProof.cosh_inv_exponential_bound line 596
lemma OAI.SharpLiebThirring.ExtremizerProof.potential_exponential_bound line 603
lemma OAI.SharpLiebThirring.ExtremizerProof.potential_memLp line 613
lemma OAI.SharpLiebThirring.ExtremizerProof.equalityPotential_admissible line 621
lemma OAI.SharpLiebThirring.ExtremizerProof.potential_pos line 628
lemma OAI.SharpLiebThirring.ExtremizerProof.potential_mass_pos line 632