Diffusion afp-devel d3612fa82146

Frequency_Moments: Remove duplication of lemmas from Concentration_Inequalities.
d3612fa82146
Actions

Tags

None

Subscribers

None

Description

Frequency_Moments: Remove duplication of lemmas from Concentration_Inequalities.

Details

Provenance

Emin Karayel <me@eminkarayel.de>

Authored on

Parents

rAFP62ebe231642c: Renamed a theorem

Branches

Unknown

Tags

Unknown

Event Timeline

Emin Karayel <me@eminkarayel.de> committed rAFPd3612fa82146: Frequency_Moments: Remove duplication of lemmas from Concentration_Inequalities..Jan 16 2024, 7:26 PM

Changes (6)

Path

Size

thys/

Distributed_Distinct_Elements/

Distributed_Distinct_Elements_Accuracy_Without_Cutoff.thy

Frequency_Moments/

Frequency_Moment_0.thy

Frequency_Moment_2.thy

Frequency_Moment_k.thy

Probability_Ext.thy

rAFPd3612fa82146

thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Accuracy_Without_Cutoff.thy

Loading...

thys/Frequency_Moments/Frequency_Moment_0.thy

Loading...

thys/Frequency_Moments/Frequency_Moment_2.thy

Loading...

thys/Frequency_Moments/Frequency_Moment_k.thy

Loading...

thys/Frequency_Moments/Probability_Ext.thy

Loading...

thys/Frequency_Moments/ROOT

Loading...