AutoSamplingTheory.TechnicalLemmas.InformationTheory.SimultaneousFDivergenceGradient

- Pointwise cancellation of the two gradient pairings in a simultaneous common-diffusion `f`-divergence calculation.

theorem common_diffusion_pairing_eq
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (q rho fpp : ℝ) (gradQ gradRho : E) :
    inner ℝ (fpp • gradRho) (rho • gradQ + q • gradRho) +
        inner ℝ ((-rho * fpp) • gradRho) gradQ =
      q * fpp * ‖gradRho‖ ^ 2 := by
  rw [inner_add_right, real_inner_smul_left, real_inner_smul_right,
    real_inner_smul_left, real_inner_smul_right,
    real_inner_smul_left, real_inner_self_eq_norm_sq]
  ring

/-- Source-shaped variant where the three gradient expressions have already
been identified and are supplied by equality hypotheses. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/SimultaneousFDivergenceGradient.lean:29published source at 0e31a3cda412

- Source-shaped variant where the three gradient expressions have already been identified and are supplied by equality hypotheses.

theorem common_diffusion_pairing_eq_of_gradients
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (q rho fpp : ℝ)
    (gradP gradQ gradRho gradFPrime gradComp : E)
    (hgradP : gradP = rho • gradQ + q • gradRho)
    (hgradFPrime : gradFPrime = fpp • gradRho)
    (hgradComp : gradComp = (-rho * fpp) • gradRho) :
    inner ℝ gradFPrime gradP + inner ℝ gradComp gradQ =
      q * fpp * ‖gradRho‖ ^ 2 := by
  rw [hgradP, hgradFPrime, hgradComp]
  exact common_diffusion_pairing_eq q rho fpp gradQ gradRho

end SimultaneousFDivergenceGradient
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/InformationTheory/SimultaneousFDivergenceGradient.lean:42published source at 0e31a3cda412