Fixed Wall Data and a Singular Layer

Exact root statement

(∀ (epsilon : ℝ),
    0 < epsilon →
      ∀ (time x y : ℝ),
        (layer epsilon).FullPlanarFlowAt time x y ∧ (layer epsilon).retainedTangentialResidual time x y = 0) ∧
  (∀ (epsilon time x : ℝ), (layer epsilon).tangential time x 0 = Real.cos time ∧ (layer epsilon).normal time x 0 = 0) ∧
    Filter.Tendsto (fun epsilon => (layer epsilon).viscosity) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) ∧
      (∀ (time y : ℝ),
          0 < y → Filter.Tendsto (fun epsilon => velocity epsilon time y) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) ∧
        ¬TendstoUniformlyOn (fun epsilon y => velocity epsilon 1 y) (fun x => 0) (nhdsWithin 0 (Set.Ioi 0)) (Set.Ioi 0)