ML.Core · Causalean Library

Hypothesis 3 core · 0 supporting The standalone ML spine carries two views of a learning method, connected later by Causalean.ML.Core.Bridge: * the parametric view (Predictor): a parameter type Θ together with an admissible set and a prediction map Θ → ★ Predictor★ HypothesisClass★ FeatureMap

Hypothesis classes and parametrized predictors

The standalone ML spine carries two views of a learning method, connected later by Causalean.ML.Core.Bridge:

* the parametric view (Predictor): a parameter type Θ together with an admissible set and a prediction map Θ → X → Y. Optimization, convexity and regularization live here. * the extensional view (HypothesisClass): a set of measurable functions X → Y. Population-risk targets and best-in-class statements live here.

FeatureMap packages a feature transform X → (K → ℝ) so that linear-in-features regression (and hence series/sieve regression) is a single object.

structure Predictor reviewed

Causalean.ML

A parametrized family of predictors bundles an admissible set of parameter values together with a map sending each parameter to a prediction function from the covariates to the outcome.

Definition (Lean source)

parameters

Θ X Y :

Type*

fields

The admissible parameter set (e.g. a norm ball, or all of `Θ`).

paramSet :

Set Θ

The prediction map: a parameter yields a function `X → Y`.

predict :

Θ → X → Y

Causalean.ML.Predictor · Causalean/ML/Core/Hypothesis.lean:27

structure HypothesisClass reviewed

Causalean.ML

A hypothesis class packaged extensionally as a set of admissible prediction functions from the covariates to the outcome, subject to the requirement that every function admitted to the class is measurable.

Definition (Lean source)

parameters

X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

fields

The set of admissible prediction functions.

carrier :

Set (X → Y)

Every admissible function is measurable.

measurable :

∀ ⦃h : X → Y⦄

if

h ∈ carrier

then

Measurable h

Causalean.ML.HypothesisClass · Causalean/ML/Core/Hypothesis.lean:36

structure FeatureMap reviewed

Causalean.ML

A finite feature map bundles a transform sending each input to its vector of K feature values. Linear-in-features predictors use x ↦ ⟪β, φ x⟫; the identity feature map recovers ordinary linear regression, and other choices of the transform recover polynomial, spline, or Fourier (sieve) regression.

Definition (Lean source)

parameters

X :

Type*

K :

Type*

Fintype K

fields

The feature transform sending an input to its vector of feature values.

φ :

X → (K → ℝ)

Causalean.ML.FeatureMap · Causalean/ML/Core/Hypothesis.lean:45

Risk 7 core · 0 supporting Risk criteria for the ML spine, in both the parametric and extensional views. ★ Loss★ empiricalRisk★ populationRisk

Empirical and population risk

Risk criteria for the ML spine, in both the parametric and extensional views. Loss is a pointwise prediction-label loss, empiricalRisk and empiricalRiskP are nonempty finite-sample averages, populationRisk and populationRiskP are Bochner-integral population criteria, and iidEmpiricalRisk expresses empirical risk through Stat.IIDSample.sampleMean. The separate predicate HasFinitePopulationRisk records when the population integral has the usual finite expected-loss interpretation.

abbrev Loss reviewed

Causalean.ML

For a label space, a pointwise loss is a real-valued function that compares a predicted label with an observed label.

Definition (Lean source)

parameters

Y :

Type*

def

Loss Y :

Type u_1

given by

Y → Y → ℝ

Causalean.ML.Loss · Causalean/ML/Core/Risk.lean:25

def empiricalRisk reviewed

Causalean.ML

For a nonempty finite sample index set, an input space, a label space, a pointwise loss, a sample of input--label pairs, and a prediction rule, the empirical risk is the average, over all sample indices, of the loss comparing the rule's prediction at that observation's input with that observation's label.

Definition (Lean source)

parameters

ι X Y :

Type*

Fintype ι

Nonempty ι

loss :

Loss Y

S :

ι → X × Y

h :

X → Y

def

empiricalRisk loss S h :

ℝ

given by

(Fintype.card ι : ℝ)⁻¹ * ∑ i, loss (h (S i).1) (S i).2

Causalean.ML.empiricalRisk · Causalean/ML/Core/Risk.lean:28 · uses Loss

def empiricalRiskP reviewed

Causalean.ML

For a nonempty finite sample index set, a parameter space, an input space, a label space, a parametric predictor, a pointwise loss, a sample of input--label pairs, and a parameter value, the parametric empirical risk is the empirical average loss of the prediction rule selected by that parameter value.

Definition (Lean source)

parameters

ι Θ X Y :

Type*

Fintype ι

Nonempty ι

M :

Predictor Θ X Y

loss :

Loss Y

S :

ι → X × Y

θ :

Θ

def

empiricalRiskP M loss S θ :

ℝ

given by

empiricalRisk loss S (M.predict θ)

Causalean.ML.empiricalRiskP · Causalean/ML/Core/Risk.lean:33 · uses Loss , Predictor

def populationRisk reviewed

Causalean.ML

For a measurable input space, a measurable label space, a pointwise loss, a joint input--label measure, and a prediction rule, the population risk is the integral under that joint measure of the loss comparing the rule's prediction at the input with the observed label.

Definition (Lean source)

parameters

X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

loss :

Loss Y

P :

Measure (X × Y)

h :

X → Y

def

populationRisk loss P h :

ℝ

given by

∫ z, loss (h z.1) z.2 ∂P

Causalean.ML.populationRisk · Causalean/ML/Core/Risk.lean:38 · uses Loss

def populationRiskP reviewed

Causalean.ML

For a parameter space, a measurable input space, a measurable label space, a parametric predictor, a pointwise loss, a joint input--label measure, and a parameter value, the parametric population risk is the population risk of the prediction rule selected by that parameter value.

Definition (Lean source)

parameters

Θ X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

M :

Predictor Θ X Y

loss :

Loss Y

P :

Measure (X × Y)

θ :

Θ

def

populationRiskP M loss P θ :

ℝ

given by

populationRisk loss P (M.predict θ)

Causalean.ML.populationRiskP · Causalean/ML/Core/Risk.lean:45 · uses Loss , Predictor

def iidEmpiricalRisk reviewed

Causalean.ML

For a measurable sample space, an input space and a label space equipped jointly with a measurable structure, an experiment measure, a joint input--label measure, an independent and identically distributed sample with those measures, a pointwise loss, a prediction rule, and a sample size, the i.i.d. empirical risk is the random sample average of the loss comparing the rule's prediction with the observed label over the first $n$ sample observations.

Definition (Lean source)

parameters

Ω X Y :

Type*

MeasurableSpace Ω

