production module

`AutoSamplingTheory.TechnicalLemmas.Measure.L2Expectation`

5 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/L2Expectation.lean.

Imports

Mathlib.Analysis.InnerProductSpace.LinearMap externalMathlib.MeasureTheory.Function.L2Space externalMathlib.MeasureTheory.Function.LpSpace.Indicator external

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.L2GeneratorIdentitiesTests.L2Expectation

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Measure.L2Expectation.one Partial Not mapped

- The constant-one element of `L²(pi)` for a finite measure.

noncomputable def one
    (pi : Measure α) [IsFiniteMeasure pi] : Lp ℝ 2 pi :=
  Lp.const 2 pi (1 : ℝ)

/-- Expectation on `L²(pi)` as the continuous linear functional
`f ↦ <1,f>_{L²(pi)}`. -/

AutoSamplingTheory/TechnicalLemmas/Measure/L2Expectation.lean:32published source at 0e31a3cda412

def AutoSamplingTheory.TechnicalLemmas.Measure.L2Expectation.expectation Partial Not mapped

- Expectation on `L²(pi)` as the continuous linear functional `f ↦ <1,f>_{L²(pi)}`.

noncomputable def expectation
    (pi : Measure α) [IsFiniteMeasure pi] : Lp ℝ 2 pi →L[ℝ] ℝ :=
  innerSL ℝ (one pi)

@[simp]

AutoSamplingTheory/TechnicalLemmas/Measure/L2Expectation.lean:38published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.L2Expectation.expectation_apply_eq_inner Partial Not mapped

No declaration docstring.

theorem expectation_apply_eq_inner
    (pi : Measure α) [IsFiniteMeasure pi]
    (f : Lp ℝ 2 pi) :
    expectation pi f = inner ℝ (one pi) f := by
  rfl

/-- The `L²(pi)` expectation functional is exactly the Bochner integral of the
chosen `Lp` representative.  The equality is representative-safe because both
sides are insensitive to `pi`-a.e. changes. -/

AutoSamplingTheory/TechnicalLemmas/Measure/L2Expectation.lean:43published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.L2Expectation.expectation_apply_eq_integral Partial Not mapped

- The `L²(pi)` expectation functional is exactly the Bochner integral of the chosen `Lp` representative. The equality is representative-safe because both sides are insensitive to `pi`-a.e. changes.

theorem expectation_apply_eq_integral
    (pi : Measure α) [IsFiniteMeasure pi]
    (f : Lp ℝ 2 pi) :
    expectation pi f = ∫ x, f x ∂pi := by
  rw [expectation_apply_eq_inner, MeasureTheory.L2.inner_def]
  apply integral_congr_ae
  filter_upwards
      [Lp.coeFn_const (α := α) (μ := pi) (p := (2 : ℝ≥0∞)) (c := (1 : ℝ))]
      with x hx
  change inner ℝ (one pi x) (f x) = f x
  rw [show one pi x = (1 : ℝ) by simpa [one] using hx]
  simp

/-- Source-facing integral form of the constant-one `L²` pairing. -/

AutoSamplingTheory/TechnicalLemmas/Measure/L2Expectation.lean:52published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.L2Expectation.inner_one_eq_integral Partial Not mapped

- Source-facing integral form of the constant-one `L²` pairing.

theorem inner_one_eq_integral
    (pi : Measure α) [IsFiniteMeasure pi]
    (f : Lp ℝ 2 pi) :
    inner ℝ (one pi) f = ∫ x, f x ∂pi := by
  simpa [expectation_apply_eq_inner] using expectation_apply_eq_integral pi f

end

end L2Expectation
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/L2Expectation.lean:66published source at 0e31a3cda412