def
definition
ContinuousCombinerPsiAffineCompletion
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.GeneralizedDAlembert on GitHub at line 557.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
of -
AczelSecondDerivativeIdentity -
LogBilinearIdentity -
SatisfiesLawsOfLogicContinuous -
ComparisonOperator -
derivedCost -
is -
of -
from -
is -
of -
is -
of -
is
used by
formal source
554of the combiner, and the Aczél equation force the actual log-bilinear identity.
555It is narrower than the former all-in ψ-affine forcing axiom because the
556second-derivative extraction is now named separately. -/
557def ContinuousCombinerPsiAffineCompletion
558 (C : ComparisonOperator)
559 (_h : SatisfiesLawsOfLogicContinuous C)
560 (_hSmooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
561 (fun t : ℝ => derivedCost C (Real.exp t)))
562 (_hDeriv : AczelSecondDerivativeIdentity (fun t : ℝ => derivedCost C (Real.exp t))) : Prop :=
563 ∃ c : ℝ, LogBilinearIdentity (fun t : ℝ => derivedCost C (Real.exp t)) c
564
565/-- Explicit package of the extra analysis needed to force bilinearity from
566an arbitrary continuous combiner. This is deliberately a hypothesis package,
567not an axiom. The quartic-log obstruction shows the package is not automatic
568from `SatisfiesLawsOfLogicContinuous`. -/
569structure ContinuousCombinerAnalysisInputs
570 (C : ComparisonOperator)
571 (h : SatisfiesLawsOfLogicContinuous C) : Prop where
572 finite_smoothness : ContinuousCombinerMollifierFiniteSmoothness C h
573 second_derivative :
574 ContinuousCombinerSecondDerivativeInput C h
575 (continuous_combiner_log_smoothness_bootstrap C h finite_smoothness)
576 psi_affine :
577 ContinuousCombinerPsiAffineCompletion C h
578 (continuous_combiner_log_smoothness_bootstrap C h finite_smoothness)
579 second_derivative
580
581/-- **Residual input 2 assembled:** smoothness plus the derivative identity
582and ψ-affine completion give the required log-bilinear identity. -/
583theorem continuous_combiner_psi_affine_forcing
584 (C : ComparisonOperator)
585 (h : SatisfiesLawsOfLogicContinuous C)
586 (hSmooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
587 (fun t : ℝ => derivedCost C (Real.exp t)))