RootClauseAEndpointC1 #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
1. The boundary half of clause (A) at the frozen binder block #
def
Algsuperdiff.Section4.Provider.Regularity.RootDisplayClauseABoundaryC1Ae
{d : ℕ}
(M : Section3.ABKModel d)
(C1 Cest alpha : ℝ)
:
Clause (A) of the a.e. lattice display at the boundary centres, frozen binders.
RootClauseABoundary.RootDisplayClauseABoundaryAe's body, character for
character, with the root's two printed datum binders — the scale-weighted sup
bound on ∇h and the classical C¹ tie Support.HasGradientOn — inserted in
the root's own order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algsuperdiff.Section4.Provider.Regularity.RootDisplayClauseABoundaryC1Ae.mono_const
{d : ℕ}
[NeZero d]
{M : Section3.ABKModel d}
{C1 Cest Cest' alpha : ℝ}
(hle : Cest ≤ Cest')
(h : RootDisplayClauseABoundaryC1Ae M C1 Cest alpha)
:
RootDisplayClauseABoundaryC1Ae M C1 Cest' alpha