OAI/Probability/InvariantIsing/Fields/FieldFiniteTiltDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Normalized Gaussian differentiation for the finite vector of field covariance coordinates and the spatial coordinate.

  1. def OAI.InvariantIsing.fieldFiniteWeightDifferential line 18

    Source documentation

    Derivative of the unnormalized Gaussian weight.

    def fieldFiniteWeightDifferential (U : (FieldCovariate n) → ℝ → ℝ)
    (DU : (FieldCovariate n) → ℝ → (FieldCovariate n) →L[ℝ] ℝ) (ζ : ℝ)
    (p : FieldCovariate n) (u : ℝ) : (FieldCovariate n) →L[ℝ] ℝ :=
…

    Mentions: OAI.InvariantIsing.FieldCovariate

  2. def OAI.InvariantIsing.fieldFiniteObservableDifferential line 24

    Source documentation

    Derivative of the weighted observable.

    def fieldFiniteObservableDifferential (U A : (FieldCovariate n) → ℝ → ℝ)
    (DU DA : (FieldCovariate n) → ℝ → (FieldCovariate n) →L[ℝ] ℝ) (ζ : ℝ)
    (p : FieldCovariate n) (u : ℝ) : (FieldCovariate n) →L[ℝ] ℝ :=
…

    Mentions: OAI.InvariantIsing.FieldCovariate

  3. lemma OAI.InvariantIsing.field_finite_tiltedFamily_hasFDerivAt line 29
  4. lemma OAI.InvariantIsing.field_finite_tiltedFamily_covariance_hasFDerivAt line 99
  5. lemma OAI.InvariantIsing.field_finite_gaussianPair_hasFDerivAt line 131
  6. lemma OAI.InvariantIsing.field_finite_average_hasFDerivAt_of_envelope line 212