module module

`IndisputableMonolith.RRF.Models.Quadratic`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.RRF.Models module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.RRF.Core module_import

declarations in this module (16)

def quadratic1DStrain L23
theorem quadratic1D_equilibrium L30
theorem quadratic1D_unique_equilibrium L34
theorem quadratic1D_minimizer L39
theorem quadratic1D_hasUniqueMin L45
def quadratic1DLedger L55
theorem quadratic1D_ledger_closed L59
def quadratic1DStrainLedger L62
theorem quadratic1D_zero_valid L67
def quadratic1DChannel L73
def quadratic1DOctave L78
theorem quadratic1DOctave_wellPosed L88
def shiftedQuadraticStrain L94
theorem shifted_equilibrium L100
theorem shifted_is_minimizer L103
theorem exp_preserves_argmin L112