test module

`Tests.GradientAECongruence`

0 named declarations scanned from Tests/GradientAECongruence.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientAECongruence

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

Tests/GradientAECongruence.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientAECongruence

open AutoSamplingTheory.TechnicalLemmas.Analysis

#check GradientAECongruence.not_gradient_ae_congr_for_arbitrary_measure
#print axioms GradientAECongruence.not_gradient_ae_congr_for_arbitrary_measure

example :
    ¬ ∀ (μ : MeasureTheory.Measure ℝ) (f g : ℝ → ℝ),
      f =ᵐ[μ] g → ∀ᵐ x ∂μ, gradient f x = gradient g x :=
  GradientAECongruence.not_gradient_ae_congr_for_arbitrary_measure