No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
257theorem transfer_function_eq_one_plus_kernel (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) :
258 transfer_function_complex H ω =
259 (1 : ℂ) + (H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ)) := by
proof body
Term-mode proof.
260 simp [transfer_function_complex]
261
262
263/-- The paper’s real-valued response function is the real part of the complex transfer function. -/
depends on (13)
Lean names referenced from this declaration's body.
-
H
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
H
in IndisputableMonolith.Cost.FunctionalEquation
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
TransferFunction
in IndisputableMonolith.Gravity.CaldeiraLeggett
decl_use
-
transfer_function_complex
in IndisputableMonolith.Gravity.CausalKernelChain
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use