OAI/Analysis/BernoulliCone/TraceBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.DeSilvaJerison.radiusSq_zero_coordinate line 11
2. lemma OAI.Bernoulli.DeSilvaJerison.radiusSq_pos_ae line 19
3. lemma OAI.Bernoulli.DeSilvaJerison.boundary_signed_slope line 42
4. lemma OAI.Bernoulli.DeSilvaJerison.boundary_outer_eventually line 51
5. lemma OAI.Bernoulli.DeSilvaJerison.upperFlux_boundary_trace line 73
6. theorem OAI.Bernoulli.DeSilvaJerison.upperFlux_zero_trace_bound line 87

   Source documentation

   Full zero-phase upper trace bound, including the conical boundary. Only the null axis is excluded; no assertion about the boundary's measure is used.

   theorem upperFlux_zero_trace_bound {x:Space 7} (hq:0<Cylindrical.radiusSq axis x)
       (hU:U x=0) {η:ℝ} (hη:0<η) :
       ∀ᶠ t:ℝ in 𝓝[>] 0,‖upperFlux (x,t)‖^2<1+η := by
   …

   Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.Cylindrical.radiusSq, OAI.Bernoulli.DeSilvaJerison.axis, OAI.Bernoulli.DeSilvaJerison.U, OAI.Bernoulli.DeSilvaJerison.upperFlux