MeasurableSpace (X × Y)

Measure Ω

Measure (X × Y)

S :

IIDSample Ω (X × Y) μ P

loss :

Loss Y

h :

X → Y

n :

ℕ

def

iidEmpiricalRisk S loss h n :

Ω → ℝ

given by

S.sampleMean (fun z => loss (h z.1) z.2) n

Causalean.ML.iidEmpiricalRisk · Causalean/ML/Core/Risk.lean:50 · uses Loss , IIDSample

def HasFinitePopulationRisk reviewed

Causalean.ML

For a measurable input space, a measurable label space, a pointwise loss, a joint input--label measure, and a prediction rule, the finite-population-risk condition holds exactly when the loss comparing the rule's prediction with the observed label is integrable under the joint measure.

Definition (Lean source)

parameters

X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

loss :

Loss Y

P :

Measure (X × Y)

h :

X → Y

def

HasFinitePopulationRisk loss P h :

Prop

given by

Integrable (fun z => loss (h z.1) z.2) P

Causalean.ML.HasFinitePopulationRisk · Causalean/ML/Core/Risk.lean:58 · uses Loss

ERM 5 core · 0 supporting Minimizer predicates for the ML spine, stated candidate-wise via Mathlib's IsMinOn (or a comparison + ε form), never via sInf/argmin — this avoids pathological real-infimum defaults on empty or unbounded sets, matching t ★ IsERMP★ IsApproxERMP★ RegularizedERM★ IsERM★ IsPopulationRiskMinimizer

Empirical-risk-minimizer predicates

Minimizer predicates for the ML spine, stated candidate-wise via Mathlib's IsMinOn (or a comparison + ε form), never via sInf/argmin — this avoids pathological real-infimum defaults on empty or unbounded sets, matching the existing Estimation.OrthogonalLearning.PluginERM idiom.

The file provides exact, approximate, and regularized parametric ERM predicates (IsERMP, IsApproxERMP, RegularizedERM), plus extensional empirical and population minimizer predicates (IsERM, IsPopulationRiskMinimizer) over a HypothesisClass. The parametric and extensional views are connected in Causalean.ML.Core.Bridge.

structure IsERMP reviewed

Causalean.ML

θhat exactly minimizes a parametric objective over the admissible set.

Definition (Lean source)

parameters

Θ :

Type*

objective :

Θ → ℝ

Θset :

Set Θ

θhat :

Θ

assumes

mem :

θhat ∈ Θset

The minimizer is admissible.

isMin :

IsMinOn objective Θset θhat

It attains the minimum of the objective over Θset.

Causalean.ML.IsERMP · Causalean/ML/Core/ERM.lean:27

structure IsApproxERMP reviewed

Causalean.ML

θhat minimizes a parametric objective up to slack ε ≥ 0.

Definition (Lean source)

parameters

Θ :

Type*

objective :

Θ → ℝ

Θset :

Set Θ

θhat :

Θ

ε :

ℝ

assumes

ε_nonneg :

0 ≤ ε

The slack is nonnegative.

mem :

θhat ∈ Θset

The candidate is admissible.

approx_min :

∀ θ ∈ Θset, objective θhat ≤ objective θ + ε

Its objective is within ε of every competitor's.

Causalean.ML.IsApproxERMP · Causalean/ML/Core/ERM.lean:34

structure RegularizedERM reviewed

Causalean.ML

θhat minimizes a penalized objective objective θ + lam · penalty θ with a nonnegative regularization weight lam.

Definition (Lean source)

parameters

Θ :

Type*

objective :

Θ → ℝ

penalty :

Θ → ℝ

lam :

ℝ

Θset :

Set Θ

θhat :

Θ

assumes

lam_nonneg :

0 ≤ lam

The regularization weight is nonnegative.

mem :

θhat ∈ Θset

The minimizer is admissible.

isMin :

IsMinOn (fun θ => objective θ + lam * penalty θ) Θset θhat

It minimizes the penalized objective over Θset.

Causalean.ML.RegularizedERM · Causalean/ML/Core/ERM.lean:44

structure IsERM reviewed

Causalean.ML

An empirical-risk minimizer is an admissible prediction rule whose finite-sample risk criterion is no larger than that of any other admissible rule. The criterion is the inverse-cardinality-scaled loss sum over a nonempty finite sample.

Definition (Lean source)

parameters

ι X Y :

Type*

Fintype ι

Nonempty ι

MeasurableSpace X

MeasurableSpace Y

H :

HypothesisClass X Y

loss :

Loss Y

S :

ι → X × Y

hhat :

X → Y

assumes

mem :

hhat ∈ H.carrier

The minimizer belongs to the class.

isMin :

IsMinOn (fun h => empiricalRisk loss S h) H.carrier hhat

It minimizes empirical risk over the class.

Causalean.ML.IsERM · Causalean/ML/Core/ERM.lean:55 · uses HypothesisClass , Loss

structure IsPopulationRiskMinimizer reviewed

Causalean.ML

A population-risk minimizer bundles the claim that a prediction rule belongs to the hypothesis class, that it has finite expected loss under the population measure, that every other rule admissible in the class also has finite expected loss, and that its population risk is no larger than that of any other rule in the class.

Definition (Lean source)

parameters

X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

H :

HypothesisClass X Y

loss :

Loss Y

P :

Measure (X × Y)

hstar :

X → Y

assumes

mem :

hstar ∈ H.carrier

The minimizer belongs to the class.

finite_self :

HasFinitePopulationRisk loss P hstar

The minimizer has finite expected loss.

finite_competitor :

∀ h ∈ H.carrier, HasFinitePopulationRisk loss P h

Every admissible competitor has finite expected loss.

isMin :

IsMinOn (fun h => populationRisk loss P h) H.carrier hstar

It minimizes population risk over the class.

Causalean.ML.IsPopulationRiskMinimizer · Causalean/ML/Core/ERM.lean:67 · uses HypothesisClass , Loss

Losses 6 core · 7 supporting This file collects the elementary pointwise loss functions used throughout Causalean.ML: the squared loss for regression, and the sigmoid / softplus / score-space logistic loss for binary classification. ★ squaredLoss★ logisticScoreLoss★ bool01_true

Loss functions for the standalone ML module

This file collects the elementary pointwise loss functions used throughout Causalean.ML: the squared loss for regression, and the sigmoid / softplus / score-space logistic loss for binary classification. Everything here is causal-free real analysis; no probability or causal layer is imported.

def squaredLoss reviewed

Causalean.ML

For a real-valued prediction $\hat y$ and a real-valued observed outcome $y$ , the squared loss is $(y-\hat y)^2$ .

