abbrev definition def or abbrev

`Kernel`

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

formal statement (Lean)

  22abbrev Kernel := ℝ → ℝ → ℝ

proof body

Definition body.

  23
  24/- Effective source in Poisson/growth (ILG display): 4π G a^2 ρ w δ. -/

used by (23)

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

no_retuning_consistent in IndisputableMonolith.Gravity.CoerciveProjection decl_use
eight_tick_resonance_certified in IndisputableMonolith.Gravity.EightTickResonance decl_use
interpolation_cost_zero_at_integer in IndisputableMonolith.Gravity.EightTickResonance decl_use
eightTickKernelParams in IndisputableMonolith.ILG.Kernel decl_use
eightTickKernelParams_C in IndisputableMonolith.ILG.Kernel decl_use
kernel_at_ratio_one_alpha_zero in IndisputableMonolith.ILG.Kernel decl_use
kernelAtRefK_eq in IndisputableMonolith.ILG.Kernel decl_use
kernel_ge_one in IndisputableMonolith.ILG.Kernel decl_use
kernel_pos in IndisputableMonolith.ILG.Kernel decl_use
effectiveSource in IndisputableMonolith.ILG.PressureForm decl_use
effectiveSource_pressure in IndisputableMonolith.ILG.PressureForm decl_use
pressure in IndisputableMonolith.ILG.PressureForm decl_use
source_equiv in IndisputableMonolith.ILG.PressureForm decl_use
angleAt in IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle decl_use
mellinIntegrand_reflect_pointwise in IndisputableMonolith.NumberTheory.MellinTransform decl_use
low_accel_saturated in IndisputableMonolith.Unification.BandwidthSaturation decl_use
Kernel in IndisputableMonolith.YM.OS decl_use
MassGap in IndisputableMonolith.YM.OS decl_use
mass_gap_of_OS_PF in IndisputableMonolith.YM.OS decl_use
OSPositivity in IndisputableMonolith.YM.OS decl_use
OverlapLowerBoundOS in IndisputableMonolith.YM.OS decl_use
TransferOperator in IndisputableMonolith.YM.OS decl_use
TransferPFGap in IndisputableMonolith.YM.OS decl_use

depends on (5)

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
Kernel in IndisputableMonolith.YM.OS decl_use