claimroutineinferred_dep

Return passage to inner radius

Return passage gives H(0,r)≳m(b)D−1log⁡(r/b)/log⁡(1/b)H(0,r)\gtrsim m(b)D^{-1}\log(r/b)/\log(1/b)
second 1/D1/D loss; completes the cylinder bound
Claim·§6 Propagation across a thin cylinder·inside lemPropagation across a thin cylinder

Statement (paper)

For b≤r≤1b\le r\le1, H(0,r)≥c(M) m(b)D log⁡(r/b)log⁡(1/b)H(0,r)\ge \dfrac{c(M)\,m(b)}{D}\,\dfrac{\log(r/b)}{\log(1/b)}. This yields , since sin⁡(πT/3)\sin(\pi T/3) is bounded below on [1,2][1,2].

In plain English

For b≤r≤1b\le r\le 1, the circular mean at T=0T=0 satisfies H(0,r)≥c(M) m(b) D−1 log⁡(r/b)/log⁡(1/b)H(0,r)\ge c(M)\,m(b)\,D^{-1}\,\log(r/b)/\log(1/b), where m(b)m(b) is the sine-weighted mean of H(⋅,b)H(\cdot,b). This gives the lemma's propagation bound, because sin⁡(πT/3)\sin(\pi T/3) is bounded below on [1,2][1,2].

Why it's here

The Harnack bound gives H(T,1)≥c m(b)/DH(T,1)\ge c\,m(b)/D for ∣T∣≤1|T|\le1. The log-affine comparison from the first claim then carries this lower bound from radius 1 down to radius rr, which produces the factor log⁡(r/b)/log⁡(1/b)\log(r/b)/\log(1/b). Combined with the earlier 1/D1/D loss this gives log⁡(r/b)/D2\log(r/b)/D^2, and replacing m(b)m(b) by ∫12H(T,b) dT\int_1^2 H(T,b)\,dT finishes the lemma.
Classified routine:
A direct combination of the earlier claims: the Harnack lower bound on the unit circle (claim-lem-cylinder-3) is carried from radius 1 down to radius r by the log-affine comparison (claim-lem-cylinder-1). This is a standard maximum-principle/comparison step for radial ODEs.

Uses

claimRadial solutions dominate log-affine interpolantsclaimHarnack lower bound on unit circle

Used by

Nothing in the paper

Figures

Two side-by-side rectangles in the $(T,s)$ plane, with $s=|\tau|$ drawn schematically. Panel (a), "Outward comparison", spans $0\le T\le3$ and $b\le s\le3$. A thick orange segment labelled "observed wave" lies on the bottom wall $s=b$ for $1\le T\le2$, and a shaded band $3/4\le s\le5/4$ is centred on a dashed line at $s=1$; below it is the factor at $s=1$, $\log 3/\log(3/b)$. Panel (b), "Inward comparison", spans $-1\le T\le1$ and $b\le s\le1$. Its thick teal top wall at $s=1$ is labelled "uniform lower bound", and dashed guides mark an orange dot at $(0,2b)$ labelled $H(0,2b)$; below it is the factor at $s=2b$, $\log 2/\log(1/b)$. Together the panels show the two logarithmic losses incurred in carrying the energy out to $s=1$ and back to the inner wall.
Figure 2schematicp. 22
The two comparisons, with radii s=∣τ∣s=|\tau| drawn schematically. The boundary mass on 1≤T≤21\le T\le2 bounds the mass in the shaded band from below. The mean inequality on a fixed annulus supplies a lower bound on the entire upper wall in (b). The two displayed fractions are values of the normalized radial harmonic functions. The comparison solutions with potential dominate fixed multiples of these values, giving the factor [log⁡(3/b)]−2[\log(3/b)]^{-2} at the dot. In the wave estimate, b=2Khb=2Kh: HH controls the wave norm on the marked segment and is controlled by the initial data at the dot.
What it shows
Two side-by-side rectangles in the (T,s)(T,s) plane, with s=∣τ∣s=|\tau| drawn schematically. Panel (a), "Outward comparison", spans 0≤T≤30\le T\le3 and b≤s≤3b\le s\le3. A thick orange segment labelled "observed wave" lies on the bottom wall s=bs=b for 1≤T≤21\le T\le2, and a shaded band 3/4≤s≤5/43/4\le s\le5/4 is centred on a dashed line at s=1s=1; below it is the factor at s=1s=1, log⁡3/log⁡(3/b)\log 3/\log(3/b). Panel (b), "Inward comparison", spans −1≤T≤1-1\le T\le1 and b≤s≤1b\le s\le1. Its thick teal top wall at s=1s=1 is labelled "uniform lower bound", and dashed guides mark an orange dot at (0,2b)(0,2b) labelled H(0,2b)H(0,2b); below it is the factor at s=2bs=2b, log⁡2/log⁡(1/b)\log 2/\log(1/b). Together the panels show the two logarithmic losses incurred in carrying the energy out to s=1s=1 and back to the inner wall.
Read from the image by claude-opus-5.5 · confidence 88%
SupportslemPropagation across a thin cylinderclaimOutward passage bounds band massclaimHarnack lower bound on unit circleclaimReturn passage to inner radiusclaimRadial solutions dominate log-affine interpolants

Sources

PaperOpen
Section
§6 Propagation across a thin cylinder
Page
—
Label
—
Line
sections/propagation.tex:94
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Return passage to inner radius" rests on claim-lem-cylinder-1
  • info
    inferred_dep
    outline: "Return passage to inner radius" rests on claim-lem-cylinder-3