Definition (Lean source)

parameters

ŷ y :

ℝ

def

squaredLoss ŷ y :

ℝ

given by

(y - ŷ) ^ 2

Causalean.ML.squaredLoss · Causalean/ML/Core/Losses.lean:19

def bool01 reviewed

Causalean.ML

For a binary label, the zero--one real-valued encoding of that label is one when the label is true and zero when it is false.

Definition (Lean source)

parameters

b :

Bool

def

bool01 b :

ℝ

given by

if b then 1 else 0

Causalean.ML.bool01 · Causalean/ML/Core/Losses.lean:24

def sigmoid reviewed

Causalean.ML

For a real-valued score $t$ , the logistic sigmoid is $(1+\exp(-t))^{-1}$ .

Definition (Lean source)

parameters

t :

ℝ

def

sigmoid t :

ℝ

given by

(1 + exp (-t))⁻¹

Causalean.ML.sigmoid · Causalean/ML/Core/Losses.lean:29

def softplus reviewed

Causalean.ML

For a real-valued score $t$ , the softplus transformation is $\log(1+\exp t)$ .

Definition (Lean source)

parameters

t :

ℝ

def

softplus t :

ℝ

given by

log (1 + exp t)

Causalean.ML.softplus · Causalean/ML/Core/Losses.lean:34

def logisticScoreLoss reviewed

Causalean.ML

For a binary outcome $y$ and a real-valued prediction score $t$ , the logistic score loss is $\log(1+\exp t)-y_0t$ , where $y_0$ is one when $y$ is true and zero when $y$ is false.

Definition (Lean source)

parameters

y :

Bool

t :

ℝ

def

logisticScoreLoss y t :

ℝ

given by

softplus t - bool01 y * t

Causalean.ML.logisticScoreLoss · Causalean/ML/Core/Losses.lean:39

lemma bool01_true reviewed

Causalean.ML

A true Boolean label is encoded as the real number one.

Formal statement

conclusion

bool01 true = 1

Proof (Lean source)

@[simp] lemma bool01_true : bool01 true = 1 := rfl

Causalean.ML.bool01_true · Causalean/ML/Core/Losses.lean:45 · uses bool01

7 supporting declarations (lemmas, instances)

bool01_false lemma — A false Boolean label is encoded as zero.

conclusion

bool01 false = 0

Proof (Lean source)

@[simp] lemma bool01_false : bool01 false = 0 := rfl

Causalean.ML.bool01_false · Causalean/ML/Core/Losses.lean:48
bool01_nonneg lemma — The zero-one encoding of a Boolean label is always nonnegative.

hypotheses

b :

Bool

conclusion

0 ≤ bool01 b

Proof (Lean source)

lemma bool01_nonneg (b : Bool) : 0 ≤ bool01 b := by cases b <;> simp [bool01]

Causalean.ML.bool01_nonneg · Causalean/ML/Core/Losses.lean:51
bool01_le_one lemma — The zero-one encoding of a Boolean label is always at most one.

hypotheses

b :

Bool

conclusion

bool01 b ≤ 1

Proof (Lean source)

lemma bool01_le_one (b : Bool) : bool01 b ≤ 1 := by cases b <;> simp [bool01]

Causalean.ML.bool01_le_one · Causalean/ML/Core/Losses.lean:55
squaredLoss_nonneg lemma — Squared loss is always nonnegative.

hypotheses

ŷ y :

ℝ

conclusion

0 ≤ squaredLoss ŷ y

Proof (Lean source)

lemma squaredLoss_nonneg (ŷ y : ℝ) : 0 ≤ squaredLoss ŷ y := sq_nonneg _

Causalean.ML.squaredLoss_nonneg · Causalean/ML/Core/Losses.lean:59
sigmoid_pos lemma — The logistic sigmoid is strictly positive at every score.

hypotheses

t :

ℝ

conclusion

0 < sigmoid t

Proof (Lean source)

lemma sigmoid_pos (t : ℝ) : 0 < sigmoid t := by have : 0 < 1 + exp (-t) := by positivity exact inv_pos.mpr this

Causalean.ML.sigmoid_pos · Causalean/ML/Core/Losses.lean:62
sigmoid_lt_one lemma — The logistic sigmoid is strictly below one at every score.

hypotheses

t :

ℝ

conclusion

sigmoid t < 1

Proof (Lean source)

lemma sigmoid_lt_one (t : ℝ) : sigmoid t < 1 := by have hpos : (0 : ℝ) < exp (-t) := Real.exp_pos _ have h1 : (1 : ℝ) < 1 + exp (-t) := by linarith calc sigmoid t = (1 + exp (-t))⁻¹ := rfl _ < 1 := by rw [inv_lt_one_iff₀] right; exact h1

Causalean.ML.sigmoid_lt_one · Causalean/ML/Core/Losses.lean:67
softplus_pos lemma — Softplus is strictly positive at every score.

hypotheses

t :

ℝ

conclusion

0 < softplus t

Proof (Lean source)

lemma softplus_pos (t : ℝ) : 0 < softplus t := by have hpos : (0 : ℝ) < exp t := Real.exp_pos _ have h1 : (1 : ℝ) < 1 + exp t := by linarith exact Real.log_pos h1

Causalean.ML.softplus_pos · Causalean/ML/Core/Losses.lean:76

Bridge 2 core · 1 supporting The image of a Predictor under its prediction map is a HypothesisClass, and a *parametric* minimizer pushes forward to an *extensional* minimizer over that image class. ★ populationTarget_pushforward

Bridge between the parametric and extensional views

The image of a Predictor under its prediction map is a HypothesisClass, and a parametric minimizer pushes forward to an extensional minimizer over that image class. These two lemmas are the only glue between the two views of a method: properties stated in parameter space (convexity, regularization, optimization) transfer to the function-class statements (best-in-class, population target).

def imageClass reviewed

Causalean.ML

Given an arbitrary parameter space, an arbitrary covariate space equipped with a σ-algebra, an arbitrary outcome space equipped with a σ-algebra, a parametric predictor together with its admissible parameter set and evidence that the prediction function is measurable for every admissible parameter, the realized hypothesis class consists exactly of the prediction functions obtained by letting the parameter range over that admissible set; its members are equipped with the stated measurability guarantee.

Definition (Lean source)

parameters

Θ X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

M :

Predictor Θ X Y

hmeas :

∀ θ ∈ M.paramSet, Measurable (M.predict θ)

def

imageClass M hmeas :

HypothesisClass X Y

given by

clause 1

carrier := (fun θ => M.predict θ) '' M.paramSet

clause 2

