production module

`AutoSamplingTheory.TechnicalLemmas.InformationTheory.FisherTransport`

3 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/InformationTheory/FisherTransport.lean.

Imports

Mathlib.Tactic external

Imported by

AutoSamplingTheory.TechnicalLemmas.InformationTheoryAutoSamplingTheory.TechnicalLemmas.InformationTheory.GeodesicFisherTransportTests.SampleWikiExampleCases

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.InformationTheory.FisherTransport.sq_div_le_fisher_of_sq_le_mul Partial Not mapped

- Divide a Fisher--transport inequality by a positive squared transport radius. This is the algebraic step used in Chewi Theorem 8.4.1 after Wasserstein geodesic convexity and Cauchy--Schwarz establish `kl^2 ≤ fi * R2`.

theorem sq_div_le_fisher_of_sq_le_mul
    {kl fi R2 : ℝ}
    (hR2 : 0 < R2)
    (hbridge : kl ^ 2 ≤ fi * R2) :
    kl ^ 2 / R2 ≤ fi := by
  rw [div_le_iff₀ hR2]
  exact hbridge

/-- Combine Fisher--transport control with the negative one-half factor from
heat-flow KL dissipation.

The conclusion is written as `-((kl^2 / R2) / 2)` to keep this lemma purely
order-algebraic; source-facing assembly may rewrite it as
`-kl^2 / (2 * R2)`. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/FisherTransport.lean:28published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.InformationTheory.FisherTransport.neg_half_fisher_le_neg_half_sq_div Partial Not mapped

- Combine Fisher--transport control with the negative one-half factor from heat-flow KL dissipation. The conclusion is written as `-((kl^2 / R2) / 2)` to keep this lemma purely order-algebraic; source-facing assembly may rewrite it as `-kl^2 / (2 * R2)`.

theorem neg_half_fisher_le_neg_half_sq_div
    {kl fi R2 : ℝ}
    (hR2 : 0 < R2)
    (hbridge : kl ^ 2 ≤ fi * R2) :
    -(fi / 2) ≤ -((kl ^ 2 / R2) / 2) := by
  have hratio : kl ^ 2 / R2 ≤ fi :=
    sq_div_le_fisher_of_sq_le_mul hR2 hbridge
  linarith

/-- Source-shaped algebraic composition: if the KL derivative is exactly
`-FI/2`, then the Fisher--transport inequality gives the reciprocal-KL style
differential upper bound used in the proximal proof. -/

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

theorem AutoSamplingTheory.TechnicalLemmas.InformationTheory.FisherTransport.kl_derivative_upper_bound_of_fisher_transport Partial Not mapped

- Source-shaped algebraic composition: if the KL derivative is exactly `-FI/2`, then the Fisher--transport inequality gives the reciprocal-KL style differential upper bound used in the proximal proof.

theorem kl_derivative_upper_bound_of_fisher_transport
    {kl fi R2 kdot : ℝ}
    (hR2 : 0 < R2)
    (hbridge : kl ^ 2 ≤ fi * R2)
    (hdiss : kdot = -(fi / 2)) :
    kdot ≤ -((kl ^ 2 / R2) / 2) := by
  rw [hdiss]
  exact neg_half_fisher_le_neg_half_sq_div hR2 hbridge

end FisherTransport
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/InformationTheory/FisherTransport.lean:54published source at 0e31a3cda412