production module

`AutoSamplingTheory.TechnicalLemmas.Analysis.MeasurableGradient`

1 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Analysis/MeasurableGradient.lean.

Imports

Mathlib.Analysis.Calculus.FDeriv.Measurable externalMathlib.Analysis.Calculus.Gradient.Basic external

Imported by

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalFisherTransportPairingAutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalBrenierMapTests.MeasurableGradient

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.MeasurableGradient.measurable_gradient Partial Not mapped

- Mathlib's total Hilbert gradient of any real-valued function is measurable. At nondifferentiability points both the underlying total derivative and the gradient use their canonical default value.

theorem measurable_gradient (phi : E → ℝ) :
    Measurable (fun x : E => gradient phi x) := by
  rw [show (fun x : E => gradient phi x) =
      fun x => (InnerProductSpace.toDual ℝ E).symm (fderiv ℝ phi x) by
    funext x
    rfl]
  exact (InnerProductSpace.toDual ℝ E).symm.continuous.measurable.comp
    (measurable_fderiv ℝ phi)

end

end MeasurableGradient
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/MeasurableGradient.lean:32published source at 0e31a3cda412