measurable := by rintro h ⟨θ, hθ, rfl⟩ exact hmeas θ hθ

Causalean.ML.imageClass · Causalean/ML/Core/Bridge.lean:22 · uses HypothesisClass , Predictor

theorem populationTarget_pushforward reviewed

Causalean.ML

Population-target pushforward. For a predictor M with loss loss and population law P, suppose every admissible parameter's prediction function is measurable, the parameter θhat is itself admissible, every admissible parameter attains finite population risk, and θhat minimizes the population risk over the admissible parameter set. Then the predictor M.predict θhat is a population-risk minimizer over the hypothesis class realized by M's image: a parametric population-risk minimizer pushes forward to an extensional minimizer over the realized function class.

Formal statement

hypotheses

Θ X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

M :

Predictor Θ X Y

loss :

Loss Y

P :

Measure (X × Y)

hmeas :

∀ θ ∈ M.paramSet, Measurable (M.predict θ)

θhat :

Θ

hmem :

θhat ∈ M.paramSet

hfinite :

∀ θ ∈ M.paramSet, HasFinitePopulationRisk loss P (M.predict θ)

h :

IsMinOn (fun θ => populationRiskP M loss P θ) M.paramSet θhat

conclusion

IsPopulationRiskMinimizer (imageClass M hmeas) loss P (M.predict θhat) where mem

Proof (Lean source)

