OAI/Probability/InvariantIsing/Fields/FieldTiltedFamilyDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Differentiating a normalized scalar Gaussian average with a varying observable. The local envelopes allow the affine-noise quadratic terms needed in the second derivative of the finite Ising recursion.

  1. def OAI.InvariantIsing.fieldWeightDifferential line 17

    Source documentation

    Derivative of the unnormalized Gaussian weight.

    def fieldWeightDifferential (U : (ℝ × ℝ) → ℝ → ℝ)
    (DU : (ℝ × ℝ) → ℝ → (ℝ × ℝ) →L[ℝ] ℝ) (ζ : ℝ)
    (p : ℝ × ℝ) (u : ℝ) : (ℝ × ℝ) →L[ℝ] ℝ :=
…
  2. def OAI.InvariantIsing.fieldObservableDifferential line 23

    Source documentation

    Derivative of the weighted observable.

    def fieldObservableDifferential (U A : (ℝ × ℝ) → ℝ → ℝ)
    (DU DA : (ℝ × ℝ) → ℝ → (ℝ × ℝ) →L[ℝ] ℝ) (ζ : ℝ)
    (p : ℝ × ℝ) (u : ℝ) : (ℝ × ℝ) →L[ℝ] ℝ :=
…
  3. lemma OAI.InvariantIsing.field_tiltedFamily_hasFDerivAt line 28