One-log and double-log bounds on actual torus functions

DefinitionOne-log bound with coefficient \(c\) and constant \(K\)#✓fully proved

For real numbers \(c\) and \(K\), the one-log bound holds when every continuous function \(u : \mathbb{T} \to \mathbb{R}\) on the torus \(\mathbb{T} = (\mathbb{R}/2\pi\mathbb{Z})^2\) that is a zero-mean \(H^2\) function, has gradient energy \(E(u) > 0\) and has frequency ratio \(\delta(u) \ge 1\) (the Laplacian energy divided by \(E(u)\)) satisfies, at every point \(x \in \mathbb{T}\),

\[u(x)^2 \le c\,E(u)\bigl(\log\delta(u) + K\bigr).\]

def OneLogBound (c K : ℝ) : Prop :=
  ∀ u : C(Torus, ℝ), IsZeroMeanH2 u → 0 < gradientEnergy u → 1 ≤ frequencyRatio u →
    ∀ x : Torus, (u x) ^ 2 ≤ c * gradientEnergy u * (Real.log (frequencyRatio u) + K)

Uses 4 · Used by 1

Statement usesZero-mean \(H^2\) functions · The torus of period \(2\pi\) · Frequency ratio · Gradient energy

Used byOptimal one-log coefficient

DefinitionDouble-log bound with coefficient \(a\) and constant \(L\)#✓fully proved

For real numbers \(a\) and \(L\), the double-log bound holds when every continuous function \(u : \mathbb{T} \to \mathbb{R}\) on the torus \(\mathbb{T} = (\mathbb{R}/2\pi\mathbb{Z})^2\) that is a zero-mean \(H^2\) function, has gradient energy \(E(u) > 0\) and has frequency ratio \(\delta(u) \ge 1\) (the Laplacian energy divided by \(E(u)\)) satisfies, at every point \(x \in \mathbb{T}\),

\[u(x)^2 \le \frac{E(u)}{4\pi}\bigl(\log\delta(u) + a\log\bigl(1 + \log\delta(u)\bigr) + L\bigr).\]

The inner logarithm is taken of \(1 + \log\delta(u)\), which is at least \(1\) because \(\delta(u) \ge 1\).

def DoubleLogBound (a L : ℝ) : Prop :=
  ∀ u : C(Torus, ℝ), IsZeroMeanH2 u → 0 < gradientEnergy u → 1 ≤ frequencyRatio u →
    ∀ x : Torus, (u x) ^ 2 ≤ gradientEnergy u / (4 * Real.pi) *
      (Real.log (frequencyRatio u) + a * Real.log (1 + Real.log (frequencyRatio u)) + L)

Uses 4

Statement usesZero-mean \(H^2\) functions · The torus of period \(2\pi\) · Frequency ratio · Gradient energy

DefinitionOptimal one-log coefficient#✓fully proved

The infimum, taken in the extended reals, of all real numbers \(c\) for which there is a real constant \(K\) such that the one-log bound with coefficient \(c\) and constant \(K\) holds. It is \(+\infty\) when no such \(c\) exists.

def oneLogLeadingCoefficientInfimum : EReal :=
  sInf ((fun c : ℝ ↦ (c : EReal)) '' {c | ∃ K : ℝ, OneLogBound c K})

Uses 1

Statement usesOne-log bound with coefficient \(c\) and constant \(K\)

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.