theorem populationTarget_pushforward {Θ X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (M : Predictor Θ X Y) (loss : Loss Y) (P : Measure (X × Y)) (hmeas : ∀ θ ∈ M.paramSet, Measurable (M.predict θ)) {θhat : Θ} (hmem : θhat ∈ M.paramSet) (hfinite : ∀ θ ∈ M.paramSet, HasFinitePopulationRisk loss P (M.predict θ)) (h : IsMinOn (fun θ => populationRiskP M loss P θ) M.paramSet θhat) : IsPopulationRiskMinimizer (imageClass M hmeas) loss P (M.predict θhat) where mem := ⟨θhat, hmem, rfl⟩ finite_self := hfinite θhat hmem finite_competitor := by rintro g ⟨θ, hθ, rfl⟩ exact hfinite θ hθ isMin := by rw [isMinOn_iff] rintro g ⟨θ, hθ, rfl⟩ simpa [populationRiskP] using (isMinOn_iff.mp h) θ hθ

Causalean.ML.populationTarget_pushforward · Causalean/ML/Core/Bridge.lean:51 · uses HasFinitePopulationRisk , IsPopulationRiskMinimizer , Loss , Predictor , imageClass , populationRiskP

1 supporting declaration (lemmas, instances)

isERMP_to_extensional theorem — A parametric empirical-risk minimizer pushes forward to an extensional empirical-risk minimizer over the realized hypothesis class.

hypotheses

ι Θ X Y :

Type*
Fintype ι
Nonempty ι
MeasurableSpace X
MeasurableSpace Y

M :

Predictor Θ X Y

loss :

Loss Y

S :

ι → X × Y

hmeas :

∀ θ ∈ M.paramSet, Measurable (M.predict θ)

θhat :

Θ

h :

IsERMP (empiricalRiskP M loss S) M.paramSet θhat

conclusion

IsERM (imageClass M hmeas) loss S (M.predict θhat) where mem

Proof (Lean source)

theorem isERMP_to_extensional {ι Θ X Y : Type*} [Fintype ι] [Nonempty ι] [MeasurableSpace X] [MeasurableSpace Y] (M : Predictor Θ X Y) (loss : Loss Y) (S : ι → X × Y) (hmeas : ∀ θ ∈ M.paramSet, Measurable (M.predict θ)) {θhat : Θ} (h : IsERMP (empiricalRiskP M loss S) M.paramSet θhat) : IsERM (imageClass M hmeas) loss S (M.predict θhat) where mem := ⟨θhat, h.mem, rfl⟩ isMin := by rw [isMinOn_iff] rintro g ⟨θ, hθ, rfl⟩ simpa [empiricalRiskP] using (isMinOn_iff.mp h.isMin) θ hθ

Causalean.ML.isERMP_to_extensional · Causalean/ML/Core/Bridge.lean:37

Convex 2 core · 5 supporting Reusable convexity, existence, first-order-optimality and subgradient facts that the convex methods (logistic regression, lasso, generic convex ERM) instantiate. ★ exists_isMinOn_univ_of_coercive

Convex-analysis substrate for ERM

Reusable convexity, existence, first-order-optimality and subgradient facts that the convex methods (logistic regression, lasso, generic convex ERM) instantiate. This file is method-agnostic: it speaks only about an abstract objective on a real vector / inner-product / normed space.

theorem exists_isMinOn_univ_of_coercive reviewed

Causalean.ML

Existence via coercivity. On a proper normed real vector space, if the objective function is continuous and it tends to infinity along the cocompact filter, i.e. it is coercive — it grows without bound as the argument leaves every compact set, then a global minimizer of the objective over the whole space exists.

Formal statement

hypotheses

E :

Type u_1

E → ℝ

shared

hcont :

Continuous objective

hcoer :

Tendsto objective (cocompact E) atTop

conclusion

∃ a, IsMinOn objective univ a

Proof (Lean source)

theorem exists_isMinOn_univ_of_coercive {objective : E → ℝ} (hcont : Continuous objective) (hcoer : Tendsto objective (cocompact E) atTop) : ∃ a, IsMinOn objective univ a := by have _ : ProperSpace E := inferInstance obtain ⟨a, ha⟩ := hcont.exists_forall_le hcoer exact ⟨a, isMinOn_univ_iff.2 ha⟩

Causalean.ML.exists_isMinOn_univ_of_coercive · Causalean/ML/Core/Convex.lean:91

def SubgradientAt reviewed

Causalean.ML

In a real inner-product space, for a real-valued function, a subset of the space, a vector, and a point, the statement that the vector is a subgradient of the function at the point relative to the subset requires the point to belong to the subset and for every point $y$ in that subset, $f(x)+\langle g,y-x\rangle\le f(y)$ .

Definition (Lean source)

parameters

E :

Type u_1

shared

f :

E → ℝ

s :

Set E

g x :

E

def

SubgradientAt f s g x :

Prop

given by

clause 1

x ∈ s

clause 2

y ∈ s :

f x + inner ℝ g (y - x) ≤ f y

Causalean.ML.SubgradientAt · Causalean/ML/Core/Convex.lean:121

5 supporting declarations (lemmas, instances)

empiricalRiskP_convexOn_of_loss_convex theorem — If every per-sample parameter loss is convex on Θset, so is the empirical risk of the predictor.

hypotheses

ι :

Type u_1
shared

Θ :

Type u_2
shared

X :

Type u_3
shared

Y :

Type u_4
shared

M :

Predictor Θ X Y

loss :

Loss Y

S :

ι → X × Y

Θset :

Set Θ

hconv :

Convex ℝ Θset

hloss :

∀ i, ConvexOn ℝ Θset (fun θ => loss (M.predict θ (S i).1) (S i).2)

conclusion

ConvexOn ℝ Θset (empiricalRiskP M loss S)

Proof (Lean source)

theorem empiricalRiskP_convexOn_of_loss_convex (M : Predictor Θ X Y) (loss : Loss Y) (S : ι → X × Y) (Θset : Set Θ) (hconv : Convex ℝ Θset) (hloss : ∀ i, ConvexOn ℝ Θset (fun θ => loss (M.predict θ (S i).1) (S i).2)) : ConvexOn ℝ Θset (empiricalRiskP M loss S) := by unfold empiricalRiskP empiricalRisk have hsum : ConvexOn ℝ Θset (fun θ => ∑ i, loss (M.predict θ (S i).1) (S i).2) := by classical have hfin : ∀ t : Finset ι, ConvexOn ℝ Θset (fun θ => t.sum (fun i => loss (M.predict θ (S i).1) (S i).2)) := by intro t induction t using Finset.induction_on with | empty => simpa using (convexOn_const (𝕜 := ℝ) (E := Θ) (β := ℝ) (s := Θset) (0 : ℝ) hconv) | insert i t hi ht => have hadd := (hloss i).add ht have hfun : ((fun θ => loss (M.predict θ (S i).1) (S i).2) + fun θ => t.sum (fun i => loss (M.predict θ (S i).1) (S i).2)) = fun θ => (insert i t).sum (fun i => loss (M.predict θ (S i).1) (S i).2) := by funext θ simp [Finset.sum_insert hi] rwa [hfun] at hadd simpa using hfin univ simpa [smul_eq_mul] using hsum.smul (inv_nonneg.mpr (Nat.cast_nonneg (card ι)))

Causalean.ML.empiricalRiskP_convexOn_of_loss_convex · Causalean/ML/Core/Convex.lean:27
convexOn_comp_inner theorem — A convex scalar function precomposed with the linear score θ ↦ ⟪θ, x⟫ is convex. This is the workhorse turning convexity of a margin loss into convexity of the parameter objective.

hypotheses

E :

Type u_1
shared

φ :

ℝ → ℝ

hφ :

ConvexOn ℝ univ φ

x :

E

conclusion

ConvexOn ℝ univ (fun θ : E => φ (inner ℝ θ x))

Proof (Lean source)

theorem convexOn_comp_inner {φ : ℝ → ℝ} (hφ : ConvexOn ℝ univ φ) (x : E) : ConvexOn ℝ univ (fun θ : E => φ (inner ℝ θ x)) := by simpa [Function.comp_def, innerSL_apply_apply, real_inner_comm] using hφ.comp_linearMap ((innerSL ℝ x).toLinearMap)

Causalean.ML.convexOn_comp_inner · Causalean/ML/Core/Convex.lean:64
exists_isMinOn_of_isCompact theorem — Existence of a minimizer on a nonempty compact set (Weierstrass).

hypotheses

Θ :

Type u_1
Θ → ℝ
Set Θ
shared

hne :

Θset.Nonempty

hcompact :

IsCompact Θset

hcont :

ContinuousOn objective Θset

conclusion

∃ θhat ∈ Θset, IsMinOn objective Θset θhat

Proof (Lean source)

theorem exists_isMinOn_of_isCompact {objective : Θ → ℝ} {Θset : Set Θ} (hne : Θset.Nonempty) (hcompact : IsCompact Θset) (hcont : ContinuousOn objective Θset) : ∃ θhat ∈ Θset, IsMinOn objective Θset θhat := by exact hcompact.exists_isMinOn hne hcont

Causalean.ML.exists_isMinOn_of_isCompact · Causalean/ML/Core/Convex.lean:78
fderiv_eq_zero_of_isMinOn_univ theorem — First-order optimality on the whole space: at an unconstrained minimizer the Fréchet derivative vanishes.

hypotheses

E :

Type u_1
E → ℝ
E →L[ℝ] ℝ
E
shared

hmin :

IsMinOn f univ a

hderiv :

HasFDerivAt f f' a

conclusion

f' = 0

Proof (Lean source)

theorem fderiv_eq_zero_of_isMinOn_univ {f : E → ℝ} {f' : E →L[ℝ] ℝ} {a : E} (hmin : IsMinOn f univ a) (hderiv : HasFDerivAt f f' a) : f' = 0 := by exact (hmin.isLocalMin univ_mem).hasFDerivAt_eq_zero hderiv

Causalean.ML.fderiv_eq_zero_of_isMinOn_univ · Causalean/ML/Core/Convex.lean:109
subgradientAt_zero_iff_isMinOn theorem — Fermat's rule, subgradient form: 0 is a subgradient at x over s iff x minimizes f over s.

hypotheses

E :

Type u_1
E → ℝ
Set E
E
shared

hx :

x ∈ s

conclusion

SubgradientAt f s 0 x ↔ IsMinOn f s x

Proof (Lean source)

theorem subgradientAt_zero_iff_isMinOn {f : E → ℝ} {s : Set E} {x : E} (hx : x ∈ s) : SubgradientAt f s 0 x ↔ IsMinOn f s x := by constructor · intro h exact isMinOn_iff.2 fun y hy => by have := h.2 y hy simpa [SubgradientAt, inner_zero_left] using this · intro hmin refine ⟨hx, ?_⟩ intro y hy simpa [SubgradientAt, inner_zero_left] using (isMinOn_iff.1 hmin y hy)

Causalean.ML.subgradientAt_zero_iff_isMinOn · Causalean/ML/Core/Convex.lean:127

PopulationTarget 2 core · 2 supporting This file collects reusable statements about what a population-risk minimizer recovers. ★ IsL2Projection★ square_loss_population_target_of_isL2Projection

Population-risk targets

This file collects reusable statements about what a population-risk minimizer recovers. populationRisk_eq_of_both_minimizers shows that any two minimizers attain the same risk, while populationRisk_minimizer_eq_target turns a unique target minimizer into equality of functions. For squared loss, IsL2Projection records the residual-orthogonality property of an L² projection, and square_loss_population_target_of_isL2Projection proves that such a projection minimizes squared population risk. The conditional-expectation bridge is isolated in ML/CausalApplication/RegressionBridge.lean, so this layer stays self-contained and causal-free.

def IsL2Projection reviewed

Causalean.ML

For a measurable covariate space, a joint measure of a covariate and a real-valued response, and a candidate regression function, the L²-projection condition holds precisely when, for every measurable real-valued function of the covariate whose product with the residual is integrable, the integral of that product is zero.

Definition (Lean source)

parameters

X :

Type u_1

shared

P :

Measure (X × ℝ)

m :

X → ℝ

g :

X → ℝ

Measurable g

Integrable (fun z => (z.2 - m z.1) * g z.1) P

def

IsL2Projection P m :

Prop

given by

∫ z, (z.2 - m z.1) * g z.1 ∂P = 0

Causalean.ML.IsL2Projection · Causalean/ML/Core/PopulationTarget.lean:47

theorem square_loss_population_target_of_isL2Projection reviewed

Causalean.ML

For a joint covariate–response law P and a competitor function h, if the residual of m is orthogonal to every function of the covariate, i.e. m is an L² projection onto functions of the covariate, m is measurable, the competitor h is measurable, m attains finite squared population risk, h attains finite squared population risk, and the cross term (Y − m(X))·(m(X) − h(X)) is integrable, then the squared population risk of m is at most that of h: m minimizes squared population risk against any such competitor.

Formal statement

hypotheses

X :

Type u_1

Measure (X × ℝ)

X → ℝ

shared

hm :

IsL2Projection P m

h :

X → ℝ

hm_meas :

Measurable m

hh_meas :

Measurable h

hint_m :

HasFinitePopulationRisk squaredLoss P m

hint_h :

HasFinitePopulationRisk squaredLoss P h

hcross :

Integrable (fun z => (z.2 - m z.1) * (m z.1 - h z.1)) P

conclusion

populationRisk squaredLoss P m ≤ populationRisk squaredLoss P h

Proof (Lean source)

theorem square_loss_population_target_of_isL2Projection {P : Measure (X × ℝ)} {m : X → ℝ} (hm : IsL2Projection P m) (h : X → ℝ) (hm_meas : Measurable m) (hh_meas : Measurable h) (hint_m : HasFinitePopulationRisk squaredLoss P m) (hint_h : HasFinitePopulationRisk squaredLoss P h) (hcross : Integrable (fun z => (z.2 - m z.1) * (m z.1 - h z.1)) P) : populationRisk squaredLoss P m ≤ populationRisk squaredLoss P h := by have hint_m' : Integrable (fun z : X × ℝ => (z.2 - m z.1) ^ 2) P := by simpa [HasFinitePopulationRisk, squaredLoss] using hint_m have hint_h' : Integrable (fun z : X × ℝ => (z.2 - h z.1) ^ 2) P := by simpa [HasFinitePopulationRisk, squaredLoss] using hint_h have hdiff : Integrable (fun z : X × ℝ => (z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) P := hint_h'.sub hint_m' have hsq_int : Integrable (fun z : X × ℝ => (m z.1 - h z.1) ^ 2) P := by have htmp : Integrable (fun z : X × ℝ => ((z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) - 2 * ((z.2 - m z.1) * (m z.1 - h z.1))) P := hdiff.sub (hcross.const_mul 2) convert htmp using 1 funext z ring have horth : ∫ z, (z.2 - m z.1) * (m z.1 - h z.1) ∂P = 0 := hm (fun x => m x - h x) (hm_meas.sub hh_meas) hcross have hdiff_nonneg : 0 ≤ ∫ z, ((z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) ∂P := by calc 0 ≤ ∫ z, (m z.1 - h z.1) ^ 2 ∂P := by exact integral_nonneg (fun z => sq_nonneg _) _ = 2 * ∫ z, (z.2 - m z.1) * (m z.1 - h z.1) ∂P + ∫ z, (m z.1 - h z.1) ^ 2 ∂P := by simp [horth] _ = ∫ z, 2 * ((z.2 - m z.1) * (m z.1 - h z.1)) + (m z.1 - h z.1) ^ 2 ∂P := by rw [integral_add] · rw [integral_const_mul] · exact hcross.const_mul 2 · exact hsq_int _ = ∫ z, ((z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) ∂P := by apply integral_congr_ae filter_upwards with z ring have hle : ∫ z, (z.2 - m z.1) ^ 2 ∂P ≤ ∫ z, (z.2 - h z.1) ^ 2 ∂P := by have hnonneg_sub : 0 ≤ ∫ z, (z.2 - h z.1) ^ 2 ∂P - ∫ z, (z.2 - m z.1) ^ 2 ∂P := by rw [← integral_sub hint_h' hint_m'] exact hdiff_nonneg linarith simpa [populationRisk, squaredLoss] using hle

Causalean.ML.square_loss_population_target_of_isL2Projection · Causalean/ML/Core/PopulationTarget.lean:63 · uses HasFinitePopulationRisk , IsL2Projection , populationRisk , squaredLoss

2 supporting declarations (lemmas, instances)

populationRisk_eq_of_both_minimizers theorem — Any two population-risk minimizers over the same class attain the same risk.

hypotheses

X :

Type u_1
shared

Y :

Type u_2
HypothesisClass X Y
Loss Y
Measure (X × Y)
X → Y
shared

H1 :

IsPopulationRiskMinimizer H loss P h₁

H2 :

IsPopulationRiskMinimizer H loss P h₂

conclusion

populationRisk loss P h₁ = populationRisk loss P h₂

Proof (Lean source)

theorem populationRisk_eq_of_both_minimizers {H : HypothesisClass X Y} {loss : Loss Y} {P : Measure (X × Y)} {h₁ h₂ : X → Y} (H1 : IsPopulationRiskMinimizer H loss P h₁) (H2 : IsPopulationRiskMinimizer H loss P h₂) : populationRisk loss P h₁ = populationRisk loss P h₂ := le_antisymm ((isMinOn_iff.mp H1.isMin) h₂ H2.mem) ((isMinOn_iff.mp H2.isMin) h₁ H1.mem)

Causalean.ML.populationRisk_eq_of_both_minimizers · Causalean/ML/Core/PopulationTarget.lean:28
populationRisk_minimizer_eq_target theorem — If a target is known to be the unique population-risk minimizer, every population-risk minimizer equals it.

hypotheses

X :

Type u_1
shared

Y :

Type u_2
HypothesisClass X Y
Loss Y
Measure (X × Y)
X → Y
shared

hStar :

IsPopulationRiskMinimizer H loss P hstar

hTarget :

IsPopulationRiskMinimizer H loss P target

hUnique :

∀ h₁ h₂
if
IsPopulationRiskMinimizer H loss P h₁
and
IsPopulationRiskMinimizer H loss P h₂
then
h₁ = h₂

conclusion

hstar = target

Proof (Lean source)

theorem populationRisk_minimizer_eq_target {H : HypothesisClass X Y} {loss : Loss Y} {P : Measure (X × Y)} {target hstar : X → Y} (hStar : IsPopulationRiskMinimizer H loss P hstar) (hTarget : IsPopulationRiskMinimizer H loss P target) (hUnique : ∀ h₁ h₂, IsPopulationRiskMinimizer H loss P h₁ → IsPopulationRiskMinimizer H loss P h₂ → h₁ = h₂) : hstar = target := hUnique hstar target hStar hTarget

Causalean.ML.populationRisk_minimizer_eq_target · Causalean/ML/Core/PopulationTarget.lean:36

Rate 2 core · 2 supporting The causal-free common currency between the method folders (which prove per-method L²-estimation rates) and ML/CausalApplication (which assembles them to discharge DML's nuisance-rate conditions). ★ isLittleOp_mul_quarter★ AchievesL2Rate

Learning-rate abstraction and rate algebra

The causal-free common currency between the method folders (which prove per-method L²-estimation rates) and ML/CausalApplication (which assembles them to discharge DML's nuisance-rate conditions).

* AchievesL2Rate ĥ h⋆ P rₙ μ — every L² seminorm of the estimation error is finite, and its real-number conversion is O_p(rₙ) under the experiment law. * generic probabilistic stochastic-order facts: an o_p(rₙ) with rₙ ≤ 1 is o_p(1); a product of two o_p(n^{-1/4}) is o_p(n^{-1/2}); and an O_p(n^{-1/2}) rate is o_p(n^{-1/4}) (turning a method's root-n IsBigOp into the o_p(n^{-1/4}) the DML side consumes).

theorem isLittleOp_mul_quarter reviewed

Causalean.ML

The n^{-1/4} product rule. If the sequence Xn is o_p(n^{-1/4}) and the sequence Yn is o_p(n^{-1/4}) under the probability law μ, then their pointwise product Xn·Yn is o_p(n^{-1/2}) — the DML product-rate condition from per-nuisance n^{-1/4} rates.

Formal statement

hypotheses

Ω :

Type u_1

Measure Ω

ℕ → Ω → ℝ

shared

hX :

IsLittleOp Xn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ

hY :

IsLittleOp Yn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ

conclusion

IsLittleOp (fun n ω => Xn n ω * Yn n ω) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ

Proof (Lean source)

theorem isLittleOp_mul_quarter (hX : IsLittleOp Xn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ) (hY : IsLittleOp Yn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ) : IsLittleOp (fun n ω => Xn n ω * Yn n ω) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ := by intro ε hε let δ : ℝ := Real.sqrt ε have hδpos : 0 < δ := Real.sqrt_pos.2 hε have hδsq : δ * δ = ε := by simpa [δ, pow_two] using Real.sq_sqrt (le_of_lt hε) let A : ℕ → Set Ω := fun n => {ω | δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) < |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) < |Yn n ω|} let C : ℕ → Set Ω := fun n => {ω | ε * (n : ℝ) ^ (-(1 / 2 : ℝ)) < |Xn n ω * Yn n ω|} have hAt : Tendsto (fun n => μ (A n)) atTop (𝓝 0) := by simpa [A, δ] using hX δ hδpos have hBt : Tendsto (fun n => μ (B n)) atTop (𝓝 0) := by simpa [B, δ] using hY δ hδpos have hsum : Tendsto (fun n => μ (A n) + μ (B n)) atTop (𝓝 0) := by simpa using hAt.add hBt refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hsum (Eventually.of_forall fun n => zero_le) ?_ filter_upwards [eventually_ge_atTop 1] with n hn have hnpos : 0 < (n : ℝ) := by exact_mod_cast hn have hrate_nonneg : 0 ≤ (n : ℝ) ^ (-(1 / 4 : ℝ)) := Real.rpow_nonneg (Nat.cast_nonneg n) _ have hrate_prod : (n : ℝ) ^ (-(1 / 4 : ℝ)) * (n : ℝ) ^ (-(1 / 4 : ℝ)) = (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [← Real.rpow_add hnpos] congr 1 norm_num have hpoint : μ (C n) ≤ μ (A n) + μ (B n) := by have hsubset : C n ⊆ A n ∪ B n := by intro ω hω by_contra hnot have hnotA : ¬ δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) < |Xn n ω| := by intro hx exact hnot (inl hx) have hnotB : ¬ δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) < |Yn n ω| := by intro hy exact hnot (inr hy) have hXle : |Xn n ω| ≤ δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) := le_of_not_gt hnotA have hYle : |Yn n ω| ≤ δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) := le_of_not_gt hnotB have hbound_nonneg : 0 ≤ δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) := mul_nonneg (le_of_lt hδpos) hrate_nonneg have hprod : |Xn n ω * Yn n ω| ≤ ε * (n : ℝ) ^ (-(1 / 2 : ℝ)) := by calc |Xn n ω * Yn n ω| = |Xn n ω| * |Yn n ω| := abs_mul (Xn n ω) (Yn n ω) _ ≤ (δ * (n : ℝ) ^ (-(1 / 4 : ℝ))) * (δ * (n : ℝ) ^ (-(1 / 4 : ℝ))) := mul_le_mul hXle hYle (abs_nonneg _) hbound_nonneg _ = ε * (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [mul_mul_mul_comm, hδsq, hrate_prod] exact not_lt_of_ge hprod hω calc μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) simpa [C] using hpoint

Causalean.ML.isLittleOp_mul_quarter · Causalean/ML/Core/Rate.lean:43 · uses IsLittleOp

def AchievesL2Rate reviewed

Causalean.ML

For a measurable sample space, a measurable covariate space, a sequence of estimated regression functions indexed by sample size and experiment outcome, a target regression function, a joint covariate--response measure, a real-valued rate sequence, and an experiment measure, the predicate that the estimators achieve the stated L² rate holds precisely when for every sample size and experiment outcome, the L² seminorm of the estimation error under the covariate marginal of the joint measure is finite, and the resulting real-valued sequence of L² seminorms is stochastically bounded at the supplied rate under the experiment measure.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

X :

Type*

MeasurableSpace X

hhat :

ℕ → Ω → (X → ℝ)

hstar :

X → ℝ

P :

Measure (X × ℝ)

rn :

ℕ → ℝ

μ :

Measure Ω

def

AchievesL2Rate hhat hstar P rn μ :

Prop

given by

clause 1

n ω :

eLpNorm (fun x => hhat n ω x - hstar x) 2 (P.map fst) ≠ ⊤

clause 2

IsBigOp (fun n ω => (eLpNorm (fun x => hhat n ω x - hstar x) 2 (P.map fst)).toReal) rn μ

Causalean.ML.AchievesL2Rate · Causalean/ML/Core/Rate.lean:196

2 supporting declarations (lemmas, instances)

isLittleOp_one_of_le_one theorem — Rate weakening: an o_p(rn) sequence with rn ≤ 1 is o_p(1).

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
shared

rn :

ℕ → ℝ

hr :

∀ n, rn n ≤ 1

h :

IsLittleOp Xn rn μ

conclusion

IsLittleOp Xn (fun _ => 1) μ

Proof (Lean source)

theorem isLittleOp_one_of_le_one {rn : ℕ → ℝ} (hr : ∀ n, rn n ≤ 1) (h : IsLittleOp Xn rn μ) : IsLittleOp Xn (fun _ => 1) μ := by intro ε hε have hlim : Tendsto (fun n => μ {ω | ε * rn n < |Xn n ω|}) atTop (𝓝 0) := h ε hε refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hlim (fun n => zero_le) ?_ intro n apply measure_mono intro ω hω have hmul : ε * rn n ≤ ε * 1 := mul_le_mul_of_nonneg_left (hr n) (le_of_lt hε) exact lt_of_le_of_lt hmul (by simpa using hω)

Causalean.ML.isLittleOp_one_of_le_one · Causalean/ML/Core/Rate.lean:29
isLittleOp_quarter_of_isBigOp_sqrt theorem — An O_p(n^{-1/2}) (root-n) rate is o_p(n^{-1/4}): a method's root-n estimation rate clears the DML o_p(n^{-1/4}) bar.

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
shared

h :

IsBigOp Xn (fun n => (sqrt (n : ℝ))⁻¹) μ

conclusion

IsLittleOp Xn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ

Proof (Lean source)

theorem isLittleOp_quarter_of_isBigOp_sqrt (h : IsBigOp Xn (fun n => (sqrt (n : ℝ))⁻¹) μ) : IsLittleOp Xn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ := by intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ by_cases hδtop : δ = ⊤ · filter_upwards with n simp [hδtop] have hδpos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop let α : ℝ := δ.toReal / 2 have hαpos : 0 < α := by dsimp [α] linarith rcases h α hαpos with ⟨M0, hM0⟩ let M : ℝ := max M0 1 have hMpos : 0 < M := by dsimp [M] exact lt_of_lt_of_le zero_lt_one (le_max_right M0 1) have hM0le : M0 ≤ M := by dsimp [M] exact le_max_left M0 1 let A : ℕ → Set Ω := fun n => {ω | ε * (n : ℝ) ^ (-(1 / 4 : ℝ)) < |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | M * (sqrt (n : ℝ))⁻¹ < |Xn n ω|} have hlimB : limsup (fun n => μ (B n)) atTop ≤ ofReal α := by refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hM0 intro n apply measure_mono intro ω hω dsimp [B] at hω ⊢ have hrate_nonneg : 0 ≤ (sqrt (n : ℝ))⁻¹ := inv_nonneg.mpr (Real.sqrt_nonneg _) exact lt_of_le_of_lt (mul_le_mul_of_nonneg_right hM0le hrate_nonneg) hω have hα_lt_delta : ofReal α < δ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [α] linarith · dsimp [α] linarith [le_of_lt hδpos] · exact hδtop have hBevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hlimB hα_lt_delta) have hthreshold : ∀ᶠ n : ℕ in atTop, M * (sqrt (n : ℝ))⁻¹ ≤ ε * (n : ℝ) ^ (-(1 / 4 : ℝ)) := by have ht : Tendsto (fun n : ℕ => (M / ε) * (n : ℝ) ^ (-(1 / 4 : ℝ))) atTop (𝓝 0) := by have hp : Tendsto (fun x : ℝ => x ^ (-(1 / 4 : ℝ))) atTop (𝓝 0) := by exact tendsto_rpow_neg_atTop (by norm_num : (0 : ℝ) < (1 / 4 : ℝ)) simpa using (Tendsto.const_mul (M / ε) (hp.comp tendsto_natCast_atTop_atTop)) have hevent_abs : ∀ᶠ n : ℕ in atTop, |(M / ε) * (n : ℝ) ^ (-(1 / 4 : ℝ))| < 1 := by have hnear := (Metric.tendsto_nhds.mp ht) 1 (by norm_num : (0 : ℝ) < (1 : ℝ)) simpa [Real.dist_eq, abs_mul, abs_div] using hnear filter_upwards [hevent_abs, eventually_ge_atTop 1] with n hnabs hn_ge have hnsmall : (M / ε) * (n : ℝ) ^ (-(1 / 4 : ℝ)) < 1 := (abs_lt.mp hnabs).2 have hnpos : 0 < (n : ℝ) := by exact_mod_cast hn_ge let q : ℝ := (n : ℝ) ^ (-(1 / 4 : ℝ)) have hqpos : 0 < q := by dsimp [q] exact Real.rpow_pos_of_pos hnpos _ have hinv_eq : (sqrt (n : ℝ))⁻¹ = (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [Real.sqrt_eq_rpow] rw [← Real.rpow_neg (le_of_lt hnpos)] have hpow_add : q * q = (n : ℝ) ^ (-(1 / 2 : ℝ)) := by dsimp [q] rw [← Real.rpow_add hnpos] congr 1 norm_num have hmul : (M / ε * q) * (ε * q) ≤ 1 * (ε * q) := by exact mul_le_mul_of_nonneg_right (le_of_lt hnsmall) (le_of_lt (mul_pos hε hqpos)) have hleft : (M / ε * q) * (ε * q) = M * (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [← hpow_add] field_simp [hε.ne'] calc M * (sqrt (n : ℝ))⁻¹ = M * (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [hinv_eq] _ = (M / ε * q) * (ε * q) := by rw [hleft] _ ≤ 1 * (ε * q) := hmul _ = ε * (n : ℝ) ^ (-(1 / 4 : ℝ)) := by simp [q] filter_upwards [hBevent, hthreshold] with n hBn hthr have hsubset : A n ⊆ B n := by intro ω hω dsimp [A, B] at hω ⊢ exact lt_of_le_of_lt hthr hω have heq : {ω | ε * (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) n < |Xn n ω|} = A n := by ext ω simp [A] rw [heq] exact le_of_lt (lt_of_le_of_lt (measure_mono hsubset) hBn)

Causalean.ML.isLittleOp_quarter_of_isBigOp_sqrt · Causalean/ML/Core/Rate.lean:106