production module

`AutoSamplingTheory.TechnicalLemmas.InformationTheory.SimultaneousFDivergence`

2 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/InformationTheory/SimultaneousFDivergence.lean.

Imports

Mathlib.Analysis.Calculus.Deriv.Comp externalMathlib.Analysis.Calculus.Deriv.Inv externalMathlib.Analysis.Calculus.Deriv.Mul externalMathlib.Tactic external

Imported by

AutoSamplingTheory.TechnicalLemmas.InformationTheoryAutoSamplingTheory.TechnicalLemmas.InformationTheory.SimultaneousFDivergenceGradientAutoSamplingTheory.TechnicalLemmas.InformationTheory.SimultaneousFDivergenceIntegralTests.SimultaneousFDivergence

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.InformationTheory.SimultaneousFDivergence.hasDerivAt_weighted_f_divergence_integrand Partial Not mapped

- Weighted quotient chain rule underlying simultaneous `f`-divergence flows. The nonzero denominator is the local positivity condition on the reference density.

theorem hasDerivAt_weighted_f_divergence_integrand
    {p q f : ℝ → ℝ} {t pdot qdot fprime : ℝ}
    (hq : q t ≠ 0)
    (hp : HasDerivAt p pdot t)
    (hqderiv : HasDerivAt q qdot t)
    (hf : HasDerivAt f fprime (p t / q t)) :
    HasDerivAt
      (fun s => q s * f (p s / q s))
      (fprime * pdot +
        (f (p t / q t) - (p t / q t) * fprime) * qdot) t := by
  have hratio :
      HasDerivAt (fun s => p s / q s)
        ((pdot * q t - p t * qdot) / (q t) ^ 2) t :=
    hp.div hqderiv hq
  have hcomp :
      HasDerivAt (fun s => f (p s / q s))
        (fprime * ((pdot * q t - p t * qdot) / (q t) ^ 2)) t :=
    hf.comp t hratio
  have hprod := hqderiv.mul hcomp
  have hcoeff :
      qdot * f (p t / q t) +
          q t * (fprime * ((pdot * q t - p t * qdot) / (q t) ^ 2)) =
        fprime * pdot +
          (f (p t / q t) - (p t / q t) * fprime) * qdot := by
    field_simp [hq]
    ring
  rw [hcoeff] at hprod
  exact hprod

/-- The same identity with the ratio named explicitly. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/SimultaneousFDivergence.lean:30published source at 0e31a3cda412

theorem

AutoSamplingTheory.TechnicalLemmas.InformationTheory.SimultaneousFDivergence.hasDerivAt_weighted_f_divergence_integrand_of_ratio

Partial Not mapped

- The same identity with the ratio named explicitly.

theorem hasDerivAt_weighted_f_divergence_integrand_of_ratio
    {p q f : ℝ → ℝ} {t pdot qdot fprime rho : ℝ}
    (hq : q t ≠ 0) (hrho : rho = p t / q t)
    (hp : HasDerivAt p pdot t)
    (hqderiv : HasDerivAt q qdot t)
    (hf : HasDerivAt f fprime rho) :
    HasDerivAt
      (fun s => q s * f (p s / q s))
      (fprime * pdot + (f rho - rho * fprime) * qdot) t := by
  subst rho
  exact hasDerivAt_weighted_f_divergence_integrand hq hp hqderiv hf

end SimultaneousFDivergence
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/InformationTheory/SimultaneousFDivergence.lean:60published source at 0e31a3cda412